Completeness is a semantic non-operational notion of program correctness suggested (but not pursued) by W.W.Wadge. Program verification can be simplified using completeness, firstly by removing the approximation relation from proofs, and secondly by removing partial objects from proofs. The dissertation proves the validity of this approach by demonstrating how it can work in the class of metric domains. We show how the use of Tarski's least fixed point theorem can be replaced by a non-operational unique fixed point theorem for many well behaved Programs. The proof of this theorem is also non-operational. After this we consider the problem of deciding what it means f or a function to be "complete". It is shown that combinators such as function composition are not complete, although they are traditionally assumed to be so. Complete versions for these combinators are given. Absolute functions are proposed as a general model for the notion of a complete function. The theory of mategories is introduced as a vehicle for studying absolute functions.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:370640 |
| Date | January 1985 |
| Creators | Matthews, S. G. |
| Publisher | University of Warwick |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://wrap.warwick.ac.uk/60775/ |
Page generated in 0.0016 seconds