  Dynamically typed object-oriented languages enable programmers to write
elegant, reusable and extensible programs. However, with the current
methodology for program verification, the absence of static type information
creates significant overhead. Our proposal is two-fold:
  First, we propose a layer of abstraction hiding the complexity of dynamic
typing when provided with sufficient type information. Since this essentially
creates the illusion of verifying a statically-typed program, the effort
required is equivalent to the statically-typed case.
  Second, we show how the required type information can be efficiently derived
for all type-safe programs by integrating a type inference algorithm into Hoare
logic, yielding a semi-automatic procedure allowing the user to focus on those
typing problems really requiring his attention. While applying type inference
to dynamically typed programs is a well-established method by now, our approach
complements conventional soft typing systems by offering formal proof as a
third option besides modifying the program (static typing) and accepting the
presence of runtime type errors (dynamic typing).
