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

TL;DR

This paper introduces the first sound and complete Hoare logic tailored for reasoning about dynamically-typed, object-oriented programs, providing formal verification tools for such languages.

Contribution

It presents a novel Hoare logic specifically designed for dynamically-typed, object-oriented languages, along with a formal semantics and correctness proofs.

Findings

Hoare logic is sound and relatively complete for the language

Formal semantics and proof rules are established

First such logic for dynamically-typed languages

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.