![Previous page: Specification with preconditions and postconditions [Section] -- Keyboard shortcut: 'p'](./images/nav-left.gif "Previous page: Specification with preconditions and postconditions [Section] -- Keyboard shortcut: 'p'")
| | Contracts and Assertions - slide 6 : 32 |
A logical expression is an expression of type boolean
An assertion is a logical expression, which, if false, indicates an error [Foldoc]
A precondition of an operation is an assertion which must be true just before the operation is called
A postcondition of an operation is an assertion which must be true just after the operation has been completed