Abstract
Proofs-as-programs is an approach to program synthesis involving the transformation of intuitionistic proofs of specification requirements to functional programs (see, e.g., [1, 2, 12]). Various authors have adapted the proofs-as-programs to other logics and programming paradigms. This paper presents a novel approach to adapting proofs-as-programs for the synthesis of imperativeSML programs with side-effect-free return values, from proofs in a constructive version of the Hoare logic. We will demonstrate the utility of this approach by sketching how our work can be used to synthesize assertion contracts, aiding software development according to the principles of design-by-contract [8].
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.
References
Constable, R., Mendler, N., Howe, D.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
Coquand, T.: Metamathematical Investigations of a Calculus of Constructions. In: Logic and Computer Science, pp. 91–122 (1990)
Filliâtre, J.-C.: Preuve de programmes impératifs en théorie des types. Thése de doctorat, Université Paris-Sud (July 1999)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the Association for Computing Machinery 12, 576–580 (1969)
Ireland, A., Stark, J.: The automatic discovery of loop invariants (1997)
Manna, Z., Waldinger, R.J.: The deductive synthesis of imperative LISP programs. In: National Conference on Artificial Intelligence, pp. 155–160 (1987)
Matskin, M., Tyugu, E.: Strategies of Structural Synthesis of Programs. In: Proceedings 12th IEEE International Conference Automated Software Engineering, pp. 305–306. IEEE Computer Society, Los Alamitos (1998)
Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs (1997)
Meyer, B.: Agents, iterators and introspection. Technology paper, ISE Corporation (May 2000), Available at http://archive.eiffel.com/doc/manuals/language/agent/page.html
Milner, R., Tofte, M., Harper, R.: The definition of Standard ML. MIT Press, Cambridge (1990)
Poernomo, I.: Variations on a theme of Curry and Howard: The Curry- Howard isomorphism and the proofs-as-programs paradigm adapted for imperative and structured program synthesis. Phd thesis, Monash University, Available from the author on request (2003)
Poernomo, I., Crossley, J.N.: Protocols between programs and proofs. In: Lau, K.-K. (ed.) LOPSTR 2000. LNCS, vol. 2042, p. 18. Springer, Heidelberg (2001)
Poernomo, I., Crossley, J.N.: The Curry-Howard isomorphism adapted for imperative program synthesis and reasoning. In: Downey, R. (ed.) Proceedings of the 7th and 8th Asian Logic Conferences, World Scientific, Singapore (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poernomo, I. (2004). Proofs-as-Imperative-Programs: Application to Synthesis of Contracts. In: Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2003. Lecture Notes in Computer Science, vol 2890. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39866-0_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-39866-0_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20813-6
Online ISBN: 978-3-540-39866-0
eBook Packages: Springer Book Archive