TODO 740 Bytes
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1

2 3
o pas de old dans les invariants

4 5 6 7 8 9 10
o e <- e

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

o WP: update

o syntactic sugar for postcondition:
11 12 13 14 15
  { pat | q } stands for { let pat = result in q }

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

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

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

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

24 25 26 27 28 29
o program alias, e.g.

    let f = String.create

o library
  x Array
30 31 32
  x String
  x Buffer
  x Char
33
  - Hashtbl
34 35
  x Queue
  x Stack
36 37 38 39

  - List
  - Map
  - Set