- Record: found
- Abstract: found
- Article: found
A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs -- Extended Version --
Preprint
2015-09-29
Read this article at
There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.
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.