TODO 795 Bytes
Newer Older
1 2 3 4

syntaxe
-------

5
  - open
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
6 7 8 9


sémantique
----------
10

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

13 14 15 16 17
  - 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
18 19
    since the key is the value. Should we use generation numbers in arguments
    and results of transformations?
20

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
21 22
  - 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
23 24 25 26

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