공리적 의미론

문장 앞뒤에 조건을 답니다

공리적 의미론(axiomatic semantics)은 문장의 앞뒤에 변수에 대한 조건을 논리식으로 적습니다. 이 조건이 단언(assertion)입니다. 앞의 사전 조건(precondition)이 참일 때 문장을 실행하면, 뒤의 사후 조건(postcondition)이 참이 됩니다.

이 강의가 따르는 교재의 예입니다(b 값은 예시). 여기 { }는 조건을 묶는 표시입니다(EBNF의 되풀이와 다릅니다). 이런 기본 규칙이 공리(axiom)입니다.

가장 느슨한 조건

딱 필요한 만큼만 요구합니다

a > 1 을 보장하려면 실행 전에 b > 0 이면 충분합니다. b > 10 도 보장은 하지만 필요 이상으로 좁습니다. 사후 조건을 보장하는 사전 조건 가운데 가장 느슨한 것이 최약 사전 조건(weakest precondition)입니다.

움직이는 점의 b 값은 예시입니다.

증명하는 순서

결과에서 거꾸로 올라갑니다

먼저 프로그램 전체의 사후 조건, 곧 원하는 결과를 적습니다. 마지막 문장부터 거꾸로 올라가며 필요한 사전 조건을 구합니다. 맨 앞에서 얻은 조건이 프로그램의 명세(지켜야 할 조건)와 같으면 프로그램은 정확합니다.

명세는 영어로 specification입니다. 첫 문장 b = x * 2 는 예시이고, * 는 곱하기입니다.

반복문

돌아도 변하지 않는 조건을 찾습니다

반복문은 몇 번 돌지 미리 알 수 없습니다. 그래서 도는 내내 참인 조건을 찾아 씁니다. 반복 불변식(loop invariant)입니다. 반복이 끝나면 불변식과 반복이 끝난 조건을 합쳐 사후 조건을 얻습니다.

예시 값입니다. 반복은 y ≠ x 인 동안 돌고, y가 x와 같아지면 끝납니다.

세 방법

무엇으로 적느냐가 다릅니다

조작적 의미론은 실행 과정으로, 표시적 의미론은 수학 함수로, 공리적 의미론은 논리 조건으로 뜻을 적습니다. 직관적인 설명에는 조작적, 엄밀한 정의에는 표시적, 프로그램 검증에는 공리적 의미론이 쓰입니다.

추상화 수준이 낮다는 것은 실제 실행 과정에 가깝다는 뜻입니다.

2강 정리

생김새, 검사, 뜻을 형식으로 적었습니다

구문은 BNF로 적고, 유도와 파스 트리로 문장의 구조를 봅니다. 실행 전에 검사할 규칙은 속성 문법으로, 실행할 때의 뜻은 세 가지 의미론으로 적습니다.