Content deleted Content added
→Weakest preconditions: conditional |
|||
Line 15:
=== Skip ===
<math>wp(\textbf{skip},R) \ =\ R</math>
=== Abort ===
<math>wp(\textbf{abort},R) \ =\
=== Assignment ===
We give below two equivalent weakest-preconditions for the assignment statement (in these formulas, <math>R[x \leftarrow E]</math> is a copy of ''R'' where [[ Free_variables_and_bound_variables| fresh occurrences]] of ''x'' are replaced by ''E''):
* version 1:
<math> wp(x := E, R)\ =\ \forall y, y = E \Rightarrow R[y \leftarrow x]\ </math> where ''y'' is a fresh variable (representing the final value of variable ''x'').
* version 2:
Line 40:
As example:
:<math>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</math>
=== Conditional ===
<math>wp(\textbf{if}\ E\ \textbf{then}\ S_1\ \textbf{else}\ S_2\ \textbf{endif},R)\ =\ (E \Rightarrow wp(S_1,R)) \wedge (\neg E \Rightarrow wp(S_2,R))</math>
As example:
:<math>wp(\textbf{if}\ x < y\ \textbf{then}\ x:=y\ \textbf{else}\ \textbf{skip}\ \textbf{endif},\ x \geq y)\ =\ (x < y \Rightarrow wp(x:=y,x\geq y)) \wedge (\neg x<y \Rightarrow x \geq y)\ =\ (x < y \Rightarrow y\geq y)\ =\ \textbf{true}</math>
=== Weakest-preconditions of [[Guarded commands]] ===
| |||