TODO 5.91 KB
Newer Older
1

Andrei Paskevich's avatar
Andrei Paskevich committed
2 3 4 5 6 7 8 9 10 11 12 13 14
library/gallery migration
-------------------------

  - check that examples/tests/cvc4-models.mlw can use arrays
    instead of ref map (commit dfc90d)

  - remove the temporary --type-only from bench/bench (commit 02be08f)

  - DISCUSS: why3 prove theories/int.why fails because of a "variant"
    clause in one of let functions: this clause requires int.Int
    for the order relation, which is not loaded automatically
    (program modules are expected to do "use import int.Int")
    and, of course, cannot be used explicitly inside int.why.
15 16 17 18 19 20 21 22 23 24 25 26 27 28

  - expression { e with f2 = e2 } is syntactic sugar for
    { f1 = e.f1; f2 = e2; f3 = e.f3 }
    We would get better error messages if we would produce instead
    { f2 = e2; f1 = e.f1; f3 = e.f3 }
    that is, with user-given fields first, then fields from e
    See for instance bench/programs/bad-typing/with1.mlw

  - the error message for
      val foo (_x : int) : int
      val f (x:int) : unit writes { foo.contents }
    is "unbound symbol 'foo'", which is not correct
    (is should rather be that "foo" has the wrong type)

Andrei Paskevich's avatar
Andrei Paskevich committed
29
  - bench/programs/bad-to-keep/{at1.mlw,old2.mlw}
30 31
    should at least produce a warning (meaningless 'old')

32 33 34
  - no warning on lemma functions
    cf examples/tests/lemma_functions.mlw

Andrei Paskevich's avatar
Andrei Paskevich committed
35 36 37
  - "old" and "at" in program code gives a syntax error
    (bench/programs/bad-to-keep/old3.mlw), we can do better

38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
docs
----

  - rename the languages to "Why" and "WhyML". "Why3ML" is a horrible name.

generic
-------

  - let modules register new command-line options. This would deprecate
    the "stop flags" in Debug, and serve, for instance, for --type-only,
    --parse-only, ocaml code extraction, printing of modules, etc.

  - introduce a dedicated buffer-backed formatter for warnings.
    The contents of the buffer would be shown on stdout or in a window
    at selected points of program execution. Demote non-critical errors
    (e.g. unnamed type variables) to warnings.

  - should we create a common [exception Why.Error of exn] to facilitate
    integration of the library? This would require a special [raise] call:
        why_raise e = raise (Why.Error e)

Andrei Paskevich's avatar
Andrei Paskevich committed
59 60 61
  - the drivers cannot deal with theories defined in the .mlw files.
    Otherwise why3 would report an error. Is it acceptable?

62 63 64
WhyML
-----

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
  - introduce logic predicates for program type invariants:
      predicate <type_name>_invariant (result : <type_name>) = ...
    Should this be just the top invariant, as written by the user,
    or should we also include the invariants for the fields?

  - allow to specify type invariants below a type definition,
    provided there are no program declarations in between.
    This allows us to define auxiliary logical functions and
    predicates that depend on the (pure) type and can be used in
    the invariant. However, the parser must know from the start
    that the type has an invariant, what's the best syntax?

  - type invariants are now assumed/asserted at the function call
    boundaries. We can add a binary flag to Ityapp to allow open
    types in function signatures (must be careful with reg_match!).
    The type cast can then play the role of the "close" instruction.
    Do we need it? What's the good syntax for open types?

83 84 85 86 87
  - we check the context type invariants around Eany and after Eabstr.
    It might be strange that Eabstr post-ensures the invariants that
    didn't necessarily hold before its execution. Also, what about
    return/raise invariants, should Eany and Eabstr enforce them?
    (at the moment, they do)
Andrei Paskevich's avatar
Andrei Paskevich committed
88

89
  - currently every unhandled exception has the postcondition "true".
90 91
    "false" would be a poor choice, as it could introduce inconsistency
    in the WPs of the caller. Should we allow unhandled exceptions at all?
Andrei Paskevich's avatar
Andrei Paskevich committed
92

93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
  - current WP does not respect the lexical scope. In the program

      let r = create 0 in
      let v = !r in
      incr r;
      let () =
        let v = !r in
        ()
      in
      assert { v = 1 }

    the last assert will be proven if the same let_defn [let v = !r]
    and therefore the same pvsymbol v is used in both places (which
    can be done using API). One possible solution is to ensure the
    one-time usage of let_defns and rec_defns in programs.

  - are mutable values worth it? They can only appear as pattern
    variables standing for mutable fields, and allow us to have
    mutable fields in algebraic types. On the other hand, they
    require tedious checks pretty much everywhere in the code,
    and they cannot be translated to OCaml.

115 116 117
  - accept match e1 with pat -> e2 end as non-ghost when e1 is ghost
    and e2 is not ghost

118 119
syntax
------
120

121
  - open
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
122

123 124 125 126 127 128 129 130
  - infix symbols as constructors, e.g.

       type list 'a = Nil | (::) 'a (list 'a)

  - constants in patterns, e.g.

       match ... with 0 :: r -> ... | ...

131 132
semantics
---------
Andrei Paskevich's avatar
Andrei Paskevich committed
133

Andrei Paskevich's avatar
Andrei Paskevich committed
134 135
  - should split_goal provide a "right-hand side only split"?

136 137 138
  - produce reparsable tasks in Why3 format: how to preserve information about
    the origins of symbols to be able to use drivers after reparsing?

139 140
  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
    de même nom)
141

142 143
session
-------
144

145
  - save the output of the prover
146

147
  - escape the string in the xml
148

François Bobot's avatar
François Bobot committed
149
  - the filenames in the location inside a session should be relative
150
    to the session_dir.
151

152 153
  - use the new restore_path for the metas in session?

154 155 156 157
tools
-----

  - the tools should verify that the provers have the same version
158 159 160
    than reported in the configuration
        Andrei: isn't this done?

161
  - Maybe : make something generic for the dialog box with memory.
162 163


164 165 166 167 168 169
OCaml extraction
----------------

  - allow other realizations for arithmetic, such as Zarith or GMP
    (currently this is Num)

170 171 172 173 174
  - avoid conversion to/from int in the for-loop

  - driver
    - %Exit -> Pervasives.Exit

175 176 177 178 179 180
provers
-------

  - PVS: use a better name for PVS theory when printing a task, e.g.
    file_theory_goal. Solution: do that when we have idents with origin
    information (necessary for parsing a task).