How to cook a complete Hoare logic for your pet OO language

DOI10.1007/978-3-540-30101-1_5MaRDI QIDQ5311301zbMATH OpenOpenAlexFDO

Authors Cees Pierik, Frank S. de Boer

Publication date 22 August 2005

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

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

Mathematics Subject Classification ID

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

Recommendations

• A syntax-directed Hoare logic for object-oriented programming concepts.
• A sound and complete Hoare logic for dynamically-typed, object-oriented programs
• scientific article; zbMATH DE number 3888900
• Hoare logic for Java in Isabelle/HOL
• scientific article; zbMATH DE number 3848601

Cited in

(4)

• Fifty years of Hoare's logic
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• Observable behavior of distributed systems: component reasoning for concurrent objects
• A syntax-directed Hoare logic for object-oriented programming concepts.

Describes a project that uses

Uses Software

• ESC/Java
• Eiffel

This page was built for publication: How to cook a complete Hoare logic for your pet OO language

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