A system of rules for proving Hoare triples by following a program's structure. Variable assignment, sequential composition and loops have corresponding proof obligations.
A partial correctness claim connecting a precondition , a program and a postcondition : every terminating execution begun with ends with . State separately whether total correctness is intended.
Articles by others on the same topic
There are currently no matching articles.