A syntax-directed Hoare logic for object-oriented programming concepts.

DOI10.1007/B94120MaRDI QIDQ5902541zbMATH OpenOpenAlexFDO

Authors Cees Pierik, Frank S. de Boer

Publication date 12 January 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b94120

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• A proof outline logic for object-oriented programming
• A logic of object-oriented programs
• Formal Methods for Components and Objects
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs
• Hoare logic for Java in Isabelle/HOL

Cited in

(19)

• An assertion-based proof system for multithreaded Java
• Specification and verification of object-oriented programs using supertype abstraction
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs
• Fifty years of Hoare's logic
• A program logic for resources
• A proof outline logic for object-oriented programming
• scientific article; zbMATH DE number 1670750 (Why is no real title available?)
• Graph-based object-oriented Hoare logic
• WP semantics and behavioral subtyping
• Separation logic, abstraction and inheritance
• The ``Hoare Logic of CSP, and All That
• Hoare logic for Java in Isabelle/HOL
• Observable behavior of distributed systems: component reasoning for concurrent objects
• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• A logic of object-oriented programs
• Formal Methods for Components and Objects
• Algebraic Methodology and Software Technology
• rCOS: a refinement calculus of object systems
• Towards verification of C\(\#\) programs: a three-level approach

Describes a project that uses

Uses Software

• JML

This page was built for publication: A syntax-directed Hoare logic for object-oriented programming concepts.

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