In this dissertation it is shown that abstract data types (ADTs) can be specified by the Classified Model (CM) specification language - a first-order Horn language with equality and sort "classification" assertations. It is shown how these sort assertations generalize the traditional syntactic signatures of ADT specifications, resulting in all of the specification capability of traditional equational specifications, but with the improved expressibility of the Horn-with-equality language and additional theorem proving applications such as program synthesis.
This work extends corresponding results from Many Sorted Algebra (MSA), Order Sorted Algebra (OSA) and Order Sorted Model (OSM) specification techniques by promoting their syntactic signatures to assertions in the Classified Model Specification language, yet retaining sorted quantification. It is shown how this solves MSA problems such as error values, polymorphism and subtypes in a way different from the OSA and OSM solutions. However, the CM technique retains the MSA and order sorted approach to parameterization. The CS generalization also suggests the use of CM specifications to axiomatize modules as a generalization of variables within Hoare Logic, with application to a restricted, but safe, use of procedures as state changing operations and functions as value returning operations of a module. CM proof theory and semantics are developed, including theorems for soundness, completeness and the existence of a free model.
| Identifer | oai:union.ndltd.org:uvic.ca/oai:dspace.library.uvic.ca:1828/39 |
| Date | 30 September 2005 |
| Creators | Stuart, Gordon F. |
| Contributors | Wadge, William W. |
| Source Sets | University of Victoria |
| Language | English, English |
| Detected Language | English |
| Type | Thesis |
| Format | 277832 bytes, 832518 bytes, 928455 bytes, 758389 bytes, 472750 bytes, 334212 bytes, 388286 bytes, 656434 bytes, 170772 bytes, 750651 bytes, 201649 bytes, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf, application/pdf |
| Rights | Available for World Wide Web |
Page generated in 0.0021 seconds