Cited By
View all- Reus BCharlton NHorsfall B(2018)Symbolic Execution Proofs for Higher Order Store ProgramsJournal of Automated Reasoning10.1007/s10817-014-9319-854:3(199-284)Online publication date: 28-Dec-2018
Verifying the reflective visitor pattern
Pages 27 - 34
Abstract
Computational reflection allows a program to inspect and manipulate the structure or behaviour of itself at runtime. Often this means that it is possible to create more generic or adaptable programs in an elegant way. However, there is little support for specification and automatic verification of reflective programs. We address this problem by implementing, specifying, and verifying a reflective library using a Hoare-logic for a simple language with stored procedures. The latter is important since reflective metadata is modelled on the heap, thus method objects will be realised as stored procedures. We verify memory safety as well as functional correctness of an instance of the reflective visitor pattern, including the reflective library. The entire verification is carried out in our (semi-)automatic verification tool Crowfoot.
References
[1]
The Crowfoot website, 2011. www.sussex.ac.uk/informatics/crowfoot.
[2]
Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, pages 115--137, 2005.
[3]
Jeremy Blosser. Java tip 98: Reflect on the visitor design pattern. JavaWorld, 2000. http://www.javaworld.com/javaworld/javatips/jw-javatip98.html.
[4]
Nathaniel Charlton, Ben Horsfall, and Bernhard Reus. Crowfoot: A verifier for higher-order store programs. In VMCAI, volume 7148 of Lecture Notes in Computer Science, pages 136--151. Springer, 2012.
[5]
Cristina David and Wei-Ngan Chin. Immutable specifications for more concise and precise verification. In OOPSLA, pages 359--374, 2011.
[6]
Dino Distefano and Matthew J. Parkinson. jStar: towards practical verification for Java. In OOPSLA, pages 213--226, 2008.
[7]
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In PLDI, pages 234--245, 2002.
[8]
Erich Gamma, Richard Helm, Ralph E. Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading, MA, 1995.
[9]
Christopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster, and Jeffrey S. Foster. Specifying and verifying the correctness of dynamic software updates. In Proceedings of the International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), January 2012.
[10]
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods, pages 41--55, 2011.
[11]
Gary Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, Daniel Zimmerman, and Werner Dietl. JML reference manual (draft v1.235). Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org, July 2008.
[12]
Jens Palsberg and C. Barry Jay. The essence of the visitor pattern. In COMPSAC, pages 9--15, 1998.
[13]
Matthew J. Parkinson and Gavin M. Bierman. Separation logic, abstraction and inheritance. In POPL, pages 75--86, 2008.
[14]
John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002.
[15]
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang. Nested Hoare triples and frame rules for higher-order store. In CSL, pages 440--454, 2009.
[16]
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, and Hongseok Yang. Nested Hoare triples and frame rule for higher-order store. Logical Methods in Computer Science, 7(3), September 2011.
Index Terms
- Verifying the reflective visitor pattern
Recommendations
Verifying executable object-oriented specifications with separation logic
ECOOP'10: Proceedings of the 24th European conference on Object-oriented programmingSpecifications of Object-Oriented programs conventionally employ Boolean expressions of the programming language for assertions. Programming errors can be discovered by checking at runtime whether an assertion, such as a precondition or class invariant, ...
Verifying higher-order functional programs with pattern-matching algebraic data types
POPL '11Type-based model checking algorithms for higher-order recursion schemes have recently emerged as a promising approach to the verification of functional programs. We introduce pattern-matching recursion schemes (PMRS) as an accurate model of computation ...
Verifying higher-order functional programs with pattern-matching algebraic data types
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesType-based model checking algorithms for higher-order recursion schemes have recently emerged as a promising approach to the verification of functional programs. We introduce pattern-matching recursion schemes (PMRS) as an accurate model of computation ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
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
- AITO: Assoc Internationale por les Technologies Objects
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 12 June 2012
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
ECOOP'12
Sponsor:
- AITO
Acceptance Rates
Overall Acceptance Rate 51 of 75 submissions, 68%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 133Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View all- Reus BCharlton NHorsfall B(2018)Symbolic Execution Proofs for Higher Order Store ProgramsJournal of Automated Reasoning10.1007/s10817-014-9319-854:3(199-284)Online publication date: 28-Dec-2018
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