Journal of Logic and Computation Advance Access originally published online on August 12, 2006
Journal of Logic and Computation 2006 16(6):841-865; doi:10.1093/logcom/exl012
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Computability in Specification
Department of Computer Science, University of Essex, Colchester, Essex CO4 3SQ, UK.
E-mail: turner{at}essex.ac.uk
| Abstract |
|---|
In reference (Foundation of specification. Journal of Logic and Computation, 15, 951974, 2005), the author introduces a core specification theory (CST) in order to provide a logical framework for the design and exploration of specification languages. In this article, we formulate two highly expressive extensions of CST. The first (CSTU) is CST + a universe of types and the second (CSTUS) permits specifications themselves to be data items. Finally, we shall explore their metamathematical properties and, in particular, provide an interpretation into first-order arithmetic.
Keywords: Data; types; specification;
-definable; conservative extensions; polymorphism