weakest precondition을 하면서 쉽다고 생각했지만 생각도 못하게 어려움을 봉착하여 이 글을 작성한다. 아직 개념을 이해하지 못하고 단순히 수학문제 풀듯이 풀었던 것이 오산이었다.
- 예시와 함께 보자
x = y + 1;
y = y - 2;
{y < 3}여기서 weakest precondition은 무엇일까?
내 처음 생각
후조건이 {y<3}이니깐 두번째 식의 weakest precondition은 {y<5}이다.
(y-2<3 이므로 y<5 이다.)
//여기까진 맞다.
x=y+1이고 후조건이 y<5 이므로 첫번째 식의 weakest precondition은
x=y+1<6으로, {x<6}이 정답이다. - 하지만 이것은 틀렸다.
정답
후조건이 {y<3}이니깐 두번째 식의 weakest precondition은 {y<5}이다.
(y-2<3 이므로 y<5 이다.)
{?} x=y+1 {y<5}에서 x=y+1을 잘 살펴보자
x=y+1은 x 에다가 y+1을 대입?한다는 것이다.
이 식은 y의 후조건에 직접적인 영향이 없는 식인 것이다.
따라서 그저 {y<5}가 weakest precondition이 된다.내가 잘못 생각했을 때의 논리는 x<6이어야 y<5 라는 것이다.
이것은 단순히 수학적으로 생각했을 때는 맞을지 모르나 x=y+1 이라는 것이 아니라 정확히는 x:=y+1, 즉 y+1을 x에다가 대입하는 것이다.
y의 값으로 x의 값이 정해지지, x의 값으로 y의 값이 정해지는 것이 아니다.
따라서 x 의 값은 사실 precondition으로 주어지지 않아도 된다.
- 추가적으로 if else 에 대한 정리
if x > 0 then a = y - 1 else a = y + 1
이 식에서 {a>0}이 후조건이라고 하자.
우리는 x에 대한 정보를 모르기에 사용될 식이 위쪽 true일때의 식인지, 아래쪽 false일 때의 식인지 알 수 없다.
우선 두 식의 precondition 먼저 구해보자 .
위의 식의 precondition은 {y>1}, 아래 식의 precondition은 {y>-1}이다.
앞에서 말했듯이 우리는 위의식을 사용할지, 아래식을 사용할지 알 수 없다.
이 때, 우리는 precondition을 strengthen 할 수 있고, postcondition을 weaken 할 수 있다.
두 식 중 더 강한 식을 사용하려면, {y>1}이라는 식을 사용할 수 밖에 없다.
만약 x에 대한 정보가 있다면 사용되는 식에 대해서만 신경을 쓸 수 있다.
*^^*