증명하는 방법에 잠시/대한 이자벨/HOL

Question

에 나는이 C 코드를 가지고 :

내가 입증 할

while(p->next) p = p->next; 

이이 루프가 끝날 때 목록이 p->next이 NULL 동일, 얼마나 오래 상관없이 및 EIP는이 루프 이후의 다음 명령어를 참조합니다.

하지만 그렇게 할 수는 없습니다. 누구든지 루프를 증명하는 방법을 알고 있습니까 이사벨/호브?

Answer 1

더 많은 추론을 위해 C 코드를 Isabelle/HOL로 가져올 수있는 일련의 도구 (부인 : 저는 후자입니다)는 Michael Norrish의 C Parser 및 AutoCorres입니다. 명령 사용 이자벨에

struct node { 
    struct node *next; 
    int data; 
}; 

struct node * traverse_list(struct node *list) 
{ 
    while (list) 
     list = list->next; 
    return list; 
} 

: AutoCorres를 사용

, 나는 다음과 같은 C 파일을 구문 분석 할 수

theory List 
imports AutoCorres 
begin 

install_C_file "list.c" 
autocorres [ts_rules = nondet] "list.c" 

우리는 다음 내용의 호어 트리플 증명할 수, 즉 모든 입력 상태에 대해 함수의 반환 값은 :

lemma "⦃ λs. True ⦄ traverse_list' l ⦃ λrv s. rv = NULL ⦄" 
    (* Unfold the function definition. *) 
    apply (unfold traverse_list'_def) 

    (* Add an invariant to the while loop. *) 
    apply (subst whileLoop_add_inv [where I="λnext s. True"]) 

    (* Run a VCG, and solve the conditions using the simplified. *) 
    apply wp 
    apply simp 
    done 

T입니다. 그의 정확성 정리는 부분 정확도 정리인데 다소은 당신이 요구 한 것을 말합니다. (특히 일 경우 함수가 종료되고 이면이면 오류가 발생하지 않으며 사후 조건은 true입니다).

보다 완벽한 증거를 들어

, 당신은 위의 몇 가지를 추가해야합니다 :

1. 하는 당신은 목록이 유효한지 알 필요가; 예를 들어 중간 노드가 잘못된 주소 (예 : 정렬되지 않은 주소)를 가리 키지 않으며 목록이 루프를 형성하지 않는다는 것을 의미합니다 (while 루프가 절대로 종료되지 않음을 의미).

2. 또한 해지를 입증해야합니다. 위의 두 번째 조건과 관련이 있지만, 왜 그것이 사실인지에 대한 논의를해야 할 것입니다. (일반적인 방법은 목록의 길이가 항상 감소하므로 결국 루프가 종료 됨).

AutoCorres는 명령 포인터의 개념을 지시하지 않지만 일반적으로 이러한 개념은 어셈블리 수준에서만 존재합니다. 그러나 종료 증명은 비슷합니다.

AutoCorres는 DataStructures.thy에 연결된 목록에 대한 추론을위한 몇 가지 기본 라이브러리를 제공합니다. 이는 좋은 시작점입니다.