11.1. Example
Here's an operation contract for the enterItem system operation. The critical element is the postconditions ; the other parts are useful but less important.
Operation: | enterItem(itemID: ItemID, quantity: integer) |
Cross References: | Use Cases: Process Sale |
Preconditions: | There is a sale underway. |
Postconditions: |
|