SPECIFICATION AND VERIFICATION USING DEPENDENT TYPES

Dependent types are a generalization of the ordinary Cartesian product and function types which allow finer and more expressive types to be formed. In this paper the rationale for, and design of, VERITAS+, a specification logic based on dependent types, is described. The overall aim is to demonstrate how the use of dependent types together with subtypes and datatypes allows the writing of specifications that are clear, concise, and generic. As an illustration, the development of theories of arithmetic, numerals, and iterative structures is described, and the proof of a theorem that greatly simplifies the formal verification of iterative arithmetic structures is outlined. The VERITAS+ logic itself is defined by modeling it as a partial algebra within a purely functional metalanguage. Aspects of the computational implementation of the logic and its associated toolset are briefly described. © 1990 IEEE