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 and notes together  slide -- Keyboard shortcut: 't'  Textbook -- Keyboard shortcut: 'v'  Help page about these notes  Alphabetic index  Course home  Page 17 : 32
Object-oriented Programming in C#
Contracts and Assertions
Obligations and Benefits in Sqrt

sqrt(x: Real) -> Real

  precondition: x >= 0;

  postcondition: abs(result * result - x) <= 0.000001

An axiomatic specification of the squareroot function.

-ObligationBenefit
ClientMust pass a non-negative numberReceives the squareroot of the input
ServerReturns a number r for which r * r = xTake for granted that x is non-negative

A tabular presentation of the obligations and benefits of the squareroot function (in a server role) and its callers (in a client role).

Notice in particular the obligation of the client and the benefit of the server