TODO

   1
   2 library/gallery migration
   3 -------------------------
   4
   5   - check that examples/tests/cvc4-models.mlw can use arrays
   6     instead of ref map (commit dfc90d)
   7
   8   - remove the temporary --type-only from bench/bench (commit 02be08f)
   9
  10   - DISCUSS: why3 prove theories/int.why fails because of a "variant"
  11     clause in one of let functions: this clause requires int.Int
  12     for the order relation, which is not loaded automatically
  13     (program modules are expected to do "use import int.Int")
  14     and, of course, cannot be used explicitly inside int.why.
  15
  16   - expression { e with f2 = e2 } is syntactic sugar for
  17     { f1 = e.f1; f2 = e2; f3 = e.f3 }
  18     We would get better error messages if we would produce instead
  19     { f2 = e2; f1 = e.f1; f3 = e.f3 }
  20     that is, with user-given fields first, then fields from e
  21     See for instance bench/programs/bad-typing/with1.mlw
  22
  23   - the error message for
  24       val foo (_x : int) : int
  25       val f (x:int) : unit writes { foo.contents }
  26     is "unbound symbol 'foo'", which is not correct
  27     (is should rather be that "foo" has the wrong type)
  28
  29   - bench/programs/bad-to-keep/{at1.mlw,old2.mlw}
  30     should at least produce a warning (meaningless 'old')
  31
  32   - no warning on lemma functions
  33     cf examples/tests/lemma_functions.mlw
  34
  35   - "old" and "at" in program code gives a syntax error
  36     (bench/programs/bad-to-keep/old3.mlw), we can do better
  37
  38 docs
  39 ----
  40
  41   - rename the languages to "Why" and "WhyML". "Why3ML" is a horrible name.
  42
  43 generic
  44 -------
  45
  46   - let modules register new command-line options. This would deprecate
  47     the "stop flags" in Debug, and serve, for instance, for --type-only,
  48     --parse-only, ocaml code extraction, printing of modules, etc.
  49
  50   - introduce a dedicated buffer-backed formatter for warnings.
  51     The contents of the buffer would be shown on stdout or in a window
  52     at selected points of program execution. Demote non-critical errors
  53     (e.g. unnamed type variables) to warnings.
  54
  55   - should we create a common [exception Why.Error of exn] to facilitate
  56     integration of the library? This would require a special [raise] call:
  57         why_raise e = raise (Why.Error e)
  58
  59   - the drivers cannot deal with theories defined in the .mlw files.
  60     Otherwise why3 would report an error. Is it acceptable?
  61
  62 WhyML
  63 -----
  64
  65   - introduce logic predicates for program type invariants:
  66       predicate <type_name>_invariant (result : <type_name>) = ...
  67     Should this be just the top invariant, as written by the user,
  68     or should we also include the invariants for the fields?
  69
  70   - allow to specify type invariants below a type definition,
  71     provided there are no program declarations in between.
  72     This allows us to define auxiliary logical functions and
  73     predicates that depend on the (pure) type and can be used in
  74     the invariant. However, the parser must know from the start
  75     that the type has an invariant, what's the best syntax?
  76
  77   - type invariants are now assumed/asserted at the function call
  78     boundaries. We can add a binary flag to Ityapp to allow open
  79     types in function signatures (must be careful with reg_match!).
  80     The type cast can then play the role of the "close" instruction.
  81     Do we need it? What's the good syntax for open types?
  82
  83   - we check the context type invariants around Eany and after Eabstr.
  84     It might be strange that Eabstr post-ensures the invariants that
  85     didn't necessarily hold before its execution. Also, what about
  86     return/raise invariants, should Eany and Eabstr enforce them?
  87     (at the moment, they do)
  88
  89   - currently every unhandled exception has the postcondition "true".
  90     "false" would be a poor choice, as it could introduce inconsistency
  91     in the WPs of the caller. Should we allow unhandled exceptions at all?
  92
  93   - current WP does not respect the lexical scope. In the program
  94
  95       let r = create 0 in
  96       let v = !r in
  97       incr r;
  98       let () =
  99         let v = !r in
 100         ()
 101       in
 102       assert { v = 1 }
 103
 104     the last assert will be proven if the same let_defn [let v = !r]
 105     and therefore the same pvsymbol v is used in both places (which
 106     can be done using API). One possible solution is to ensure the
 107     one-time usage of let_defns and rec_defns in programs.
 108
 109   - are mutable values worth it? They can only appear as pattern
 110     variables standing for mutable fields, and allow us to have
 111     mutable fields in algebraic types. On the other hand, they
 112     require tedious checks pretty much everywhere in the code,
 113     and they cannot be translated to OCaml.
 114
 115   - accept match e1 with pat -> e2 end as non-ghost when e1 is ghost
 116     and e2 is not ghost
 117
 118 syntax
 119 ------
 120
 121   - open
 122
 123   - infix symbols as constructors, e.g.
 124
 125        type list 'a = Nil | (::) 'a (list 'a)
 126
 127   - constants in patterns, e.g.
 128
 129        match ... with 0 :: r -> ... | ...
 130
 131 semantics
 132 ---------
 133
 134   - should split_goal provide a "right-hand side only split"?
 135
 136   - produce reparsable tasks in Why3 format: how to preserve information about
 137     the origins of symbols to be able to use drivers after reparsing?
 138
 139   - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
 140     de même nom)
 141
 142 session
 143 -------
 144
 145   - save the output of the prover
 146
 147   - escape the string in the xml
 148
 149   - the filenames in the location inside a session should be relative
 150     to the session_dir.
 151
 152   - use the new restore_path for the metas in session?
 153
 154 tools
 155 -----
 156
 157   - the tools should verify that the provers have the same version
 158     than reported in the configuration
 159         Andrei: isn't this done?
 160
 161   - Maybe : make something generic for the dialog box with memory.
 162
 163
 164 OCaml extraction
 165 ----------------
 166
 167   - allow other realizations for arithmetic, such as Zarith or GMP
 168     (currently this is Num)
 169
 170   - avoid conversion to/from int in the for-loop
 171
 172   - driver
 173     - %Exit -> Pervasives.Exit
 174
 175 provers
 176 -------
 177
 178   - PVS: use a better name for PVS theory when printing a task, e.g.
 179     file_theory_goal. Solution: do that when we have idents with origin
 180     information (necessary for parsing a task).