© 1977 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Generic commandsa tool for partial correctness formalisms
Department of Artificial Intelligence, University of Edinburgh, Hope Park Square, Meadow Lane, Edinburgh, UK
A semantic framework for logical formalisms based on partial correctness assertions of the form P{S}Q is given. P{S}Q asserts that if P holds before execution of S then Q holds after. Generic commands are introduced. The generic command {P=
Q} is in a sense the least specified command with precondition P and postcondition Q. Proof rules and a noneffective semantics are given for generic commands. A proof rule for recursive procedures is given using generic commands.
Received October 1975.
* Department of Artificial Intelligence, University of Edinburgh, Hope Park Square, Meadow Lane, Edinburgh EH8 9NW