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

Andrei Paskevich's avatar
Andrei Paskevich committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
  - 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?

22 23 24
  - 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
25

26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
  - 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.

48 49 50
syntaxe
-------

51
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
52

53 54 55 56 57 58 59 60
  - 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
61

62
sémantique
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
63
----------
64

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

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

70 71 72 73 74
  - 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
75 76
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
77
     François -- I don't get that point the weak Hashtbl that we use
78 79 80
   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.
81

82 83
  - 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
84

85 86
  - open (et échouer si "open A" et "open B" avec A et B déclarant un symbole
    de même nom)
87

88 89 90 91 92 93
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)
94 95 96 97 98

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

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