Computability in Specification
T. Raymond · Journal of Logic and Computation · 2006
In reference (Foundation of specification. Journal of Logic and Computation, 15, 951–974, 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.