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 HoareTriple''s''.''

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