Hoare logic
Predicate transformer semantics
Guarded Command Language
Refinement calculus
Z notation
Specification language
Attempto Controlled English
Controlled natural language
Natural language programming
Refinement Calculus Tutorial