TODO 650 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 11 12 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,
    since the key is the value.

Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
18 19
  - 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
20 21 22 23

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