Modular verification of OO programs with interfaces
作者： Qiu Zongyan , Hong Ali , Liu Yijing
DOI: 10.1007/978-3-642-34281-3_13
关键词:
摘要: Interface types in OO languages support polymorphism, abstraction and information hiding by separating interfaces from their implementations. The separation enhances modularity of programs, however, it causes also challenges to the formal verification. Here we present a study on interface types, develop specification verification theory based our former veriJ framework. We multi-specifications for classes inherited superclass, keep modularly without re-touching verified code. concepts developed veriJ, namely abstract predicate, play important roles this extension, thus are proved widely useful very natural proofs programs.
springer.com
core.ac.uk
sci-hub.st 参考文章(24)
ECOOP 2009 - Object-Oriented Programming Lecture Notes in Computer Science. ,vol. 5653, ,(2009) , 10.1007/978-3-642-03013-0
David A. Naumann, Gary T. Leavens, Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs ,(2006)
Jan Smans, Bart Jacobs, Frank Piessens, Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic european conference on object oriented programming. ,vol. 5653, pp. 148- 172 ,(2009) , 10.1007/978-3-642-03013-0_8
Richard Helm, John Vlissides, Ralph Johnson, Erich Gamma, Design Patterns: Elements of Reusable Object-Oriented Software ,(1994)
Liu Yijing, Qiu Zongyan, A separation logic for OO programs formal aspects of component software. pp. 88- 105 ,(2010) , 10.1007/978-3-642-27269-1_6
Yoonsik Cheon, Stephen Edwards, Murali Sitaraman, Gary Leavens, Model variables: cleanly supporting abstraction in design by contract: Research Articles Software - Practice and Experience. ,vol. 35, pp. 583- 599 ,(2005) , 10.1002/SPE.V35:6
Mike Barnett, K. Rustan M. Leino, Wolfram Schulte, The Spec# Programming System: An Overview Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. ,vol. 3362, pp. 49- 69 ,(2005) , 10.1007/978-3-540-30569-9_3
Barbara H. Liskov, Jeannette M. Wing, A behavioral notion of subtyping ACM Transactions on Programming Languages and Systems. ,vol. 16, pp. 1811- 1841 ,(1994) , 10.1145/197320.197383
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, Herman Venter, Specification and verification: the Spec# experience Communications of The ACM. ,vol. 54, pp. 81- 91 ,(2011) , 10.1145/1953122.1953145
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, Shengchao Qin, Enhancing modular OO verification with separation logic Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '08. ,vol. 43, pp. 87- 99 ,(2008) , 10.1145/1328438.1328452