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 nonnegative number
Receives the squareroot of the input
Server
Returns a number r for which r * r = x
Take for granted that x is nonnegative
Notice in particular the obligation of the client and the benefit of the server