Data abstraction allows specifications to express program behavior in an implementation-independent way. Such abstract behavior specifications are important to support subtyping and information hiding. In languages like Eiffel, the Java Modeling Language (JML), and Spec#, where contracts are based on side-effect free expressions of the programming language, data abstraction is expressed via model fields and side-effect free methods. In this talk, I present a sound and modular verification methodology for model fields, discuss its generalization to method calls in specifications, and identify open problems for future work.