A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs -- Extended Version --
Programming Languages
2016-01-12 v3 Logic in Computer Science
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.
Cite
@article{arxiv.1509.08605,
title = {A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs -- Extended Version --},
author = {Björn Engelmann and Ernst-Rüdiger Olderog},
journal= {arXiv preprint arXiv:1509.08605},
year = {2016}
}
Comments
Extended Version -- contains all proofs, proof rules and additional information; new version -- elaborated explanations in section 7, added reference, minor visual improvements; new version -- incorporated reviews & improved formalizations