Issue No. 09 - September (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.58783
<p>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.</p>
theorem proving; dependent types; VERITAS/sup +/; specification logic; numerals; iterative structures; modeling; functional metalanguage; computational implementation; formal specification; iterative methods; modelling; theorem proving.
F. Hanna, M. Longley and N. Daeche, "Specification and Verification Using Dependent Types," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 949-964, 1990.