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

DOI10.1007/978-3-319-30734-3_13zbMATH Open1475.68085arXiv1509.08605OpenAlexW2347161843MaRDI QIDQ2026792

Ernst-Rüdiger Olderog, Björn Engelmann

Publication date: 20 May 2021

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.

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

zbMATH Keywords

soundnessrelative completenessaxiomatic semanticsprogram verificationdynamic typingcompleteness for total correctnessmultiple notions of correctnesspure object-orientationtagged Hoare logic

Mathematics Subject Classification ID

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

Related Items (1)

Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures

Recommendations

• Title not available (Why is that?) 👍 👎
• An observationally complete program logic for imperative higher-order functions 👍 👎
• The axiomatic semantics of programs based on Hoare's logic 👍 👎
• The propositional dynamic logic of deterministic, well-structured programs 👍 👎
• Hoare-style logic for unstructured programs 👍 👎
• A Hoare Logic for SIMT Programs 👍 👎
• Verification: Theory and Practice 👍 👎
• Theorem Proving in Higher Order Logics 👍 👎
• A type system for logic programs 👍 👎
• Formal Methods for Open Object-Based Distributed Systems 👍 👎

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)