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