Concetti Chiave
하이퍼 호어 로직은 프로그램 하이퍼프로퍼티를 증명하거나 반증할 수 있는 일반적이고 강력한 프로그램 논리이다.
Sintesi
이 논문은 하이퍼 호어 로직을 소개한다. 하이퍼 호어 로직은 프로그램 하이퍼프로퍼티를 증명하거나 반증할 수 있는 일반적이고 강력한 프로그램 논리이다.
주요 내용은 다음과 같다:
하이퍼 호어 로직의 핵심 규칙을 정의하고, 이 규칙들이 완전하고 건전함을 증명한다.
하이퍼 호어 로직이 기존 호어 로직들이 다루지 못했던 다양한 종류의 하이퍼프로퍼티를 다룰 수 있음을 보인다. 이는 과소추정(underapproximation)과 과대추정(overapproximation) 추론을 모두 지원하기 때문이다.
하이퍼 호어 로직의 표현력을 입증하기 위해, 기존 호어 로직들로는 표현할 수 없었던 일반화된 비간섭(generalized non-interference) 등의 하이퍼프로퍼티를 다룰 수 있음을 보인다.
하이퍼 호어 로직의 모든 기술적 결과를 Isabelle/HOL에서 검증했다.
Statistiche
프로그램 상태는 지역 변수에서 값으로의 전체 함수로 정의된다.
프로그램 명령어에는 skip, 할당, 비결정적 할당, assume, 순차 실행, 비결정적 선택, 비결정적 반복 등이 포함된다.
하이퍼 호어 로직의 핵심 규칙에는 Skip, Seq, Cons, Exist, Assume, Assign, Havoc, Choice, Iter 등이 있다.
하이퍼 호어 로직은 건전성과 완전성이 증명되었다.