Hoare Triple

From MetaLanguage:

BackusNaurForm is a language (method?) to formally describe the syntax of programming language constructs. It is also possible to formally describe semantics ; one way to do so is by using HoareTriples.

This sounds interesting. Would someone care to either elaborate or provide references?


The term comes from the field of AxiomaticSemantics? of programs. A Hoare triple has three parts, a precondition P, a program statement or series of statements S, and a postcondition Q. It's usually written in the form

{P} S {Q}

The meaning is "if P is true before S is executed, and if the execution of S terminates, then Q is true afterwards". Note that the triple does not assert that S will terminate; that requires a separate proof. There's a little calculus for manipulating the triples. For example, if P and Q are propositions, Q involves the program variable v, and you've proved that P implies Q[E/v] (i.e., Q with the expression E substituted for v), then you can conclude that the triple

{P} v := E {Q}

is valid. Or if you know {P} S1 {R} and {R} S2 {Q}, then you can deduce

{P} S1; S2 {Q}.

Things are pretty mechanical until you get to loops. Then you have to guess a loop invariant.

There are also other styles of programming language semantics, the main alternatives being DenotationalSemantics and OperationalSemantics?.

See http://en.wikipedia.org/wiki/Hoare_triple

EditText of this page (last edited July 20, 2005) or FindPage with title or text search