Specification and verification using dependent types

Abstract

VERITAS/sup +/, 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. 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/sup +/ logic 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.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>