술어 변환기 의미론

의미론
언어학적 논리적
하위 필드 계산 어휘(사전, 사전) 통계적 구조적 토픽 분석. 구성성 문맥 (언어 사용) 원형이론 힘의 동역학 미해결 언어학적 문제 의미적 특징 의미간극 기술론 분석. 잠재성 머신 러닝 적용들 시맨틱 파일 시스템 시맨틱 매칭 시맨틱 파싱 의미 유사성 시맨틱 쿼리 시맨틱 웹 시맨틱 위키
의 의미론 프로그래밍 언어
종류들 액션. 대수학 공리적 범주형 동시성 표시 게임 운용성 술어 변환 이론. 추상적 해석 추상적 의미 그래프
언어 언어학
v t

술어 트랜스포머 의미론은 Edsger Dijkstra가 그의 신학교 논문 "Guarded commands, nondeterminity and formal derivation of programs"에서 소개했습니다.이 언어의 각 문장에 대응하는 술어 변환기를 할당하여 명령형 프로그래밍 패러다임의 의미를 정의합니다. 즉, 문장의 상태 공간에서 두 술어 사이의 총 함수입니다.이런 의미에서 술어 트랜스포머 의미론은 일종의 표현적 의미론입니다.실제로, 보호 명령에서 Dijkstra는 단지 한 종류의 술어 변환기만을 사용합니다: 잘 알려진 가장 약한 전제 조건(아래 참조).

또한 술어 트랜스포머 의미론은 플로이드를 재구성한 것입니다.호어 논리.Hoare 논리가 연역 체계로 제시되는 반면, 술어 변환기 의미론(아래에서 보는 가장 약한 전제 조건 또는 가장 강한 사후 조건)은 Hoare 논리의 유효한 추론을 구축하기 위한 완전한 전략입니다.즉, 그들은 Hoare 트리플을 검증하는 문제를 1차 공식을 증명하는 문제로 줄이는 효과적인 알고리즘을 제공합니다.기술적으로 술어 변환기 의미론은 술어에 대한 일종의 상징적 실행을 수행합니다. 실행은 가장 약한 전제 조건의 경우 뒤로 실행되거나 가장 강한 사후 조건의 경우 앞으로 실행됩니다.

가장 약한 전제조건

정의.

문장 S와 후조건 R에 대하여, 가장 약한 전제조건은 어떤 전제조건 P에 대하여 $\{{\displaystyle P}$ ${\displaystyle \}}$ ${\displaystyle S}${${\displaystyle R}$}$${\$displaystyle$\}$S\{R\}$인 경우에만, ${\displaystyle P}$가 ${\displaystyle P\rightarrow$Q}인 경우에 한해, 술어 Q이다$.$ 즉, 이것은 S 다음에 R이 고정되는 것을 보장하기 위해 필요한 "최소한" 또는 최소 제한적인 요건입니다.고유성은 정의에서 쉽게 따르게 됩니다.만약 Q와 Q'가 모두 약한 전제조건이라면, 정의$${${\displaystyle {\text{'}\}}^{}}$S${\displaystyle }${${\displaystyle R\}}$ ${\displaystyle \{Q'\}S\{R\}$이므로 $Q{\displaystyle {\text{'}}^{}}$ ⇒ Q ${\displaystyle$ $'\rightarrow Q}$ 및 $\{{\displaystyle Q\}}$ ${\displaystyle S}${${\displaystyle R\}}$ ${\displaystyle \{Q\}S\{R\}$이므로 $Q$는 ${\displaystyle {}^{}}$⇒ ${\displaystyle Q\rightarrow$ Q$'$이므로$$$Q$ = ${\displaystyle {\text{'}}^{}}$ ${\displaystyle$Q=$Q'}$입니다$.$ 우리는 t를 나타내기 위해 ${\displaystyle \mathrm{종종}}$ w p ${\displaystyle (S,}$ R${\displaystyle }$) ${\displaystyle wp(S,R)}$를 사용합니다.사후 조건 R에 관하여 문장 S에 대한 가장 약한 전제 조건.

관습

T는 어디에나 참인 술어를, F는 어디에나 거짓인 술어를 나타냅니다.우리는 적어도 개념적으로 일부 언어 구문에 의해 정의된 부울 표현과 혼동해서는 안 됩니다. 부울 스칼라로서 참과 거짓을 포함할 수도 있습니다.그러한 스칼라에 대해 우리는 T = 술어(참)와 F = 술어(false)를 갖도록 유형 강제를 해야 합니다.그런 프로모션은 무심코 진행되는 경우가 많기 때문에 T는 진실, F는 거짓으로 받아들이는 경향이 있습니다.

건너뛰다.

${\displaystyle wp ({\texttt {skip}},R)\ =\ R}$

중단

${\displaystyle wp ({\texttt {abort}},R)\ =\ {\texttt {F}}$

과제

우리는 할당 명세서에 대한 두 가지 동등한 가장 약한 전제 조건을 아래에 제시합니다.이 공식에서 $R{\displaystyle }$[ ${\displaystyle x}$ ← E${\displaystyle }$] ${\displaystyle R$[ x$\leftarrow E]}$은(는) x의 자유 발생이 E로 대체되는 R의 복사본입니다.따라서 여기서 식 E는 기본 논리의 유효한 용어로 암시적으로 강제됩니다. 따라서 완전하게 정의되고 종료되며 부작용이 없는 순수한 표현입니다.

• 버전 1:

${\displaystyle wp(x:=E,R)\ =\ (\forall.y)=E\오른쪽 화살표 R[x\leftarrow])$ 여기서 y는 E와 R에서 자유롭지 않은 신선한 변수입니다(변수 x의 최종 값을 나타냄).

• 버전 2:

E가 잘 정의되어 있다면, 우리는 버전 1에 소위 원포인트 규칙을 적용할 뿐입니다.그리고나서

${\displaystyle wp(x:=E,R)\ =\R[x\leftarrow E]}$

첫 번째 버전은 R에서 x의 잠재적인 중복을 방지하는 반면, 두 번째 버전은 R에서 x가 최대로 한 번 발생할 때 더 간단합니다.첫 번째 버전은 또한 가장 약한 상태-전제 조건과 가장 강한 상태-후제 조건 사이의 깊은 이중성을 보여줍니다(아래 참조).

정수 값 변수 x가 있는 할당에 대한 wp(버전 2 사용)의 유효한 계산 예는 다음과 같습니다.

${\displaystyle {\begin{array}{rcl}wp(x:=x-5,x>10)&=&x-5>10\\\\left rightarrow &x>15\end{array}}$

과제 수행 후 조건 x > 10이 참이기 위해서는 과제 수행 전 전제 조건 x > 15가 참이어야 함을 의미합니다.이것은 또한 할당 후 x > 10을 참으로 만드는 x 값에 대한 "가장 약한" 제한이라는 점에서 "가장 약한 전제 조건"입니다.

순서

${\displaystyle wp(S_{1});S_{2},R)\ =\wp(S_{1},wp(S_{2},R)}$

예를들면,

${\displaystyle {\begin{array}{rcl}wp(x:=x-5;x:=x*2\,\x>20)&=&wp(x:=x-5,wp(x:=x*2,x>20))\\&=&wp(x:=x-5,x*2>20)\&=&(x-5)*2>20\&=&x>15\end{array}}$

조건부

${\displaystyle wp ({\texttt {if}}\ E\ {\texttt {then}}\ S_{1}\ {\texttt {else}}\ S_{2}\ {\texttt {end}},R)\ =\ (E\rightarrow wp(S_{1},R)\wedge(\neg E\rightarrow wp(S_{2},R))}$

예:

${\displaystyle {\begin{array}{rcl}wp ({\texttt {if}}\x<y\{\texttt {then}}\x:=y\{\texttt {else}}\;\;{\texttt {end}}\;\;{\texttt {end}},\x\geq y)&=(x<y\rightarrow wp(x=y,x\geq y))\\wedge \(\neg(y<y)\rightarrow wp ({\texttt {skip}},x\geq y)\\&=&(x<y\rightarrowy\geqy)\\wedge \(\neg(x<y)\rightarrow x\geqy)\&\rightarrow &{texttt {true}}\end{array}}$

While loop

부분 수정

잠시 동안 종료를 무시하면 술어 \textit{를 사용하여 wlp로 표시된 가장 약한 자유주의 전제조건에 대한 규칙을 정의할 수 있습니다.INV, [[루프 \textit{]]라는INV}ariant]], 일반적으로 프로그래머가 제공합니다.

${\displaystyle wlp({\texttt {while}})\E\{\texttt {do}}\S\{\texttt {done}},R)\왼쪽 화살표 \{\textit {INV}}\ \ {\text{if}}\ \ {\begin{array}{l}\(E\wedge {\textit {INV}}\오른쪽 화살표 wlp(S,{\textit {INV}).\\\wedge \ (\neg E\wedge {\textit {INV}}\오른쪽 화살표 R)\end{array}}$

총 정확도

완전한 정확성을 보여주기 위해서는 루프가 종료됨을 보여주어야 합니다.이를 위해 (wfs, <)로 표시된 상태 공간에 대한 잘 근거된 관계를 정의하고 변형 함수 vf를 정의합니다.

${\displaystyle wp({\texttt {while}})\E\{\texttt {do}}\S\{\texttt {done}},R)\\왼쪽 화살표 \{\textit {INV}}\ \ {\text{if}}\ \ \ \ \ begin{array}{l}\(E\wedge {\textit {INV}}\오른쪽 화살표 {\textit {vf}}\in {\textit {wfs})\\wedge \ (E\wedge {\textit {INV}}\wedge v={\textit {vf}}\오른쪽 화살표 wp(S,{\textit {INV}}\wedge v<{\textit {vf}})\\\wedge \ (\neg E\wedge {\textit {INV}}\오른쪽 화살표 R)\end{array}}$ 여기서 v는 변수의 새 튜플입니다.

비공식적으로 위의 세 가지 공식의 결합에서:

• 첫 번째는 루프에 진입하기 전에 변형이 근거가 충분한 관계의 일부여야 한다는 것을 의미합니다.
• 두 번째는 루프의 몸체(즉, 문장 S)가 불변성을 보존하고 변형을 감소시켜야 한다는 것을 의미합니다.
• 마지막은 루프가 끝날 때 루프 후조건 R이 성립되어야 함을 의미합니다.

그러나 이 세 가지의 결합은 필요조건이 아닙니다.맞아요, 저희가.

${\displaystyle wp ({\texttt {where}}\ E\ {\texttt {do}}\ S\ {\texttt {done}}, R)\ \ =\ {\text{재귀 방정식의 가장 강력한 해}}\ {\begin{array}}{l}Z:[Z\equiv (E\wedgewp(S,Z))\vee (\neg E\wedge R)]\end{array}}$

비결정성 경비 명령

사실, Dijkstra의 GCL(Guarded Command Language)은 여기까지 주어진 단순한 명령어의 확장이며, 결정적이지 않은 명령어입니다.실제로, GCL은 알고리즘을 정의하는 공식적인 표기법이 되는 것을 목표로 합니다.비결정론적 진술은 (효과적인 프로그래밍 언어로) 실제 구현에 맡겨진 선택을 나타냅니다. 비결정론적 진술에서 증명된 속성은 구현의 모든 가능한 선택에 대해 보장됩니다.즉, 비결정론적 진술의 가장 약한 전제조건은

• 종료 실행이 존재하는지 여부(예: 구현이 존재함),
• 그리고 모든 종료 실행의 최종 상태가 사후 조건을 만족하는지 여부.

위에 제시된 가장 약한 전제 조건(특히, while-loop의 경우)의 정의는 이 속성을 유지합니다.

선택.

선택은 if 문을 일반화한 것입니다.

${\displaystyle wp({\texttt {if}})\E_{1}\오른쪽 화살표 S_{1}\[\!]\ \ldots \[\!]\E_{n}\오른쪽 화살표 S_{n}\{\texttt {fi}},R)\ = {\begin{array}{l}(E_{1})\vee \ldots \vee E_{n})\wedge \ (E_{1}\rightarrow wp(S_{1},R)\\ldots \(E_{n}\rightarrow wp(S_{n},R))\\\dots \(E_{n}\rightarrow wp(S_{n},R))\\\end{array}}}$

^{[citation 필요]}

여기서 두 $개$의 ${\displaystyle {가드}_{}}$ Ei$${\$displaystyle$E_${i$}와 Ej$${\$displaystyle$E_${j$}가 동시에$$ 참일 때, 이 문을 실행하면 연관된 문장 ${\displaystyle {Si}_{}}$ ${\$ 또는$$ ${\displaystyle {Sj}_{}}$ ${\$를 실행할 수 있습니다$.$

반복

반복은 비슷한 방식으로 while문을 일반화하는 것입니다.

규격명세서

정제 미적분학은 사양문 개념으로 GCL을 확장합니다.통사적으로, 우리는 사양 문을 다음과 같이 쓰는 것을 선호합니다.

     ${\displaystyle x:l[pre,post]}$ 

이것은 pre를 만족하는 상태에서 시작하여 x만 변경함으로써 post를 만족하는 상태로 끝날 것을 보장하는 계산을 지정합니다.$우리$는$$l {\$displaystyle$ l$}$을(를) 규격에 도움이 되는 논리$$ 상수라고 부릅니다.예를 들어 x를 1씩 증가시키는 계산을 다음과 같이 지정할 수 있습니다.

     ${\displaystyle x:l[x=l,x=l+1]}$ 

다른 예로는 정수의 제곱근 계산이 있습니다.

     ${\displaystyle x:l[x=l^{2},x=l]}$ 

규격문은 다른 문을 포함하지 않는다는 점에서 원시문처럼 보입니다.그러나 사전과 사후는 임의의 술어이기 때문에 매우 표현력이 뛰어납니다.가장 약한 전제조건은 다음과 같습니다.

${\displaystyle wp(x:l[pre,post],R)=(\exist l::pre)\wedge(\모든 경우:(\for all:pre:post(x\left 화살표)):R(x\왼쪽 화살표)}$ s는 신선합니다.

그것은 모건의 통사적인 생각과 비즐마, 매튜스, 윌트링크의 날카로움의 생각을 결합한 것입니다.^[1]이것의 가장 큰 장점은 고투 L의 wp와 다른 점프문을 정의하는 능력입니다.

전표로 이동

go to L과 같은 점프문의 형식화는 매우 긴 험난한 과정을 거칩니다.일반적인 믿음은 고투 진술이 작동적으로만 주장될 수 있음을 나타내는 것 같습니다.이것은 아마도 고트 L이 실제로 기적적이라는 것을 인식하지 못했기 때문일 것이며(즉, 엄격하지 않음), 그 자체로서 디크스트라의 기적 배제 법칙을 따르지 않기 때문일 것입니다.하지만 가장 취약한 전제조건 관점에서 매우 단순한 운영 관점을 누리고 있는데, 이는 예상치 못했던 것입니다.우리는 정의합니다.

${\displaystyle wp ({\texttt {goto}}\L,R)=wpL}$ 여기서 wpL은 라벨 L에서 가장 약한 전제조건입니다.

Good L 실행의 경우 가장 약한 전제 조건이 유지되어야 하는 레이블 L로 제어가 전달됩니다.규칙에서 wpL이 언급되는 방식은 큰 놀라움으로 받아들여져서는 안됩니다.해당 지점에 계산된 일부 Q에 대해$$ ${\displaystyle \mathrm{wp}(L:S,Q)}$ ${\displaystyle wp(L:S,Q)}$입니다.이는 구성 문을 사용하여 wp 정의를 제공하는 다른 wp 규칙과 유사합니다. 비록 go to L이 원시적인 것처럼 보이지만.이 규칙은 프로그램 내에서 wpL이 유지되는 위치에 대한 고유성을 요구하지 않으므로 이론적으로 각 위치에서 가장 약한 전제 조건이 동일한 wpL인 한 동일한 레이블이 여러 위치에 나타날 수 있습니다.이동 명령문은 해당 위치로 이동할 수 있습니다.이것은 실제로 S${\displaystyle (L}$ :${\displaystyle L}$ :${\displaystyle }$S $)$ {\$displaystyle$ S$(L:L$:${\displaystyle \mathrm{S1})\}}$와$$$동일$한 S$($ :${\displaystyle }$S1$)$ {\$displaystyle$ S$(L$ : $S1)}$와 동일한 동일한 위치에 동일한 레이블을 여러 번 배치할 수 있음을 정당화합니다$.$ 또한 범위 지정 규칙을 의미하지 않으므로 예를 들어 루프 본체로 점프할 수 있습니다.루프 본체로 점프하는 다음 프로그램 S의 wp를 계산해 보겠습니다.

wp(dox > 0 → L : x : = x-1 od; if x < 0 → x : = -x; 이동 L ⫿ x ≥ 0 → fi 건너뛰기, 게시물) = {순차구성 및 교대규칙 } wp(dox > 0 → L : x : = x-1 od, (x < 0 ∧ wp(x : = -x; 이동 L, 게시물) ∨(x ∧ 0 ≥ 게시물) → {순차구성, 이동, 배정규칙 } wp(do x > 0 = x : ← x-1 od, x < 0 ∧ wpL(x = -x) ∨ x ≥0 ∧ 게시물) = {반복규칙 wp(x : -x)}      Z의 가장 강력한 해: [ Z ≡ x > 0 ∧ wp (L : x : = x-1, Z) ∨ x < 0 ∧ wpL (x ← -x) ∨ x = 0 ∧ post ] = {할당 규칙,발견된 wpL = Z(x ← x-1) } Z의 가장 강한 해: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← x-1) (x ← -x) ∨ x = 0 ∧ 포스트] = { 치환} Z의 가장 강한 해: [ Z ≡ x > 0 ∧ Z(x ← x-1) ∨ x < 0 ∧ Z(x ← -x-1) ∨ x = 0 ∧ 포스트 ] = { 근사로 방정식을 푸세요 } 포스트(x ← 0)

그러므로,

wp(S, post) = post(x ← 0).

기타 술어 변환기

가장 약한 자유주의 전제조건

가장 약한 전제 조건의 중요한 변형은 가장 약한 자유 전제 조건 ${\displaystyle \mathrm{wlp}(S,R)}$ ${\displaystyle wlp(S,R)}$이며$,$ 이는 S가 종료되지 않거나 R을 설정하는 가장 약한 조건을 산출합니다.따라서 종료를 보장하지 않는다는 점에서 wp와 차이가 있습니다.따라서 부분 수정에서는 Hoare 논리에 해당합니다. 위에 주어진 문장 언어의 경우 wlp는 wp와 오직 while-loop에서만 다르고 변형이 필요하지 않습니다(위 참조).

가장 강력한 포스트 컨디션

S 문과 R이 전제 조건(초기 상태의 술어)일 때,${\displaystyle }$sp (${\displaystyle S,}$R$)$ {\$displaystyle sp(S$,R$)}$는 그들의 가장 강한-사후 조건입니다$$: 그것은 R을 만족하는 모든 초기 상태에 대해 S의 실행의 최종 상태에 의해 충족되는 모든 후조건을 의미합니다.즉, 호아레 삼중 {${\displaystyle P}$ ${\displaystyle \}}{\displaystyle }$S${\displaystyle }${$}$ {\$displaystyle \{P\}S$\{Q$\}}$는 다음과 같은 경우에만 호아레 논리에서 증명할 수 있습니다$$.

${\displaystyle \for all x,sp(S,P)\오른쪽 화살표 Q}$

일반적으로 부분 수정 시에는 가장 강한 사후 조건이 사용됩니다.따라서, 우리는 가장 약한-자유주의-전제조건과 가장 강한-후제조건 사이에 다음과 같은 관계를 갖습니다.

${\displaystyle(\모든 x에 대해),P\오른쪽 화살표 wlp(S,Q))\\왼쪽 오른쪽 화살표 \(\모든 x에 대해,sp(S,P)\오른쪽 화살표 Q)}$

예를 들어, 할당 시 다음과 같은 내용이 있습니다.

${\displaystyle sp(x:=E,R)\ =\ \exists y,x=E[x\leftarrow]\wedge R[x\leftarrow]}$ y가 신선한 곳에

위에서 논리 변수 y는 변수 x의 초기 값을 나타냅니다.이런 이유로,

${\displaystyle sp(x:=x-5,x>15)\ =\ \exists y,x=y-5\wedge y>15\ \ \\좌우 화살표 \x>10}$

순서에 따라 spr은 앞으로 달리는 것처럼 보입니다(wp는 뒤로 달리는 반면).

${\displaystyle sp(S_{1};S_{2}\,\R)\ =\sp(S_{2},sp(S_{1},R())}$

술어 변환기를 이기고 죄를 짓습니다.

Leslie Lamport는 동시 프로그래밍을 위한 술어 트랜스포머로 win and sin을 제시했습니다.^[3]

술어 변환기 속성

이 절에서는 술어 변환기의 몇 가지 특징적인 속성을 제시합니다.^[4]아래에서 S는 술어 변환기(상태 공간 상에서 두 술어 사이의 함수)를 의미하고 P는 술어를 의미합니다.예를 들어, S(P)는 wp(S,P) 또는 sp(S,P)를 나타낼 수 있습니다.우리는 x를 상태 공간의 변수로 유지합니다.

모노토닉

관심 있는 술어 변환기(wp, wlp 및 sp)는 단조롭습니다.술어 변환기 S는 다음과 같은 경우에만 단조적입니다.

${\displaystyle(\모든 x:P:Q)\오른쪽 화살표(\모든 x에 대해:S(P):S(Q))}$

이 속성은 호아레 논리의 결과 규칙과 관련이 있습니다.

엄격한.

술어 변환기 S는 다음과 같은 경우 엄격합니다.

${\displaystyle S({\texttt {F}})\\좌측 화살표 \{\texttt {F}}$

예를 들어 wp는 인위적으로 엄격한 반면 wlp는 일반적으로 그렇지 않습니다.특히, 문장 S가 종료되지 않으면 ${\displaystyle \mathrm{wlp}}$(${\displaystyle S,}$ ${\displaystyle F)}$ ${\displaystyle wlp ($S, ${\textt {F})}$가 충족됩니다.우리는 가지고 있다.

${\displaystyle wlp({\texttt {where}})\{\texttt {true}}\{\texttt {do}}\{\texttt {done}}, {\texttt {F}}\\\texttt {T}}\\texttt {t}}$

실제로 T는 해당 루프의 유효한 불변량입니다.

엄격하지는 않지만 단조롭거나 연속적인 술어 변환기는 기적이라고 불리며 특히 다이크스트라가 덜 관심을 가졌던 프로그래밍 구문의 클래스를 정의하는 데 사용될 수도 있습니다.이러한 점프문에는 L로 직진, 루프에서 브레이크 및 계속, 절차 기관에서 리턴문, 예외 처리 등이 포함됩니다.모든 점프문은 실행 가능한 기적, ^[5]즉 실행은 가능하지만 엄격하지는 않다는 것이 밝혀졌습니다.

터미네이션

다음과 같은 경우 술어 변환기 S가 종료됩니다.

${\displaystyle S({\texttt {T}})\\좌측 화살표 \{\texttt {T}}$

실제로 이 용어는 엄격한 술어 변환기에만 적합합니다. 실제로 ${\displaystyle \mathrm{wp}(S,}$ ${\displaystyle T)}$ ${\displaystyle wp(S$, ${\texttt {T}})}$는 S의 종료를 보장하는 가장 약한 전제 조건입니다.

이 재산의 이름을 낙태금지라고 짓는 것이 더 적절할 것으로 보입니다: 완전한 정확성에서, 낙태금지는 낙태인 반면, 부분적인 정확성에서, 그렇지 않습니다.

접속성

술어 변환기 S는 다음과 같은 경우에 접속사입니다.

${\displaystyle S(P\wedge Q)\\\좌우 화살표 \S(P)\wedge S(Q)}$

이것은 문 S가 선택 문 또는 규격 문으로서 비결정적인 경우에도$$${\displaystyle \mathrm{wp}}$(${\displaystyle S,}$.${\displaystyle }$) ${\displaystyle wp (S$, $.)}$의 경우입니다.

접속사

술어 변환기 S는 다음과 같은 경우에 접속사입니다.

${\displaystyle S(P\vee Q)\\좌측 화살표 \S(P)\vee S(Q)}$

이것은 일반적으로 S가 비결정적일 때$$ ${\displaystyle \mathrm{wp}}$(${\displaystyle S,}$ ${\displaystyle .)}$ ${\displaystyle wp (S$, $.)}$의 경우가 아닙니다.실제로 임의의 부울을 선택하는 비결정론적 문장 S를 생각해 보십시오.이 문장은 여기에 다음과 같은 선택 문장으로 주어집니다.

${\displaystyle S\=\{\texttt {if}}\{\texttt {true}\rightarrow x:=0\[\!]\{\texttt {true}\rightarrow x:=1\{\texttt {fi}}$

그런 다음 ${\displaystyle \mathrm{wp}}$(${\displaystyle S,}$ R${\displaystyle }$) ${\displaystyle wp($${\displaystyle S}$$,$${\displaystyle \mathrm{R}}$$)}$가 공식 R [ $x$ ← 0 ]${\displaystyle }$∧ R${\displaystyle }$[ ${\displaystyle x}$ ← ${\displaystyle 1}$] ${\displaystyle R$[ $x\leftarrow 0]\$wedge R [ $x\leftarrow 1]}$로 줄어듭니다$.$

따라서 ${\displaystyle \mathrm{wp}}$ (${\displaystyle S,}$ ${\displaystyle \text{x}}$ = ${\displaystyle 0}$ ∨ ${\displaystyle x}$ = 1${\displaystyle }$) ${\displaystyle wp(S,\$x = $0\vee$x = 1$)}$는 tautology (${\displaystyle 0}$ = ${\displaystyle 0}$ ∧ ${\displaystyle 0}$= 1 )$$wedge${\displaystyle }$(${\displaystyle 1}$ = 0 ∨ 1 = ${\displaystyle 1}$) ${\displaystyle ($0$$=$0\vee$0 = 1$)}$

반면 공식 ${\displaystyle \mathrm{wp}}$(${\displaystyle S,}$ ${\displaystyle x}$ = ${\displaystyle 0}$ )${\displaystyle }$∨ ${\displaystyle \mathrm{wp}}$(${\displaystyle S,}$ x = 1${\displaystyle }$) ${\displaystyle wp (S,x$= $)\vewp$(${\displaystyle \mathrm{S}}$$,x$ = ${\displaystyle 1}$$)}$는 잘못된 명제$$(${\displaystyle 0}$ = ${\displaystyle 0}$ ∧ 1 = ${\displaystyle 0}$ )${\displaystyle }$∨${\displaystyle }$(${\displaystyle 1}$ = ${\displaystyle 0}$ ∧ ${\displaystyle 1}$ = 1${\displaystyle }$) ${\displaystyle ($0$$=$0\$wedge$$1$$=$0)\ve ($1$$=$0\$wedge 1 = 1$)}$로 줄어듭니다$.$

적용들

• 가장 약한 전제 조건의 계산은 주로 정리 증명자(SMT 해결사 또는 증명 보조자 등)를 사용하여 프로그램에서 주장을 정적으로 확인하는 데 사용됩니다. Frama-C 또는 ESC/Java2 참조.
• 다른 많은 의미 형식주의와 달리 술어 변환기 의미론은 계산의 기초에 대한 조사로 설계되지 않았습니다.오히려 프로그래머들이 프로그램을 "계산 방식"으로 "구성에 의한 올바른" 것으로 개발하는 방법론을 제공하고자 했습니다.이 "톱다운" 스타일은 Dijkstra와^[6] N에 의해 주장되었습니다. 워스.^[7]R.-J. 백과 다른 사람들에 의해 더 공식화되었습니다.B-Method와 같은 일부 도구는 이 방법론을 촉진하기 위해 자동화된 추론을 제공합니다.
• 호아레 논리학의 메타 이론에서, 약한 전제 조건은 상대적 완전성의 증명에서 핵심 개념으로 나타납니다.^[8]

술어 변환기 이상

명령식의 가장 약한 전제조건과 가장 강한 사후조건

술어 트랜스포머 의미론에서 표현은 논리의 용어로 제한됩니다(위 참조).그러나 이 제한은 대부분의 기존 프로그래밍 언어에 너무 강력한 것 같습니다. 식에 부작용이 있을 수 있고(부작용이 있는 함수를 호출) 종료 또는 중단되지 않을 수 있습니다(0으로 나누는 것처럼).명령형 표현 언어와 특히 모나드에 대해 가장 약한 전제 조건 또는 가장 강한 사후 조건을 확장하려는 많은 제안이 있습니다.

그 중 호아레 유형론은 하스켈과 같은 언어, 분리 논리, 유형론에 호아레 논리를 결합한 것입니다.^[9]이 시스템은 현재 Ynot이라는 Coq 라이브러리로 구현되어 있습니다.^[10]이 언어에서 식의 평가는 가장 강한-사후 조건의 계산에 해당합니다.

확률적 술어 변환기

확률적 술어 변환기는 확률적 프로그램을 위한 술어 변환기의 확장입니다.실제로 이러한 프로그램은 암호학(일부 무작위 잡음을 이용한 정보 숨기기), 분산 시스템(대칭 파괴)에 많은 응용 프로그램을 가지고 있습니다.

참고 항목

• 공리적 의미론 - 술어 변환기 의미론 포함
• 동적 논리 - 술어 변환기가 모달리티로 나타나는 경우
• 프로그래밍 언어의 공식적 의미론 - 개요

메모들

참고문헌