 Hoare logic

A system of rules for proving Hoare triples by following a program's structure. Variable assignment, sequential composition and loops have corresponding proof obligations.