This course addresses programming disciplines for specifying and reasoning about programs in class-based languages like Java, using classical first order assertions as in JML. Disciplines help cope with challenges posed by inheritance, heap sharing, re-entrant callbacks, and design patterns that combine such features. This course focuses on the use of ghost state to express heap structure in support of flexible disciplines for encapsulation of invariants. Additional topics include the use of method calls in assertions and the use of model programs for first order reasoning about higher order methods.