Simple Subtypes for Specification
Jonathan Edwards, Daniel Jackson and Emina Torlak
Type systems have been studied extensively for programs, but not for
specifications. This paper presents a type system for the increasingly
important class of specification languages based on first-order
constraints over relational data models, which have applications in
software modelling, architectural description, web ontologies, access
control, etc.
The system has rather a different flavour from a traditional type
system. From a users perspective, the type of an expression is nothing
more than another relational expression approximating its value.
Computationally, a type is a relation, and types are constructed from
relational operators. Type errors indicate semantic redundancies, in
which expressions could be replaced by constants without affecting the
meaning of the specification as a whole. The system supports subtypes
and union types without the need for downcasts, and a form of
overloading that decouples semantics from typing. Its simplicity, it
turns out, derives from the power and simplicity of relational join.
|