  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.
