1. Axiomatic Semantics
program이 semantics 적으로 올바른가? 가 무슨 뜻일까?
뒤에 더 설명하겠지만 프로그램의 precondition이 axiom원리에 의해 도출된 condition과 일치하면 correct하다고 할 수 있다.
즉 프로그램이 실행 전, 후 상태가 참이면 semantics가 올바르다고 볼 수 있다.
precondition이 true이고 GCD-1이 실행, 종료 뒤, postcondition이 true라는 말이다.
코드의 각 statement를 이 두 assertion을 가지고 판별한다면 아래와 같다.
즉 x:= x+4라는 프로그램의 post condition이 x = 10이라면, precondition이 {x=5}여야지
이 프로그램이 semantics상 올바르다고 할 수 있다는 것이다.
2 Axiom of assignment
post condition, precondition을 가지고 새로운 논리를 증명할때 사용할 수 있는 도구들을 하나씩 배워볼 것이다.
x:=E라는 코드가 실행되다가 Q라는 결과가 나왔을때 그 전 상태는 어떻게 되어야 할까?
---------> ??
a = b + 1
---------> {a > 1}
postcondition이 a>1일때, a = b + 1이 실행되기 전 상태는 뭘까?
항상 만족시킬 수 있는 weakest condition, { b>0 } 도 가능하고
stronger 한 것중 하나로는 {b>10}도 가능할 것이다.
이 precondition을 도출하기 위해 axiom of assignment를 사용한다.
{Qx->E} a = b + 1 {a>1}
Q는 a>1인데
x자리에 E를 대입하면은 a에 b+1을 대입하라는 말과 같다.
따라서 b+1> 1 -> b>0 이 된다.
inference rule중 하나인 consequence rule로 표현하면 아래와 같다.
분자에 식들이 참임을 증명하면 자연스럽게 분모가 참임을 뜻한다.
{P} a=b+1 {a>1} , {b>0} -> P
-------------------------------------
{b>0} a=b+1 {a>1}
3 Axiom of sequences
S_1, S_2 두 코드가 순서대로 실행될 때, 프로그램 상태들의 변화를 추적한다고 생각하면 이해가 더 쉽다.
1. sequence(composition) rule에 의해 {5 + 1 = 6} a:=5 {Q}, {Q} a := a+1 {a=6} 이면 위 식은 참이다.
2. {Q} a := a+1 {a=6} 에서 Q는 axiom of assignment에 의해 {a + 1 = 6}이다.
3. {5+1 = 6} a:= 5 {a + 1 = 6}를 이제 증명하자
4. axiom of assignment에 의해 {5+1 = 6}다.
5. 따라서 증명완료.
// Axiom of assignment
{Q} a := a+1 {a=6}, {Q} -> {a + 1 = 6}
---------------------------------------
{a + 1 = 6} a := a+1 {a=6}
// Axiom of assignment
{Q} a:=5 {a + 1 = 6}, {Q} -> {5 + 1 = 6}
-----------------------------------------
{5 + 1 = 6} a:=5 {a + 1 = 6}
// Axiom of consequence
{5 + 1 = 6} -> {Q}, {Q} -> a:=5 {a + 1 = 6}
----------------------------------------------
{5 + 1 = 6} a:=5 {a + 1 = 6}
// Axiom of sequence
{5 + 1 = 6} a:=5 {Q}, {Q} a := a+1 {a=6}
-----------------------------------------
{5 + 1 = 6} a:=5, a := a+1 {a=6}
4 Axiom of selection
if else 구문에서의 correctness를 판별해보자.
if - else 구문 끝에 post condition 이 R이고 precondition이 Q일때,
각 line이 실행될때마다의 상태 변화를 나타낸 그림이다.
따라서 if-else를 증명하려면 분자식을 만족시키면 된다.
5. Axiom of Loop
loop문이 있을 때, loop와 무관하게 변하지 않는 loop Invariant가 있을 것이다.
E를 만족하지 않으면 loop를 탈출해서 결국은 not E가 될 것이다.
정리하면 위와 같은 식이 도출된다.
이건 Invariant의 특징에 대한 설명이다. 결국 I는 변하지 않는다는 것을 의미한다. 하지만 loop가 끝난 뒤에 I에 대해서는 장담할 수 없다.
위 5가지 항목을 만족하면 loop는 올바르다고 할 수 있다.
6. Axiom of Consequence
assignment 구문들의 올바름을 판단할때 이 식을 사용할거다. {P'} S {Q'}가 올바르다는 걸 증명하려면
분자식을 증명하면 된다는 뜻이다.
pre-condition을 weaken하거나 post-condition을 강화할 수 있다.
'ComputerScience > Principle of programing language' 카테고리의 다른 글
PL7. Syntax Analysis - bottom up parsing (0) | 2023.10.27 |
---|---|
PL6. Syntax Analysis - top down parsing (0) | 2023.10.06 |
PL4. Dynamic semantics : Operational, Denotational (0) | 2023.09.27 |
PL3. Static semantic (0) | 2023.09.15 |
PL2. Syntax (0) | 2023.09.14 |