Abstract
Methods that query the state of a data structure often return identical or equivalent values as long as the data structure does not change. Program verification depends on this fact, but it has been difficult to specify and verify such equivalent-results methods and their callers.
This paper presents an encoding from which one can determine equivalent-results methods to be deterministic modulo a user-defined equivalence relation. It also presents a technique for checking that a query method returns equivalent results and enforcing that the result depends only on a user-defined influence set.
The technique is general, for example it supports user-defined equivalence relations based on Equals methods and it supports query methods that return newly allocated objects. The paper also discusses the implementation of the technique in the context of the Spec# static program verifier.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations (CSFW), pp. 100–114. IEEE Computer Society Press, Los Alamitos (2004)
Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 23–50 (1972)
Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A Reachability Predicate for Analyzing Low-Level Software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)
Clarke, D.G., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA. SIGPLAN Notices, vol. 37(11), pp. 292–310. ACM Press, New York (2002)
Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA. SIGPLAN Notices, vol. 33(10), pp. 48–64. ACM Press, New York (1998)
Cok, D.: Reasoning with specifications containing method calls and model fields. Journal of Object Technology 4(8), 77–103 (2005)
Darvas, Á., Leino, K.R.M.: Practical Reasoning About Invocations and Implementations of Pure Methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 336–351. Springer, Heidelberg (2007)
Darvas, Á., Müller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology 5(5), 59–85 (2006)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (March 2005)
Filliâtre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud (March 2003)
Jacobs, B.: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. PhD thesis, Katholieke Universiteit Leuven (2007)
Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)
Kiniry, J.R., Cok, D.R.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer Academic Publishers, Dordrecht (1999)
Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming 55(1–3), 185–208 (2005)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J.: JML reference manual. Dept. Comp. Sci., Iowa State University (2007), http://www.jmlspecs.org
Leino, K.R.M., Müller, P.: Object Invariants in Dynamic Contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–516. Springer, Heidelberg (2004)
Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. In: 2006 Marktoberdorf Summer School on Programming Methodology, Springer, Heidelberg (to appear, 2007), research.microsoft.com/~leino/papers.html
Naumann, D.A.: From Coupling Relations to Mated Invariants for Checking Information Flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 279–296. Springer, Heidelberg (2006)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, pp. 268–280 (2004)
Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL, pp. 247–258. ACM Press, New York (2005)
Poetzsch-Heffter, A., Müller, P.: Logical foundations for typed object-oriented languages. In: Programming Concepts and Methods (PROCOMET), pp. 404–423 (1998)
Salcianu, A., Rinard, M.: Purity and Side Effect Analysis for Java Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199–215. Springer, Heidelberg (2005)
Stevenson, D.E., Phillips, A.T.: Implementing object equivalence in Java using the template method design pattern. SIGCSE Bulletin 35(1), 278–282 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leino, K.R.M., Müller, P. (2008). Verification of Equivalent-Results Methods. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)