Hoare Logic 루프 불변량

Question

Hoare Logic을보고 있는데 루프 불변성을 찾는 방법을 이해하는 데 문제가 있습니다.

누군가가 루프 불변량을 계산하는 데 사용 된 방법을 설명 할 수 있습니까?

그리고 루프 인바 리언 트가 포함해야하는 것은 "유용한"것이어야합니까?

난 단지 같은 예에서, 간단한 예제를 다루는 불변을 발견하고, 부분과 전체 보정을 증명하고 있습니다 :

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 } 

Answer 1

, 다음 전제 조건 및 사후 조건을 사용하여 프로그램을 분해 유도 공식을 작성하고 증명하는 호어의 논리 추론 시스템의 규칙을 사용합니다. 당신의 예에서

, 당신은 귀하의 경우에는 규칙

{p} while b do S {p^not(b)} <=> {p^b} S {p} 

를 사용하여 프로그램을 분해 할

• P : 내가 ≥ 0
• B :> 0
• S : i : = i-1.

따라서 다음 단계에서 우리는 {i ≥ 0^i > 0} i := i−1 {i ≥ 0}을 유추합니다. 이것은 더 추론되고 아주 쉽게 증명 될 수 있습니다. 도움이되기를 바랍니다.

Answer 2

이 (당신의 추론에) 도움이된다는 것은 불변의 주요 포인트입니다. 따라서 입증하려는 사후 조건을보고 사후 조건에 도달하고 루프 코드에서 파생되는 데 도움이되는 불변량을 만들기 위해 시도하십시오.

Answer 3

이 귀하의 질문에 대답합니다 있는지 확실하지 않습니다,하지만 단지의 경우에 수행합니다

• A "루프 불변"비공식적 전과의 반복 후 진정한 남아있는 사실의 진술입니다 고리. 그것은 본질적으로 해당 루프와 관련하여 프로그램의 일관성 제약 조건을 정의합니다.
• Hoare Logic에 대해 루프 불변량이 어떻게 '계산'되는지 정확하게 알 수는 없지만 공식적인 증명 언어 자체보다 분석 된 코드의 언어에 의존 할 것이라고 생각됩니다. . 함께 작업하는 정식 알고리즘 설명이 있습니까? 좀 더 배경을 가지고 더 나아갈 수도 있습니다.
• 유용한 루프 불변성은 응용 프로그램의 상태에 특정한 것을 설명합니다. 예를 들어 Insertion Sort를 작성하는 경우 주 요소 이동 루프에 대한 유용한 루프 불변 식은 본질적으로 (하위) 목록에 루프 실행 전후의 동일한 개체 모음이 포함되어 있으며 이전에 있었던 요소 정렬 된 순서로 정렬 된 순서로 유지됩니다. 우리가 프로그램의 (부분) 정확성을 입증하기위한 호어의 논리에 대해 이야기하는 경우