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