WP Semantics and Behavioral Subtyping

DOI10.1007/978-3-642-23283-1_12zbMath1351.68167OpenAlexW135120204MaRDI QIDQ3105750

Yijing Liu, Quan Long, Zong-Yan Qiu

Publication date: 6 January 2012

Published in: Theoretical Aspects of Computing – ICTAC 2011 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23283-1_12

zbMATH Keywords

refinementspecificationobject orientationseparation logicweakest preconditionbehavioral subtyping

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• JML
• Spec#
• ESC/Java

Cites Work

• rCOS: a refinement calculus of object systems
• Predicate-transformer semantics of general recursion
• Weakest pre-condition reasoning for Java programs with JML annotations
• Proof of correctness of data representations
• A proof outline logic for object-oriented programming
• The Relationship between Separation Logic and Implicit Dynamic Frames
• Separation logic, abstraction and inheritance
• Modular specification and verification of object-oriented programs