Modelling the algebra of weakest preconditions

Master Thesis

1991

Permanent link to this Item
http://hdl.handle.net/11427/23363
Files
Rewitzky_Modelling_algebra_1991.pdf (3.12 MB)
Authors
Rewitzky, Ingrid Moira
Supervisors
Brink, Chris
Journal Title
Link to Journal
Journal ISSN
Volume Title
Publisher
Publisher

University of Cape Town

Department
Department of Mathematics and Applied Mathematics
Faculty
Faculty of Science
License
Series
Abstract
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.
Description
Keywords
Mathematics

Reference:

Rewitzky, I. 1991. Modelling the algebra of weakest preconditions. University of Cape Town.

Collections
Masters