标签：wedge frac Notes mathsf vdash Logic Hoare Rightarrow
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
From： https://www.cnblogs.com/ErkkiErkko/p/16659659.html