Theory of Computation and Specification Over Abstract Data Types and its Applications
Abstract
In these lectures the authors sketches a theory of functions and relations that are computable and specifiable, uniformly over a class of many sorted algebras. Such a class K of algebras is a mathematical model of the semantics of software module; in particular, a module defining an abstract data type. The theory of computation, specification and verification over K has many applications; those I will describe concern the following subjects: Program specification and verification; logic programming modules and abstract data types; and synchronous concurrent algorithms and their application in hardware design. The author's research on these apparently disparate applications is part of a program based on the algebraic theory of abstract data types, that aims at the formulation and analysis of the many interesting notions of computability, specifiability, and verifiability that exist in different areas of computer science and mathematics. (KR)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 17, 1989
- Accession Number
- ADA213954
Entities
People
- John V. Tucker
Organizations
- Swansea University