On type checking in VDM and related consistency issues

Abstract

The variants of specification languages used with the Vienna Development Method (VDM) offer a rather expressive notion of types. Higher order function types, recursively defined types, and a notion of union types which does not require injection and projection are all included, not to mention subtypes characterized by arbitrary predicates. Besides this, VDM specifications are in general not executable so dynamic type checking does not make sense. However, proof of their total consistency (satisfiability), as advocated by Cliff Jones [5], covers all type checking including what is usually considered “dynamic”, e.g. index range checks. In addition, it ensures other desirable properties such as termination of recursively defined functions. In this paper, we identify a number of general problems concerning automatic type checking of VDM specifications and the relation to consistency proofs. The authors are currently investigating different ways of handling the problems and the presentation includes outlines of some of these.