Correctness formula {P} A {Q}:
The meaning of {P} A {Q}:
“Any execution of A, starting in a state where P holds, will terminate in a state where Q holds.”
P and Q are properties of the various entities involved.
A denotes an operation; P is the pre-condition that A may assume; Q is the post-condition that A must satisfy.
Correctness formulae (also called Hoare triples) are a mathematical notation, not a programming construct, that helps to express properties of software elements.
Example: {x >= 9} x := x + 5 {x >= 13} (This valid formula is not the strongest possible one.)