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

4 5 6
  - 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
7

8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29
  - 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.

30 31 32
syntaxe
-------

33
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
34

35 36 37 38 39 40 41 42
  - 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
43

44
sémantique
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
45
----------
46

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

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

52 53 54 55 56
  - 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
57 58
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
59
     François -- I don't get that point the weak Hashtbl that we use
60 61 62
   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.
63

64 65
  - 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
66

67 68
  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
    de même nom)
69

70 71 72 73 74 75
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)
76 77 78 79 80

session
-------
  - save the output of the prover
  - escape the string in the xml
François Bobot's avatar
François Bobot committed
81 82
  - the filenames in the location inside a session should be relative
   to the session_dir.
83 84 85 86 87 88 89 90

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