Hoare Logic Notes
作者：互联网
The Hoare assignment axiom
\[\vdash \{P[E/V]\} V:=E \{P\} \]The Floyd assignment axiom
\[\vdash \{P\} V:=E \{\exist v.\ (V=E[v/V]) \wedge P[v/V]\} \]Precondition strengthening
\[\frac{\vdash P \Rightarrow P',\vdash\{P'\}C\{Q\}}{\vdash\{P\}C\{Q\}} \]Postcondition weakening
\[\frac{\vdash\{P\}C\{Q'\},\vdash Q' \Rightarrow Q}{\vdash\{P\}C\{Q\}} \]Specification conjunction
\[\frac{\vdash\{P_1\}C\{Q_1\},\vdash\{P_2\}C\{Q_2\}}{\vdash\{P_1 \wedge P_2\}C\{Q_1 \wedge Q_2\}} \]Specification disjunction
\[\frac{\vdash\{P_1\}C\{Q_1\},\vdash\{P_2\}C\{Q_2\}}{\vdash\{P_1 \vee P_2\}C\{Q_1 \vee Q_2\}} \]The sequencing rule
\[\frac{\vdash\{P\}C_1\{Q\},\vdash\{Q\}C_2\{R\}}{\vdash\{P\}C_1;C_2\{R\}} \]The derived sequencing rule
\[\frac{\vdash\{P_1\}C_1\{Q_1\},\vdash\{P_2\}C_2\{Q_2\},...,\vdash\{P_n\}C_n\{Q_n\},\vdash P \Rightarrow P_1,\vdash Q_1 \Rightarrow P_2,\vdash Q_2 \Rightarrow P_3,...,\vdash Q_n \Rightarrow Q}{\vdash\{P\}C_1;...;C_n\{Q\}} \]The conditional rule
\[\frac{\vdash\{P \wedge S\}C_1\{Q\},\vdash\{P \wedge \neg S\}C_2\{Q\}}{\vdash\{P\}\ \mathsf{IF}\ S\ \mathsf{THEN}\ C_1\ \mathsf{ELSE}\ C_2 \{Q\}} \]标签：wedge,frac,...,Notes,mathsf,vdash,Logic,Hoare,Rightarrow 来源： https://www.cnblogs.com/ErkkiErkko/p/16659659.html