Graph-based object-oriented Hoare logic

DOI10.1007/978-3-642-39698-4_23MaRDI QIDQ2842647zbMATH OpenOpenAlexFDO

Authors Liang Zhao, Shu-Ling Wang, Zhiming Liu

Publication date 16 August 2013

Published in Theories of Programming and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39698-4_23

zbMATH Keywords

state graphaliasingHoare logicobject-oriented program

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Recommendations

• A logic of object-oriented programs
• A syntax-directed Hoare logic for object-oriented programming concepts.
• A proof outline logic for object-oriented programming
• A logic for information flow in object-oriented programs
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs

Cites work

• scientific article; zbMATH DE number 3550151 (Why is no real title available?)
• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• scientific article; zbMATH DE number 1390329 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• A syntax-directed Hoare logic for object-oriented programming concepts.
• An axiomatic basis for computer programming
• Graph Transformations
• Graph transformations for object-oriented refinement
• Graph-based object-oriented Hoare logic
• Refinement and verification in component-based model-driven design
• Separation logic and abstraction
• rCOS: a refinement calculus of object systems

Cited in

(3)

• A logic of object-oriented programs
• Graph-based object-oriented Hoare logic
• A graph-based generic type system for object-oriented programs

Describes a project that uses

Uses Software

• rCOS

This page was built for publication: Graph-based object-oriented Hoare logic

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