WP Semantics and Behavioral Subtyping
作者： Yijing Liu , Zongyan Qiu , Quan Long
DOI: 10.1007/978-3-642-23283-1_12
关键词:
摘要: For the object oriented (OO) world, developing formal semantics for theoretical study and practical use is still an important topic despite of a decade's efforts. In this paper, sufficiently large subset sequential Java with pure reference model, we define Weakest Precondition (WP) semantics, prove its soundness completeness. Based on thisWP specifications methods refinement relationship between specifications, propose new definitions invariants behavioral subtyping notation general OO programs.
core.ac.uk
springer.com
sci-hub.st 参考文章(34)
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)
Gary T. Leavens, David A. Naumann, Behavioral Subtyping, Specification Inheritance, and Modular Reasoning ACM Transactions on Programming Languages and Systems. ,vol. 37, pp. 13- ,(2015) , 10.1145/2766446
Lilian Burdy, Antoine Requet, Jean-Louis Lanet, Java Applet Correctness: A Developer-Oriented Approach formal methods. pp. 422- 439 ,(2003) , 10.1007/978-3-540-45236-2_24
Matthew J. Parkinson, Alexander J. Summers, The Relationship between Separation Logic and Implicit Dynamic Frames Programming Languages and Systems. ,vol. 6602, pp. 439- 458 ,(2011) , 10.1007/978-3-642-19718-5_23
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
W. H. Hesselink, Predicate-transformer semantics of general recursion Acta Informatica. ,vol. 26, pp. 309- 332 ,(1989) , 10.1007/BF00276020
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
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
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