TODO 3.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
WhyML
-----

  - 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?

12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
  - 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.

  - get rid of %Exit, implement unit-typed "break" and "continue",
    usable in all kinds of loops, including "for". Why the heck
    aren't these in OCaml?
37 38 39 40

syntaxe
-------

41
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
42

43 44 45 46 47 48 49 50
  - 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
51

52
sémantique
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
53
----------
54

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

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

60 61 62 63 64
  - 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
65 66
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
67
     François -- I don't get that point the weak Hashtbl that we use
68 69 70
   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.
71

72 73
  - 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
74

75 76
  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
    de même nom)
77

78 79 80 81 82 83
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)
84 85 86 87 88

session
-------
  - save the output of the prover
  - escape the string in the xml
François Bobot's avatar
François Bobot committed
89 90
  - the filenames in the location inside a session should be relative
   to the session_dir.
91 92 93 94 95 96 97 98

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
99
   are taken into account in session.