Note on Hoare Triple Paper

ReviewPLSE


In the paper, the author provides a logical foundation for proving the properties of the program (i.e. whether a program has intended behavior under all specific circumstances). To simplify the process, the author introduces Hoare triple $P|Q|R$ where P is the precondition, Q is the program, and R is the assertion of the state after Q is executed.

Axiom of assignment: $\vdash P_0 \{x :=f\} P$ where $P_0$ is $P$ substituting all f with x.

Rules of Consequence: Similar to rule of inference in mathematical logic, $\vdash P \{Q\}R \wedge \vdash R \supset S \implies \vdash P\{Q\}S$ and $\vdash P \{Q\}R \wedge \vdash S \supset P \implies \vdash S\{Q\}R$. For the first one, it means, for all logic that final assertion can imply, we can replace final assertion with that logic; for the second, for all logic that precondition can be implied by, we can replace precondition with that logic.

Rules of Composition: $\vdash P \{Q_1\}R_1 \wedge \vdash R_1 \{Q_2\}R \implies \vdash P\{Q_1;Q_2\}R$. That is, if the precondition of the second triple is identical to the first final assertion, then we can combine both triples.

Rules of Composition: $\vdash P \wedge B \{S\}P \implies \vdash P \{while\ B\ do\ S\} \neg B \wedge P$. That is, for a while loop to terminate, we must have the statement B evaluated to be false. Additionally, the loop should not change the state that S has not changed.

Pros

Cons