A sound and complete Hoare logic for dynamically-typed, object-oriented programs

DOI10.1007/978-3-319-30734-3_13MaRDI QIDQ2026792zbMATH OpenOpenAlexFDO

Authors Björn Engelmann, Ernst-Rüdiger Olderog

Publication date 20 May 2021

Full work available at URL https://arxiv.org/abs/1509.08605

zbMATH Keywords

axiomatic semanticscompleteness for total correctnessdynamic typingmultiple notions of correctnessprogram verificationpure object-orientationrelative completenesssoundnesstagged Hoare logic

Mathematics Subject Classification ID

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

Abstract: A simple dynamically-typed, (purely) object-oriented language is defined. A structural operational semantics as well as a Hoare-style program logic for reasoning about programs in the language in multiple notions of correctness are given. The Hoare logic is proved to be both sound and (relative) complete and is -- to the best of our knowledge -- the first such logic presented for a dynamically-typed language.

Recommendations

• A syntax-directed Hoare logic for object-oriented programming concepts.
• A logic of object-oriented programs
• Theorem Proving in Higher Order Logics
• Hoare-style logic for unstructured programs
• scientific article; zbMATH DE number 1670748
• A Hoare logic for SIMT programs
• The propositional dynamic logic of deterministic, well-structured programs
• A type system for logic programs
• The axiomatic semantics of programs based on Hoare's logic
• An observationally complete program logic for imperative higher-order functions

Cited in

(9)

• Graph-based object-oriented Hoare logic
• Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures
• Towards a program logic for JavaScript
• Hoare logic for Java in Isabelle/HOL
• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• A logic of object-oriented programs
• Formal Methods for Components and Objects
• A syntax-directed Hoare logic for object-oriented programming concepts.
• A generic complete dynamic logic for reasoning about purity and effects

This page was built for publication: A sound and complete Hoare logic for dynamically-typed, object-oriented programs

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