This paper describes an approach to formal development in which specifications, development steps, and proofs are expressed in a typed functional language and presented in a literate mathematical style. This approach is illustrated and discussed by the development of a revision management system. The specifications and development steps of this case study are constructed following the VDM-methodology. The proofs of the associated proof obligations have been machine-checked for correctness.
CITATION STYLE
Weber, M. (1994). Literate mathematical development of a revision management system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 873 LNCS, pp. 441–460). Springer Verlag. https://doi.org/10.1007/3-540-58555-9_109
Mendeley helps you to discover research relevant for your work.