The Library
Classified algebras
Tools
Tools
Tools
Wadge, William W. (1982) Classified algebras. Coventry, UK: University of Warwick. Department of Computer Science. (Department of Computer Science Research Report). (Unpublished)
|
PDF
WRAP_cs-rr-046.pdf - Other - Requires a PDF viewer. Download (1533Kb) | Preview |
Abstract
We present a new formal system for the specification and verification of abstract data types, one which allows subtypes and polymorphism.
The new system is based on a modified notion of algebra, namely that of classified algebra. A classified algebra (our terminology) is essentially a single sorted algebra together with a classification (family of subsets) of its universe. The classification, which is not necessarily a partition, is labelled by sort (type) symbols; the subset of the universe labelled by a sort symbol s are the objects of ‘type’ s.
An assertion in the new system is either an equation, which asserts that two expressions always have the same value, or a declaration, which asserts that the value of a particular expression is always of a particular type. Equations and declarations have equal status and the rules of inference (substitution and replacement) can be applied to both.
We show that any specification (set of assertions) has an initial model, unique up to isomorphism, which we can take to be the family of data types and operations specified. The declarations in a specification act as the ‘generators’ of the types, and this principle forms the basis for an inductlon rule of inference for proving assertions about initial models.
| Item Type: | Report | ||||
|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
| Library of Congress Subject Headings (LCSH): | Algebra, Universal | ||||
| Series Name: | Department of Computer Science Research Report | ||||
| Publisher: | University of Warwick. Department of Computer Science | ||||
| Place of Publication: | Coventry, UK | ||||
| Official Date: | October 1982 | ||||
| Dates: |
|
||||
| Number: | Number 46 | ||||
| Number of Pages: | 21 | ||||
| DOI: | CS-RR-046 | ||||
| Institution: | University of Warwick | ||||
| Theses Department: | Department of Computer Science | ||||
| Status: | Not Peer Reviewed | ||||
| Publication Status: | Unpublished | ||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
