CSC/ECE 517 Fall 2011/ch18 6a sc: Difference between revisions
Line 6: | Line 6: | ||
=Programming by contract= | =Programming by contract= | ||
Programming by Contract or Design by Contract (DbC) was first introduced by [http://c2.com/cgi/wiki?BertrandMeyer Bertrand Meyer], the creator of [http://c2.com/cgi/wiki?EiffelLanguage Eiffel programming language]. Although Eiffel has implemented assertions as built in DbC support, the concepts can be applied in any language. It uses [http://en.wikipedia.org/wiki/Precondition pre-conditions] and [http://en.wikipedia.org/wiki/Postcondition post-conditions] to document or programmatically assert the change in state caused by a piece of a program. [http://c2.com/cgi/wiki?DesignByContract (1)] | Programming by Contract or [http://en.wikipedia.org/wiki/Design_by_contract Design by Contract (DbC)] was first introduced by [http://c2.com/cgi/wiki?BertrandMeyer Bertrand Meyer], the creator of [http://c2.com/cgi/wiki?EiffelLanguage Eiffel programming language]. Although Eiffel has implemented assertions as built in DbC support, the concepts can be applied in any language. It uses [http://en.wikipedia.org/wiki/Precondition pre-conditions] and [http://en.wikipedia.org/wiki/Postcondition post-conditions] to document or programmatically assert the change in state caused by a piece of a program. [http://c2.com/cgi/wiki?DesignByContract (1)] | ||
==Background== | ==Background== | ||
Programming by Contract or Design by Contract (DbC) has its roots in work on [http://en.wikipedia.org/wiki/Formal_verification formal verification], [http://en.wikipedia.org/wiki/Formal_specification, formal specification] and [http://en.wikipedia.org/wiki/Hoare_logic Hoare logic]. The original contributions includes: | Programming by Contract or [http://en.wikipedia.org/wiki/Design_by_contract Design by Contract (DbC)] has its roots in work on [http://en.wikipedia.org/wiki/Formal_verification formal verification], [http://en.wikipedia.org/wiki/Formal_specification, formal specification] and [http://en.wikipedia.org/wiki/Hoare_logic Hoare logic]. The original contributions includes: | ||
* A clear metaphor to guide the design process | * A clear metaphor to guide the design process | ||
* The application to [http://en.wikipedia.org/wiki/Inheritance_%28computer_science%29 inheritance], in particular a formalism for redefinition and [http://en.wikipedia.org/wiki/Dynamic_binding_%28computer_science%29 dynamic binding] | * The application to [http://en.wikipedia.org/wiki/Inheritance_%28computer_science%29 inheritance], in particular a formalism for redefinition and [http://en.wikipedia.org/wiki/Dynamic_binding_%28computer_science%29 dynamic binding] |
Revision as of 19:34, 15 November 2011
Programming by Contract
Common programming errors
Programming by contract
Programming by Contract or Design by Contract (DbC) was first introduced by Bertrand Meyer, the creator of Eiffel programming language. Although Eiffel has implemented assertions as built in DbC support, the concepts can be applied in any language. It uses pre-conditions and post-conditions to document or programmatically assert the change in state caused by a piece of a program. (1)
Background
Programming by Contract or Design by Contract (DbC) has its roots in work on formal verification, formal specification and Hoare logic. The original contributions includes:
- A clear metaphor to guide the design process
- The application to inheritance, in particular a formalism for redefinition and dynamic binding
- The application to exception handling
- The connection with automatic software documentation
Methodology
Programming by Contract creates a contract between the software developer and software user - in Meyer's terms the supplier and the consumer.
Before enters a method or routine, a pre-condition that must be satisfied by the consumer of the routine. Each routine ends with post-conditions which the supplier guarantees to be true (if and only if the preconditions were met). Also, each class has an invariant which must be satisfied after any changes to an object represented by the class. In the other words, the invariant guarantees the object is in a valid state. (2)
DbC is a metaphor on how elements of a software system collaborate with each other, on the basis of mutual obligations and benefits. The metaphor comes from business life, where a "client" and a "supplier" agree on a "contract" which documents that:
- The supplier must provide a certain product (obligation) and is entitled to expect that the client has paid its fee (benefit).
- The client must pay the fee (obligation) and is entitled to get the product (benefit).
- Both parties must satisfy certain obligations, such as laws and regulations, applying to all contracts. (3)
Benifit
How does it work with inheritance?
Examples
Example 1
Example 2
Example 3
Summary
References
1. Cunningham & Cunningham, Inc., Design by Contract
2. University of North Carolina
3. Eiffel Software, Design by Contract
http://en.wikipedia.org/wiki/Design_by_contract
http://www.cs.usfca.edu/~parrt/course/601/lectures/programming.by.contract.html