WP semantics and behavioral subtyping

DOI10.1007/978-3-642-23283-1_12MaRDI QIDQ3105750zbMATH OpenOpenAlexFDO

Authors Yijing Liu, Zongyan Qiu, Quan Long

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

behavioral subtypingobject orientationrefinementseparation logicspecificationweakest precondition

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)

Recommendations

• scientific article; zbMATH DE number 1487496
• scientific article; zbMATH DE number 1696907
• Weakest pre-condition reasoning for Java programs with JML annotations
• A syntax-directed Hoare logic for object-oriented programming concepts.
• A logic of object-oriented programs

Cites work

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

Cited in

(2)

• scientific article; zbMATH DE number 1487496 (Why is no real title available?)
• A Representation-Independent Behavioral Semantics for Object-Oriented Components

Describes a project that uses

Uses Software

• JML
• Spec#
• ESC/Java

This page was built for publication: WP semantics and behavioral subtyping

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3105750)