Abstract
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.
This work was supported by a scholarship from the Deutsche Forschungsgemeinschaft and earried out while the author was staying at the Massachusetts Institute of Technology as a visiting scientist
Preview
Unable to display preview. Download preview PDF.
References
J. R. Abrial. The B-Tool (Abstract). In R. Bloomfield, L. Marshall, and C. Jones, editors, VDM'88 — The Way Ahead. Springer-Verlag, 1988.
M. Anlauff. Devil: Deva's Interactive Laboratory. Tutorial and User Manual. Technical Report 93-42, TU Berlin, 1993.
M. Anlauff. A Support Environment for a Generic Devlopment Language. Forthcoming dissertation., TU Berlin, 1994.
M. Anlauff, S. Jälmichen, and M. Simons. A support system for formal mathematical reasoning. In T. Denvir, editor, Formal Methods Europe' 94, LNCS. Springer-Verlag, 1994.
D. Bert and C. Lafontaine. Integration of semantical verification conditions in a specification language definition. In Proceedings of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST '91, Workshops in Computing. Springer-Verlag, 1992.
M. Biersack, R. Raschke, and M. Simons. The DevaWEB system: Introduction, tutorial, user manual, and implementation. Technical Report 93–39, TU Berlin, 1993.
R. Bird. Lectures on constructive functional programming. In M. Broy, editor, Constructive Methods in Computer Science, volume F69 of NATO ASI Series, pages 151–216. Springer-Verlag, 1989.
M. Broy and C. B. Jones, editors. Programming Concepts and Methods. North Holland, 1990.
T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.
N. G. de Bruijn. A survey of the project AUTOMATH. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 579–606. Academic Press, 1980.
R. Gabriel. Program transformation expressed in the Deva meta-calculus. In Proceedings of the IFIP TC2 Working Conference on Constructing Programs from Specifications, 1991.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proof and Types. Cambridge University Press, 1989.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
D. Gries and F. B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.
J.C.Bicarregui, J.S. Fitzgerald, P.A.Lindsay, R. Moore, and B.Ritchie. Proof in VDM: A Practitioner's Guide. Springer-Verlag, 1994.
C. B. Jones. Systematic Software Development using VDM, second edition. Prentice Hall, 1990.
C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. Mural: A Formal Development Support System. Springer, 1991.
D. Knuth. Literate programming. The Computer Journal, 27(2):97–111, May 1984.
D. Knuth. Literate Programming. Center for the Study of Language and Information, 1992.
C. Lafontaine. Formalization of the VDM reification in the Deva meta-calculus. In Broy and Jones [8], pages 333–368.
C. Lafontaine, Y. Ledru, and P. Schobbens. Two approaches towards the formalisation of VDM. In D. Bjorner, C. Hoare, and H. Langmaack, editors, Proceedings of VDM'90: VDM and Z, volume 428 of LNCS, pages 370–398. Springer, 1990.
Andreas Lampen. Advancing files to attributed software-objects. In Procceedings of the Winter 1991 USENIX Conference, pages 219–229, Berkeley (CA), January 1991. USENIX Association.
L. Meertens. Algorithmics: Towards programming as a mathematical activity. In J. W. de Bakker, M. Hazewinkel, and J. K. Lenstra, editors, Proceedings of the CWI Symposium on Mathematics and Computer Science, volume 1, pages 289–334. North Holland, 1986.
C. Morgan and B. Sufrin. Specification of the unix filing system. IEEE Transactions of Software Engineering, SE-10(2):128–140, March 1984.
M.Weber. Development of a revision management system, research report, TU-Berlin, 1993.
R. P. Neclerpelt. Strong Normalization in a typed lambda calculus with lambda structured types. PhD thesis, Technical University of Eindhoven, 1973.
L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, 1989.
M. Simons, M. Biersack, and R. Raschke. Literate and structured presentation of formal proofs. In E.-R. Olderog, editor, IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94). North Holland, 1994.
W. F. Tichy. Res — A System for Version Control. Software — Practice and Experience, 15(7):637–654, July 1985.
M. Weber. Formalization of the Bird-Meertens algorithmic calculus in the Deva metacalculus. In Broy and Jones [8], pages 201–232.
M. Weber. Deriving transitivity of VDM reification in the Deva meta-calculus. In S. Prehn and W. J. Toetenel, editors, VDM'91 Formal Software Development Methods, volume 551 of LNCS, pages 406–427. Springer, 1991.
M. Weber. Definition and basic properties of the Deva meta-calculus. Formal Aspects of Computing, 5:391–431, 1993.
M. Weber, M. Simons, and Ch. Lafontaine. The Generic Development Language Deva: Presentation and Case Studies, volume 738 of LNCS. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Weber, M. (1994). Literate mathematical development of a revision management system. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_109
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_109
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive