WP Semantics for OO Programs and Its Applications I
作者： Liu Yingjing , Qiu Zongyan
DOI:
关键词: Notation 、 Action semantics 、 Programming language 、 Soundness 、 Java 、 Formal semantics (linguistics) 、 Predicate transformer semantics 、 Operational semantics 、 Computer science 、 Object-oriented programming
摘要: 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 e orts. In this paper, su ciently large subset sequential Java with pure reference model, we define Weakest Precondition (WP) semantics, prove its soundness completeness. Based on WP specifications methods refinement relationship between specifications, propose new definitions invariants behavioral subtyping notation general OO programs.
参考文章(39)
Paulo Borba, Augusto Sampaio, Basic Laws of ROOL: an object-oriented language. Revista De Informática Teórica E Aplicada. ,vol. 7, pp. 49- 68 ,(2000)
Yijing Liu, Zongyan Qiu, Quan Long, WP Semantics and Behavioral Subtyping Theoretical Aspects of Computing – ICTAC 2011. pp. 154- 172 ,(2011) , 10.1007/978-3-642-23283-1_12
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
Paulo Borba, Augusto Sampaio, Márcio Cornélio, A Refinement Algebra for Object-Oriented Programming european conference on object-oriented programming. pp. 457- 482 ,(2003) , 10.1007/978-3-540-45070-2_20
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
J.-R. Abrial, The B-Book: Assigning Programs to Meanings ,(1996)