TODO 3.58 KB
Newer Older
1 2 3
WhyML
-----

Andrei Paskevich's avatar
Andrei Paskevich committed
4 5 6 7 8 9 10 11 12 13
  - currently every unhandled exception has postcondition "false".
    Should it be "true"? Should we allow unhandled exceptions at all?

  - currently we require every _global_ effect in a val/any to be
    reflected in pre/postconditions (in order to keep the symbols).
    We could produce dummy preconditions such as "r = r" for such
    effects, but the requirement seems rather reasonable.

  - should we produce the WPs for the modules loaded from loadpath?

14 15 16 17 18 19 20 21
  - should the API ensure that every psymbol resets the new regions?
    Should they be always reset at the last arrow? What if they are
    already reset at some earlier arrows, should we reset them again?

  - in "val" and "any", when a region rho is written into, but some
    subregion rho' of rho is not, should we reset rho' under rho?
    In Mlw_typing or in Mlw_expr?

22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
  - 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.

44 45 46
syntaxe
-------

47
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
48

49 50 51 52 53 54 55 56
  - infix symbols as constructors, e.g.

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

  - constants in patterns, e.g.

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

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
57

58
sémantique
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
59
----------
60

61
  - env should not contain theories under the null path.
Andrei Paskevich's avatar
Andrei Paskevich committed
62 63
    The current implementation of Typing.find_theory is potentially broken.

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

66 67 68 69 70
  - produce reparsable tasks in Why3 format: how to preserve information about
    the origins of symbols to be able to use drivers after reparsing?

  - weak memoization in transformations has a disadvantage: if a task or a decl
    is not changed by a transformation, it will stay in the hash table forever,
Andrei Paskevich's avatar
Andrei Paskevich committed
71 72
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
73
     François -- I don't get that point the weak Hashtbl that we use
74 75 76
   are designed to work on this case, even with the identity function.
   What we should do is a way to remove the task from a session when
   they are not needed anymore.
77

78 79
  - uses : pour l'instant, l'ordre des théories dans le fichier est important
    i.e. les théories mentionnées par uses doivent être définies précédemment
80

81 82
  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
    de même nom)
83

84 85 86 87 88 89
error reporting
---------------

  - 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)
90 91 92 93 94

session
-------
  - save the output of the prover
  - escape the string in the xml
François Bobot's avatar
François Bobot committed
95 96
  - the filenames in the location inside a session should be relative
   to the session_dir.
97 98 99 100 101 102 103 104

tools
-----

  - the tools should verify that the provers have the same version
   than reported in the configuration
  - Maybe : make something generic for the dialog box with memory.
  - autodetection can be modified now that only name/version/altern
105
   are taken into account in session.