Note on Hoare Triple Paper
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
- The author has been the first to propose a measure to prove the program using logic and axioms. The author claims that if the compiler and hardware conform to the axioms, and the axioms have proved the correctness of the program, then we could deduce the behavior of the program with great confidence.
- By introducing the Hoare triple, programmers no longer need to depend on the use of flow charts or testing extensively. Such a measure has effectively reduced the time used to evaluate the correctness of the program. Additionally, this prevents the cost of failure of the program when being used on critical systems by catching all errors. Finally, the proof could also provide insight into why a specific result could happen given the input. This could be helpful for identifying where the error happens.
- The proof could identify and help document the machine dependent part of the program. This could be helpful while the programmer is trying to transfer a program from one system to another. Given the fact that the axioms have to be modified if a machine dependent instruction is used, then either replacing that machine dependent instruction with a machine independent instruction or documenting the modified axioms and applying this modified one on new system could prevent errors during transferring.
- The author also introduces the abstract interpretation of the program. In the proof, the author suggests that the reasoner could recognize part of the program as undefined. This could effectively reduce the size and increase the efficiency of the proof.
Cons
- The axioms do not take into account of side effects produced by the language. However, the author recognizes that the production of side effects in a high level language is not useful and not expected if the language aims to produce correct programs.
- Some languages are machine dependent. To take care of this, axioms may have to be modified and examined for each different system.
- The axioms fail to take care of the program that would not terminate due to possibly non-terminating loops and system limitations. The author proposes to include the program would successfully terminate as a precondition. This would make the proof dependent of the context of the system that the program is executing on.
- The axioms have not covered the jump instructions and pointer operations, which could make the program hard to prove. These instructions, even nowadays, could not be efficiently proved.
- The proof could be hard to carry out at the time when the paper was published since no solver or proof assistant exists at that time.