Object-oriented programming languages like Smalltalk-80 have a message passing mechanism that allows code to work on instances of many different types. Techniques for the formal specification of such polymorphic functions and abstract types are described, as well as a logic for verifying programs that use message passing but not object mutation or assignment. The reasoning techniques formalize informal methods based on the use of subtypes. A formal definition of subtype relationships among abstract types whose objects have no time-varying state but may be nondeterministic or incompletely specified is given. This definition captures the intuition that each instance of a subtype behaves like some instance of that type's supertypes. Specifications of polymorphic functions are written by allowing instances of subtypes as arguments. Restrictions on the way that abstract types are specified ensure that such function specifications are meaningful and do not have to be rewritten when new subtypes are specified. Verification consists of showing that the specified relation among types has certain semantic properties, that each expression's value is an instance of a subtype of the expression's type, and a proof of correctness that ignores subtyping.