Written by JS970
on April 11, 2023

프로그래밍언어론 2023-04-11 수업정리

Flow

프로그램 요소에 대한 사전조건(precondition)과 사후조건(postcondition)을 통해 프로그램의 의미를 파학한다.
프로그램 수행 측면 중 일부는 무시된다.
아래와 같이 표기된다.$${P}\ program\ {Q}$$
- P : 프로그램 수행 전의 조건, input specification
- Q : 프로그램 수행 후의 조건, output specification

여러 가능한 사전조건 중 주어진 사후조건에 대해 제한이 가장 작은 사전조건
아래는 wp의 예시이다.$${P}\ sum:= 2 * x +1\ {sum>1}$$
- 위 Axiomatic Semantics의 표현에서 사전조건으로 아래와 같은 식들이 모두 가능하다.
  - P : x > 50
  - P : x > 40
  - P : x > 10
  - P : x > 0
- x > 50은 x > 40, x >10, x > 0을 imply(함의) 할 수 있다.
- 따라서 이 중에서 사후조건 sum>1 에 대해 가장 제약이 적은 사전조건은 P : x > 0이다.
  - wp : x > 0
만약 wp를 output specification으로부터 추론 가능하다면 해당 프로그램 정상적인 프로그램이라고 말할 수 있다.
- 프로그램(S)의 결과(Q)에 대한 최약 사전조건(WP)이 도출되지 않는다면 비정상적인 프로그램이다.
- 이를 사용해 프로그램의 유효성에 대한 증명을 할 수 있다.

$${Q[E/x]}\ x:= E\ {Q}$$

Q{[E/x]}란, Q의 자유 변수 x를 모두 E로 치환한 것이다.
적용 예시 $${P}\ a:=b/2-1\ {a<10}$$ $${a<10}[(b/2-1)/a]$$ $${b/2-1 < 10}$$ $${b<22}$$

Weakening the Postcondition$$\frac{{P}\ S\ {Q'}, Q' \Rightarrow Q} {{P}\ S\ {Q}}$$
Strengthen the Precondition$$\frac{P\Rightarrow P',\ {P'}\ S\ {Q}}{{P}\ S\ {Q}}$$
Merging them$$\frac{P\Rightarrow P',\ {P'}\ S\ {Q'},\ Q'\Rightarrow Q}{{P}\ S\ {Q}}$$
적용 예시$$\frac{x>5\Rightarrow x>3,\ {x>3}\ x:x-3\ {x>0}}{{x>5}\ x:x-3\ {x>0}}$$

$$\frac{{P}\ S_1\ {Q},\ {Q}\ S_2\ {R}}{{P}\ S_1;S_2\ {R}}$$

S1, S2를 순차적으로 실행하면 P로부터 R을 유도할 수 있다.
적용 예시$${P}\ y:=3*x + 1;x:= y+3\ {x<10}$$
- Assignment Axiom을 적용하여 아래와 같이 식의 변형이 가능하다.$${P}\ y:=3*x+1\ {y<7}$$
- 다시 Assignment Axiom을 적용하면$${P}\Rightarrow{x<2}$$

$$\frac{{P\wedge B}\ S_1\ {Q},\ {P \wedge \neg B}\ S_2\ {Q}}{{P}\ if \ B\ then\ S_1\ else\ S_2}$$

$$\frac{{I\wedge B}\ S\ {I}}{{I}\ while\ B\ do\ S\ {I\wedge \neg B}}$$

I : Loop Invarient, 루프 불변식
- 반복문 수행 전에도 참
- 반복문 수행 중에도 참
- 반복문 수행 후에도 참
- 항상 참이다.

다음 구문에서 weakest precondition을 찾으시오

while y!=x do
	y := y+1
{y=x}

(cont...)

Top