A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented\n Programs -- Extended Version --

2015/09/29 by Björn Engelmann, Engelmann, Björn, Ernst-Rüdiger Olderog +1 · 1 citation
Computer Science · #Logic, programming, and type systems #Software Engineering Research #Model-Driven Software Engineering Techniques

paper · pdf · doi:10.48550/arxiv.1509.08605

Abstract

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

Cited by

• Type Safety via Hoare Logic with Separation and Pure Types

Related

• Closing the Gap -- Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic -- Extended Version --
• Tutorial implementation of Hoare logic in Haskell
• Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications
• Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
• A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests