Axiomatic semantics: Non-determinism

p 344
Why should one want to specify non-deterministic behavior? The are two
main reasons.

The first reason is that non-deterministic programs may be useful to
model non-deterministic behavior in the real-world.

The second reason has to do with the desire not to overspecify.


Routines and recursion:

pp 353-354
This is the idea of *programming by contract*. A routine call is a
contract to perform a certain task. The caller is the "client", the
called routine is the "supplier". As in every good contract, there are
advantages and obligations for both parties:
. The precondition is an obligation for the client; for the supplier,
  it is a benefit, since it relieves the routine body from having to
  care about cases not covered by the precondition.
. For the postcondition the situation is reversed.

p 369
Two particular embedding strategies:
- Constant relaxation
- Uncoupling