Difference between revisions of "OCL"
From Suhrid.net Wiki
Jump to navigationJump to searchLine 20: | Line 20: | ||
* And the implementer doesn't need to worry about cases where the precondition is not true. | * And the implementer doesn't need to worry about cases where the precondition is not true. | ||
[TODO] : How about handling errors for invalid preconditions ? | [TODO] : How about handling errors for invalid preconditions ? | ||
− | + | * So a contract can be many things: | |
+ | ** A specification of what a method should do | ||
+ | ** Documentation - more precise than class interfaces [TODO : e.g. ] | ||
+ | ** Offers runtime checks for correctness. | ||
+ | ** Are a basis for testing. | ||
+ | ** Are a basis for formal proofs of programs correctness. | ||
[[Category:OODE]] | [[Category:OODE]] |
Revision as of 06:18, 30 October 2011
Introduction
- How can we express constraints in UML ?
- E.g. the balance attribute in a SavingsAccount class can never be less than zero and more than 100000.
- UML only has a notion of an informal constraint in terms of a note - which can be attached to a model. However its just text.
- To write formal and machine checkable constraints - we use the Object Constraint Language (OCL).
Assertions
- In a program, assertions express constraints on program state that must be true at a specified point during execution.
- In a model/diagram, they document what must be true of an implementation of a modelling element.
- Can have optional preconditions - (must be true when operation is invoked). for e.g. an argument to a certain operation cannot be null.
- Can have optional postconditions - (must be true when operation completes). for e.g. the operation must update the database when it completes.
Design by contract
- A pre and post condition can be viewed as a contract between an operation and its invokers.
- Something like - "If the client promises to invoke the operation with the precondition satisfied, then the operation guarantees that its implementing methods will deliver a final state in which the postcondition is true".
- So the invoker doesn't care about how final state is produced
- And the implementer doesn't need to worry about cases where the precondition is not true.
[TODO] : How about handling errors for invalid preconditions ?
- So a contract can be many things:
- A specification of what a method should do
- Documentation - more precise than class interfaces [TODO : e.g. ]
- Offers runtime checks for correctness.
- Are a basis for testing.
- Are a basis for formal proofs of programs correctness.