Design by Contract by Example
by Richard Mitchell and Jim McKim

Book Title Design by contract, by example
Citation Mitchell and McKim (2002)
Author Richard Mitchell and Jim McKim
Edition 1st Edition
ISBN-13 978-0201634600
Publisher Addison-Wesley
URL Amazon Google
Course CS709 - Formal Methods For Software Engineering
Instructor Dr. Fakhar Lodhi

Design by Contract is a systematic approach to specifying and implementing object-oriented software elements based on precisely defined obligations between them. This is the first practical, example-centered guide to using Design by Contract. The authors introduce powerful design principles for writing good contracts and supporting guidelines -- and demonstrate those principles with real-world Java and Eiffel code examples. They review the fundamentals of Design by Contract -- preconditions, postconditions and invariants -- and presenting a real-world example. Next, drawing on their unparalleled experience with Design by Contract, they present six powerful design principles -- each with a clear statement of goals, rationale, examples in both Java and Eiffel, and supporting notes. Developers will learn how to strengthen their components' internal support for contracts; how to use contracts to specify subclasses whose objects can safely be substituted for superclass objects; how to extend contract to specify and check properties that remain unchanged; and how to use contracts in analysis-level models. The book concludes by summarizing key principles and presenting a realistic cost/benefit analysis of their use.

Related Books:
Using Z: Specification, Refinement, and Proof
by Jim Woodcock & Jim Davies
Object-Oriented Software Construction
 by Bertrand Meyer
Program Construction and Verification
by Roland C. Backhouse
Program Construction: Calculating Implementation
by Roland Backhouse
Software Engineering
by Ian Sommerville
The Object Constraint Language, precise modeling with UML by Jos Warmer and Anneke Kleppe The Specification of Complex Systems
by B. Cohen, W. T. Harwood and M. I. Jackson