Paper Info
Title
Proofs-as-Imperative-Programs: Application to Synthesis of Contracts
Abstract
Proof-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 imperative SML 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].
Year
DOI
Venue
2003
10.1007/978-3-540-39866-0_13
Lecture Notes in Computer Science
Keywords
Field
DocType
design by contract,hoare logic,functional programming,programming paradigm,software development,side effect
Intuitionistic logic,Programming language,Program synthesis,Programming paradigm,Constructive,Computer science,Hoare logic,Assertion,Imperative programming,Software development
Conference
Volume
ISSN
Citations 
2890
0302-9743
3
PageRank 
References 
Authors
0.41
5
1
Name
Order
Citations
PageRank
Iman Poernomo142827.61