TODO 4.11 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
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
22 23 24
  - the drivers cannot deal with theories defined in the .mlw files.
    Otherwise why3 would report an error. Is it acceptable?

25 26 27
WhyML
-----

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
  - 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?

Andrei Paskevich's avatar
Andrei Paskevich committed
46 47 48 49 50 51 52 53 54
  - we check the context type invariants around Eany, but not around
    Eabstr, which is rather strange. Should Eabstr have preconditions?
    If not, why should it post-ensure the invariants that didn't
    necessarily hold before its execution? Probably, we shouldn't
    add the context invariants to the outer spec of Eany.

  - and what about return/raise invariants, should Eany and Eabstr
    ensure them? (at the moment, they do)

55 56 57
  - currently every unhandled exception has postcondition "true".
    "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
58

59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
  - 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.

Andrei Paskevich's avatar
Andrei Paskevich committed
81 82
syntax
------
83

84
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
85

86 87 88 89 90 91 92 93
  - infix symbols as constructors, e.g.

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

  - constants in patterns, e.g.

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

Andrei Paskevich's avatar
Andrei Paskevich committed
94 95
semantics
---------
Andrei Paskevich's avatar
Andrei Paskevich committed
96

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

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

102 103
  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
    de même nom)
104

105 106
session
-------
Andrei Paskevich's avatar
Andrei Paskevich committed
107

108
  - save the output of the prover
Andrei Paskevich's avatar
Andrei Paskevich committed
109

110
  - escape the string in the xml
Andrei Paskevich's avatar
Andrei Paskevich committed
111

François Bobot's avatar
François Bobot committed
112
  - the filenames in the location inside a session should be relative
Andrei Paskevich's avatar
Andrei Paskevich committed
113
    to the session_dir.
114 115 116 117 118

tools
-----

  - the tools should verify that the provers have the same version
Andrei Paskevich's avatar
Andrei Paskevich committed
119 120 121
    than reported in the configuration
        Andrei: isn't this done?

122
  - Maybe : make something generic for the dialog box with memory.