정식 논리의 정확성 증명.

Question

누구든지이 질문에 답할 수 있는지 궁금합니다. 이전 시험지에서 나온 것으로 이번 해의 시험 준비를 알면됩니다.

이 질문은이 요구를 정확히, 내가 완전히 잃어버린 오전 너무 간단 보인다?

코드 관련된 정수 변수의 다음 섹션 고려해

if (i < j) { 
    m = i; 
} else { 
    m = j; 
} 

적절한 출력 조건을 명시하고 코드의 단편의 정확성을 확인하여를 실행 한 후 그 증명, m은 같다 최소 i와 j. {난은 m = ∧ < J ∨ m = J ∧ J < 제가 }

이 올바른지 :

I는 사후 조건을 가지고? 어떻게 이것을 확인합니까? 그것은 단순 해 보인다.

감사합니다.

Answer 1

게시물 상태가 정확합니다.

(i<j → m=i) ∧ (i≥j → m=j) 

이 프로그램은 다음을 수행 포스트 조건을 만족하는 것을 증명하려면 : 개인적으로 더 자연스러운하지만 (동등) 다음과 같은 변형을 찾을 수 있습니다. 항상 만족 포스트 조건이 당신이 당신의 사전 조건으로 true를 사용한다 확인 프로그램을 만들 수

1. 참고.

2. 그래서 당신은 트리플 다음 호어 있습니다

   {true} 
   if (i < j) { 
   
   
       m = i; 
   
   } else { 
   
   
       m = j; 
   
   } 
   {(i < j → m = i) ∧ (i ≥ j → m = j)} 
   

3. 사후 조건은 우리가

   이 너무 (조건문에 대한 표준 약한 전제 조건 규칙에 따라), 두 가지의 끝에서 개최 할 필요가

   {true} 
   if (i < j) { 
   
   
       m = i; 
       {(i < j → m = i) ∧ (i ≥ j → m = j)}  <--. 
   } else {          | 
                  | 
                  | 
       m = j;          | copy 
       {(i < j → m = i) ∧ (i ≥ j → m = j)}  <--| 
   }            | 
   {(i < j → m = i) ∧ (i ≥ j → m = j)} ----------' 
   

4. 할당 수율에 대한 약한 전제에 따라 상기 가입 화학식 밀기

   진정한 지점의 상단에

5. 우리는 i < j가, 그리고 다른 지점의 상단에 우리가 알고있는 것을 알고 ¬(i < j)이 : 표시하려면 왼쪽 무엇

   {true} 
   if (i < j) { 
       {i < j}        (1) <--- added 
       {(i < j → i = i) ∧ (i ≥ j → i = j)} (2) 
       m = i; 
       {(i < j → m = i) ∧ (i ≥ j → m = j)} 
   } else { 
       {¬(i < j)}       (3) <--- added 
       {(i < j → j = i) ∧ (i ≥ j → j = j)} (4) 
       m = j; 
       {(i < j → m = i) ∧ (i ≥ j → m = j)} 
   } 
   {(i < j → m = i) ∧ (i ≥ j → m = j)} 
   

6. 어떤 두 개의 연속적인 주장을위한의 첫 번째 주장은 두 번째 주장을 암시한다. (이 일반적으로 "증거 의무"라고합니다.) 우리는이 개 같은 의무를 가지고 : (1)이 (2)을 의미해야하며 (3)이 (4)을 의미한다. 이것은 분명히 드러납니다.

   - 나는 아틸라 희망