logic verification hoare-calculus
Definition
Hoare Triple
A Hoare triple is a construct used in Hoare calculus to describe how the execution of a piece of code changes the state of the computation. It is written as:
where:
is the precondition: an assertion that must hold before the execution of . is the command or program fragment. is the postcondition: an assertion that must hold after terminates.
Semantics
The meaning of a Hoare triple depends on whether we consider partial or total correctness.
Partial Correctness
Partial Correctness
The triple
holds under partial correctness if, whenever starts in a state satisfying and if it terminates, then the resulting state satisfies . This is often denoted as:
Total Correctness
Total Correctness
The triple
(or sometimes with explicit termination) holds under total correctness if, whenever starts in a state satisfying , it must terminate, and the resulting state satisfies .
Formal Verification
In program verification, Hoare triples are used as the building blocks for proofs. The goal is to show that a program is partially correct or totally correct with respect to its specification given by the precondition and postcondition.