Lecture overview -- Keyboard shortcut: 'u'  Previous page: Contracts: Obligations and Benefits -- Keyboard shortcut: 'p'  Next page: Class Invariants [Section] -- Keyboard shortcut: 'n'  Lecture notes - all slides together  Annotated slide -- Keyboard shortcut: 't'  Textbook -- Keyboard shortcut: 'v'  Alphabetic index  Help page about these notes  Course home    Contracts and Assertions - slide 17 : 32

Obligations and Benefits in Sqrt
sqrt(x: Real) -> Real

  precondition: x >= 0;

  postcondition: abs(result * result - x) <= 0.000001
- Obligation Benefit
Client Must pass a non-negative number Receives the squareroot of the input
Server Returns a number r for which r * r = x Take for granted that x is non-negative
Notice in particular the obligation of the client and the benefit of the server