Property-preserving program refinement
Abstract
During the development and maintenance process, a program changes form, often being refined as specifications and implementation decisions are realized. A correctness proof built in parallel with an original program can be extended to a proof of refined program by showing equivalences between the original and refined program. This paper illustrates two examples of property-preserving refinement, partial evaluation and generalization, and explores the correctness-preserving equivalences underpinning those refinement techniques. We plan to explore ways in which the informal reasoning behind these and similar program refinement tasks may be captured to extend the proof for an original program into a proof of the refined program.
References
[1]
UVa Online Judge, Downloaded Apr. 2012. http://uva.onlinejudge.org/.
[2]
S. Abramsky. The lazy lambda calculus. In D. A. Turner, editor, Research topics in functional programming, pages 65–116. Addison-Wesley Longman, Boston, MA, USA, 1990.
[3]
R. Arnold. Software restructuring. Proceedings of the IEEE, 77(4):607 –617, Apr. 1989.
[4]
D. W. Binkley and K. B. Gallagher. Program slicing. volume 43 of Advances in Computers, pages 1 – 50. Academic Press, 1996.
[5]
R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. J. ACM, 24(1):44–67, Jan. 1977.
[6]
C. Consel and O. Danvy. Tutorial notes on partial evaluation. In POPL ’93, pages 493–501, Charleston, South Carolina, USA, 1993. ACM.
[7]
W. R. Cook and R. Lämmel. Tutorial on online partial evaluation. Information Processing Letters, 66(January):493–501, 2011.
[8]
T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms, Third Edition. The MIT Press, 3rd edition, 2009.
[9]
J. Gibbons and R. Hinze. Just do it: simple monadic equational reasoning. SIGPLAN Not., 46(9):2–14, Sept. 2011.
[10]
W. G. Griswold and D. Notkin. Automated assistance for program restructuring. ACM Trans. Softw. Eng. Methodol., 2(3):228–269, July 1993.
[11]
G. Hutton and D. Fulger. Reasoning About Effects: Seeing the Wood Through the Trees. In Trends in Functional Programming, Nijmegen, The Netherlands, May 2008.
[12]
N. D. Jones, C. K. Gomard, and P. Sestoft. Partial evaluation and automatic program generation. Prentice-Hall, Upper Saddle River, NJ, USA, 1993.
[13]
M. Kaufmann, J. S. Moore, and P. Manolios. Computer-Aided Reasoning: An Approach. Kluwer, Norwell, MA, USA, 2000.
[14]
J. Launchbury. Projection factorisations in partial evaluation. Cambridge University Press, New York, NY, USA, 1991.
[15]
T. Mens and T. Tourwe. A survey of software refactoring. IEEE Trans. on Softw. Eng., 30(2):126 – 139, Feb. 2004.
[16]
D. Michie. “memo” functions and machine learning. Nature, pages 19–22, Apr. 1968.
[17]
R. Milner. Communication and concurrency. Prentice Hall, Hertfordshire, UK, UK, 1995.
[18]
P. Norvig. Techniques for automatic memoization with applications to context-free parsing. Comput. Linguist., 17(1):91–98, Mar. 1991.
[19]
S. Ray and R. Sumners. Verification of an in-place quicksort in ACL2. In Workshop on the ACL2 Theorem Prover and Its Applications, 2002., Apr. 2002.
[20]
J. Sobel. Is Scheme faster than C?, Downloaded Apr. 2012. http://www.cs.indiana.edu/ jsobel/.
[21]
E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. J. ACM, 54(5), Oct. 2007.
[22]
The Coq Development Team. The Coq Proof Assistant: Version 8.3 pl3. Roquencourt, France, Apr. 2011. Available at http://coq.inria.fr/ downloaded Jan. 7th, 2012.
[23]
M. Weiser. Program slicing. In ICSE ’81, pages 439–449, Piscataway, NJ, USA, 1981. IEEE Press.
[24]
J. Woodcock and J. Davies. Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1996.
Index Terms
- Property-preserving program refinement
Recommendations
A Mechanized Theory of Program Refinement
Formal Methods and Software EngineeringAbstractWe present a mechanized theory of program refinement that allows for the stepwise development of imperative programs in the Coq proof assistant. We formalize a design language with support for gradual refinement and a calculus which enforces ...
A frame stack semantics for sequential Core Erlang
IFL '23: Proceedings of the 35th Symposium on Implementation and Application of Functional LanguagesWe present a small-step, frame stack style, semantics for sequential Core Erlang, a dynamically typed, impure functional programming language. The semantics and the properties that we prove are machine-checked with the Coq proof assistant. We improve on ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2012
409 pages
ISBN:9781450312042
DOI:10.1145/2351676
- General Chair:
- Michael Goedicke,
- Program Chairs:
- Tim Menzies,
- Motoshi Saeki
Copyright © 2012 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
In-Cooperation
- SIGAI: ACM Special Interest Group on Artificial Intelligence
- Universität Duisburg Essen: Universität Duisburg Essen
- TCSE: IEEE Computer Society's Tech. Council on Software Engin.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 03 September 2012
Check for updates
Author Tags
Qualifiers
- Article
Conference
ASE'12
Sponsor:
ASE'12: IEEE/ACM International Conference on Automated Software Engineering
September 3 - 7, 2012
Essen, Germany
Acceptance Rates
Overall Acceptance Rate 82 of 337 submissions, 24%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 111Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 04 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in