Modelling the algebra of weakest preconditions

In expounding the notions of pre- and postconditions, of termination and nontermination, of correctness and of predicate transformers I found that the same trivalent distinction played a major role in all contexts. Namely: Initialisation properties: An execution of a program always, sometimes or never starts from an initial state. Termination/nontermination properties: If it starts, the execution always, sometimes or never terminates. Clean-/messy termination properties: A terminating execution always, sometimes or never terminates cleanly. Final state properties: All, some or no final states of α from s have a given property.

Grantor dc:publisher.institution

Department of Mathematics and Applied Mathematics

Year dc:date.issued

1991

Author dc:creator

• Rewitzky, Ingrid Moira

Advisor dc:contributor.advisor

• Brink, Chris

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/11427/23363

OAI identifier oai:identifier

oai:open.uct.ac.za:11427/23363