PL5. Dynamic semantics : Axiomatic

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을 강화할 수 있다.