This paper introduces the approach, now known as the Boogie method, which form the basis of Spec#. The basic idea is a modular approach to verifying object invariants (and pre- and post-conditions) by maintaining a notion of object validity and packing and unpacking that validity in the course of checking invariants. The main motivation was to tidy up problems with DbC where objects could run into problems when calling their own public methods while their invariants didn’t hold. The modularity is a big win as well as the fact that a lot of useful things can be statically verified rather than deferring all checking until runtime (as is common in DbC). I can only hope that some of these ideas eventually see the light of day in a stack other than the one encumbered by the evil empire.