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

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

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

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

10 11
o fmla_effect

12 13
o model types (abstract but not mutable)
  abstract types (no model)
14

15 16 17 18 19 20
o program alias, e.g.

    let f = String.create

o library
  x Array
21 22 23
  x String
  x Buffer
  x Char
24
  - Hashtbl
25 26
  x Queue
  x Stack
27 28 29 30

  - List
  - Map
  - Set