Abstract
Math∫pad is a document preparation system designed and developed by the authors and oriented towards the calculational construction of programs. PVS (Prototype Verification System) is a theorem checker developed at SRI that has been extensively used for verifying software, in particular in safety-critical applications. This paper describes how these two systems have been combined into one. We discuss the potential benefits of the combination seen from the viewpoint of someone wanting to use formal methods for the construction of computer programs, and we discuss the architecture of the combined system for the benefit of anyone wanting to investigate combining the Math∫pad system with other programming tools.
Research supported by the Dutch Organisation for Scientific Research (NWO) under contract SION 612-14-001.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. Anderson, M. Goldsmith, B. Scattergood, and T. Teitelbaum. An environment for intergrating formal methods tools. In Bertot [7]. See also: http://www.grammatech.com/papers/uitp.html.
Myla Archer, Constance Heitmeyer, and Steve Sims. TAME: A PVS interface to simplify proofs for automata models. In Backhouse [4], pages 147–156. See also: http://www.win.tue.nl/cs/ipa/uitp/papers/Archer.ps.gz.
R.C. Backhouse. Archive of the mathematics of program construction group. Available online at http://www.win.tue.nl/cs/wp/papers/, July 1998.
R.C. Backhouse, editor. Workshop on User Interfaces for Theorem Provers, Computing Science Reports, July 1998. International Workshop, see also http://www.win.tue.nl/cs/ipa/uitp/proceedings.html.
R.C. Backhouse, R. Verhoeven, and O. Weber. Math≀pad: A system for on-line preparation of mathematical documents. Software-Concepts and Tools, 18: 80–89, 1997. See also: http://www.win.tue.nl/cs/wp/mathspad/.
Roland Backhouse and Richard Verhoeven. Math∫pad Ergonomic Document Preparation, version 0.60 edition, February 1996. Manual of the Math∫pad system. See also: http://www.win.tue.nl/cs/wp/mathspad/.
Yves Bertot, editor. Workshop on User Interfaces for Theorem Provers, September 1997. International Workshop, see also http://www-sop.inria.fr/croap/ events/uitp97-papers.html.
Eerke Boiten, John Derrick, Howard Bowman, and Maarten Steen. Consistency and refinement for partial specification in z. In Marie-Claude Gaudel and James Woodcock, editors, FME’ 96: Industrial Benefit and Advances in Formal Methods, volume 1051 of LNCS, pages 287–306. Springer, 1996.
Bettina Buth. Operation Refinement Proofs for VDM-like Specifications. PhD thesis, Institute of Computer Science and Practical Mathematics of the Christian-Albrechts-University Kiel, February 1995. See also: http://www.informatik. uni-bremen.de/~bb
Ingo Dahn. Using ILF as an interface to many theorem provers. In Backhouse [4], pages 75–86. See also: http://www.win.tue.nl/cs/ipa/uitp/papers/Dahn.ps.gz.
E.W. Dijkstra and C.S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag, Berlin, 1990.
D.E. Knuth. Literate programming. Computer Journal, 27(2):97–111, 1984.
N.A. Merriam and M.D. Harrison. What is wrong with GUIs for theorem provers. In Bertot [7]. See also: http://www.cs.york.ac.uk/~nam/uitp97.ps.gz
S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993. See also: http://pvs.csl.sri.com/.
Lawrence C. Paulson. Isabelle: a Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer, Berlin, 1994.
Darren Redfern. The Maple Handbook. Springer, 1996.
John Rushby. What is pvs? Available online at http://pvs.csl.sri.com/ whatispvs.html, November 1998. Contains a description of PVS.
Frits D. Schalij. Tangram manual. Technical Report UR 008/93, Philips Electronics N.V., 1996.
Martin Simons. Proof presentation for Isabelle. In Elsa Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs’ 97, volume 1275 of Lecture Notes in Computer Science, pages 259–274, Murray Hill, NJ, August 1997. Springer-Verlag.
Bernard Sufrin and Richard Bornat. User interfaces for generic proof assistants part II: Displaying proofs. In Backhouse
Matteo Vaccari. Calculational Derivation of Circuits. PhD thesis, Dipartimento di Informatica, Università degli Studi di Milano, May 1998. See also: http:// dotto.usr.dsi.unimi.it/~matteo/tesi.ps.gz
Stephen Wolfram. The Mathematica Book. Cambridge University Press, third edition, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag
About this paper
Cite this paper
Verhoeven, R., Backhouse, R. (1999). Interfacing program construction and verification. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_10
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive