Hoare Logic

Hoare Logic is a formalism relating the initial and terminal state of a program.

1. Hoare Triples

Where is a command, is a precondition describing the initial state and is a postcondition describing the final state:

When is executed in a state satisfying , if the execution of terminates, then the state in which it terminates satisfies .

Conditions on program variables are written using mathematical notation together with logical operators. For example . Be careful not to reuse variables.

2. Hoare Logic

Hoare Logic is a deductive proof system for hoare triples. It can be used as a semantics (set of axioms) to show properties of programs. To do this, we need the big-step WHILE language defined previously. A language for defining state predicates and its semantics (assertion language), and a formal interpretation of hoare triples with a proof system.

2.1 Assertion Language

Assertion Language is an instance of first-order logic with equality, with values as integers and assertions properties of WHILE states:

Note that can be defined as .

2.2 Semantics of Assertions

A term in a state is written as where:

Partial Correctness: For any assertions , and command :

2.3 Derivation Rules

We can now define the rules of Hoare Logic. We do not consider :

2.4 Soundness & Completeness

We now have a syntactic method for deriving Hoare triples, and a definition for there meaning:

Back to Home