lustrec/optim/TODO.org @ 6a93d814
| 1 |
|
|---|---|
| 2 |
* a partir du machine code, generer les predicats et annotations concrets, PC et AC |
| 3 |
* a partir du lustre, generer les predicats abstraits PA |
| 4 |
* prouver que le code C respecte AC |
| 5 |
** horloges |
| 6 |
** genericite |
| 7 |
** noeuds imbriques (sans applatissement) |
| 8 |
* prouver que AC=>PA |