[Programming] Axiomatic Semantics examples

Axiomatic semantics에 대해서 이해가 되지 않는데 예제를 주실 수 있나요?

 

Axiomatic semantics는 Denotational semantics의 한 종류이다.

[Programming] Denotational semantics examples

Axiomatic semantics 또한 프로그램에서 특정 logic이

어떤 식으로 작동하고 값이 산출되는지를 확인하기 위해서 사용된다.

한마디로 Axiomatic semantics를 이용하는 목적은 프로그램의 계산을 검증하거나 확인하기 위해서 사용된다는 것이다.

따라서 Axiomatic semantics를 program logic를 예측한다고 하여 predicate calculus라고도 불린다.

Axiomatic semantics에는 두가지 조건이 있는데 Preconditions와 Postconditions이다.

말 그대로 Preconditions는 states보다 앞에 조건이 있으며, Postconditions는 states보다 뒤에 조건이 나온다.

따라서 같은 states라도 Precondtions인지 아니면 Postcondtions에 따라서 산출 값도 달라질 수 있다.

이해를 돕기 위해 예제를 바로 살펴보자.

 

//HOOAI
val = 1 * num -10 {val > 1}

 

위의 예제 코드를 살펴보면 val이라는 변수는 1*num-10을 한 값에 해당한다.

num이 어떤 값이 들어갈지는 모르지만 결과적으로 val은 1보다 커야 한다.

따라서 num에 대해서 preconditions를 지정하자면, val 값이 1보다 크게 나올 수 있는 num 값을 지정해야 된다.

 

A. {num >1}
B. {num>-5}
C. {num>20}
D. {num>100}

 

예를 들어 A부터 D까지 num에 대한 조건식이 있다고 가정한다면,

val값이 1보다 커야 하기 때문에 A와 B는 Invalid precondition, 즉 조건에 해당되지 못한다.

반면에 C와 D는 val 값이 1보다 크기 때문에 해당 조건에 충족하며, precondition에 해당된다.

또한 C와 D 중에서는 C가 weakest precondition에 해당되는 것이다.