next up previous contents
Next: Specification versus High Level Up: Comparison of Specification Languages Previous: Building Up Specifications

The Data Type Invariant

As a final point of comparison, it is instructive to consider the role of the data type invariant in VDM. When a model is built up from built-in data types, it is expected that the fit with what is desired may not be quite right. The data type invariant is there to tailor the fit, to invalidate any values of the original model that have no counterpart in the requirements.

For the algebraic approach, an understanding of the required properties of an abstract data type is often a useful prelude to identifying an appropriate collection of atomic constructors. We must be careful to create those atomic constructors which will result in exactly the set of values required. However, we may have to resort to introducing additional operations to ``constrain'' the values of a data type in the sense that the atomic constructors are too general (this idea was discussed in chapter 9 in the context of hidden (private) operations). The additional operations are constructor operations, which are defined (using axioms) in terms of atomic constructors, and which allow ``valid'' values of the data type to be constructed. Any external specification which wants to use this specification then views these additional constructors as the atomic constructors for that imported type. This means that the original atomic constructors cannot be exported with the specification and must be treated as hidden. The binary search tree of chapter 9 and the petrochemical tank of chapter 11 were two such examples.


next up previous contents
Next: Specification versus High Level Up: Comparison of Specification Languages Previous: Building Up Specifications
Lee McCluskey
2002-12-18