Abstract
In this paper, we combine a Hoare logic with a typed λ-calculus to create a reliable tool for deriving correct programs. In this combined system proofs become part of the programs. The main advantages of our approach are (1) that the Hoare logic conforms to the de Bruijn criterion and hence, can be implemented in a reliable way; (2) that the Hoare logic and the typed λ-calculus co-exist at the same level and therefore programs do not have to be encoded within a theorem prover and (3) scopes of variables are dealt with explicitly using contexts for Hoare triples and hence, the specification language is strictly separated from the programming language.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Bibliography
Apt, K. R. ‘Ten Years of Hoare’s Logic: A Survey - Part I’. ACM Transactions on Programming Languages and Systems 3 (4), 432–483. 1981.
Barendregt, H. ‘Lambda Calculi with Types’. In: S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds.): Background: Computational Structures, Vol. 2 of Handbook of Logic in Computer Science. pp. 118–310. 1992.
Barendregt, H. and E. Barendsen, ‘Autarkic Computations in Formal Proofs’. Journal of Automated Reasoning, 28: 3, 321–336. 2002.
Filliâtre, J.-C. ‘Proof of Imperative Programs in Type Theory’. In: T. Altenkirch, W. Naraschewski, and B. Reus (eds.): Types for proofs and programs1998, Vol. 1657. 1999.
Franssen, M. ‘AP-: A Pure Type System for First Order Logic with Automated Theorem Proving’. Computing Science Report 97–15, Eindhoven University of Technology. 1997.
Franssen, M. ‘Cocktail: A Tool for Deriving Correct Programs’. Ph.D. thesis, Eindhoven University of Technology. 2000.
Franssen, M. ‘Embedding First-Order Tableaux into a Pure Type System’. In: D. Galmiche (ed.): Electronic Notes in Theoretical Computer Science, Vol. 17. 2000.
Gordon, M. J. C. Teaching hardware and software verification in a uniform frameword, Chapt. in [Hinchey, 1996]. Academic Press. 1996.
Gorelick. 1975, ‘A complete axiomatic system for proving assertions about recursive and non-recursive programs’. Technical Report 75, University of Toronto, Department of Computer Science. 1975.
Gries, D. The Science of Programming. Springer. 1981.
Gries, D. and G. Levin. ‘Assignment and Procedure Call Proof Rules’. ACM TOPLAS 2, 564-–579. 1980.
Heisel, M. ‘Formalizing and implementing Gries’ program developmentmethod in dynamic logic’. Science of Computer Programming 18, 107–137. 1992.
Hinchey, 1996] Hinchey, M. G. (ed.). Teaching and Learning Formal Methods. Academic Press. 1996.
Homeier, P. V. and D. F. Martin. ‘A Mechanically Verified Verification Condition Generator’. The Computer Journal 38 (2), 131 - 141. 1995.
Homeier, P. V. and D. F. Martin. ‘Mechanical Verification of Mutually Recursive Procedures’. In: M. McRobbie and J. Slaney (eds.): Automated Deduction CADE-13. pp. 201–215. 1996.
Kleymann, T. ‘Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs’. Ph.D. thesis, University of Edinburgh. 1998.
Nielson, H. R. and F. Nielson. Semantics with Applications: A Formal Introduction, Wiley Professional Computing. Wiley. 1992.
Oostdijk, M. and H. Geuvers. ‘Proof by Computation in the Coq system’. Theoretical Computer Science 272 (1-2), 293–314. Special Issue on the MSJ regional workshop on Theories of Types and Proofs (TTP’97), Tokyo, Japan. 2002.
Reif, 2000] Reif, W. ‘The Karlsruhe Interactive Verifier’. 2000. In: URL: http://www.informatik.uni-augsburg.desvt/fmg/
Reps, T. W. and T. Teitelbaum. The Synthesizer Generator, A System for Constructing Language-Based Editors, Texts and Monographs in Computer Science. Springer-Verlag. 1989.
von Wright, J. ‘Program Refinement by Theorem Prover’. In: D. Till (ed.): 6th Refinement Workshop. pp. 121–150. 1994.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Franssen, M. (2003). Hoare Logic with Explicit Contexts. In: Kamareddine, F.D. (eds) Thirty Five Years of Automating Mathematics. Applied Logic Series, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0253-9_6
Download citation
DOI: https://doi.org/10.1007/978-94-017-0253-9_6
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6440-0
Online ISBN: 978-94-017-0253-9
eBook Packages: Springer Book Archive