Class-local object invariants
作者： K. Rustan M. Leino , Angela Wallenburg
关键词:
摘要: The correctness of object-oriented programs relies on object invariants. A system for verifying such requires a systematic method coping with invariants that can be violated temporarily. This paper describes sound methodology flexibly changing data locally in structures, supporting programming patterns occur frequently practice. In more detail, to handle subclasses, previous approaches have been geared toward update the fields an only overridable virtual methods object. enhanced this handles field updates much flexible way. flexibility applied common case where is not mentioned subclass
core.ac.uk
acm.org
sci-hub.se 参考文章(20)
Frank Piessens, Bart Jacobs, Verification of programs using inspector methods formal techniques for java-like programs. pp. 1- 22 ,(2006)
Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte, None, A statically verifiable programming model for concurrent object-oriented programs formal methods. ,vol. 4260, pp. 420- 439 ,(2006) , 10.1007/11901433_23
Mike Barnett, David A. Naumann, Friends Need a Bit More: Maintaining Invariants Over Shared State mathematics of program construction. pp. 54- 84 ,(2004) , 10.1007/978-3-540-27764-4_5
Ioannis T. Kassios, Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions FM 2006: Formal Methods. pp. 268- 283 ,(2006) , 10.1007/11813040_19
K. Rustan M. Leino, Peter Müller, Object Invariants in Dynamic Contexts european conference on object-oriented programming. ,vol. 3086, pp. 491- 515 ,(2004) , 10.1007/978-3-540-24851-4_22
Ádám Darvas, K. Rustan M. Leino, Practical Reasoning About Invocations and Implementations of Pure Methods Fundamental Approaches to Software Engineering. pp. 336- 351 ,(2007) , 10.1007/978-3-540-71289-3_26
K. Rustan M. Leino, Peter Müller, Modular Verification of Static Class Invariants FM 2005: Formal Methods. ,vol. 3582, pp. 26- 42 ,(2005) , 10.1007/11526841_4
Ronald Middelkoop, Cornelis Huizing, Ruurd Kuiper, Erik J. Luit, Invariants for Non-Hierarchical Object Structures Electronic Notes in Theoretical Computer Science. ,vol. 195, pp. 211- 229 ,(2008) , 10.1016/J.ENTCS.2007.08.034
David G Clarke, John M Potter, James Noble, None, Ownership types for flexible alias protection Proceedings of the 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications - OOPSLA '98. ,vol. 33, pp. 48- 64 ,(1998) , 10.1145/286936.286947
K. Rustan M. Leino, Wolfram Schulte, Using history invariants to verify observers european symposium on programming. ,vol. 4421, pp. 80- 94 ,(2007) , 10.1007/978-3-540-71316-6_7