o pas de old dans les invariants

o e <- e

o {| e with x1 = e1; ...; xn = en |}

o WP: update

o syntactic sugar for postcondition:
  { pat | q } stands for { let pat = result in q }

  particular case { x | ... } to use x instead of result
  but also { a,b | ... }, etc.

o automatically add a label pre_f at entrance of each function f

o use of old in loop invariant should be reported as an error (correctly)

o what about pervasives old, at, label, unit = ()
  in particular, how to prevent old and at from being used in programs?
  can we get rid of theories/programs.why?

o program alias, e.g.

    let f = String.create

o library
  x Array
  x String
  x Buffer
  x Char
  - Hashtbl
  x Queue
  x Stack

  - List
  - Map
  - Set