|
1
|
ALT2
|
|
2
|
|
|
3
|
evalue plusieurs options
|
|
4
|
- soit l'iniling de toutes les nodes (inlining via lustrec)
|
|
5
|
|
|
6
|
|
|
7
|
- soit passer toutes les variables locales en existencielles (au lieu de let)
|
|
8
|
pousser les variables locales dans l'intergace de trans
|
|
9
|
et les quantifier existencielle;ent dans Ctrans
|
|
10
|
|
|
11
|
dans le cas let: gros but ou petit nombre de gros buts, dur a analyser ?(au
|
|
12
|
moins pour lhumain)
|
|
13
|
|
|
14
|
dans le cas existenciel: plein de petits buts, mais il y en a un qui ne passe
|
|
15
|
pas
|
|
16
|
|
|
17
|
|
|
18
|
- probleme du typage des bool
|
|
19
|
- si on utilise _Bool ca merde, il faudrait modifier les mlw
|
|
20
|
- ca a l'air de marcher si on les declare comme int
|
|
21
|
|
|
22
|
|
|
23
|
|
|
24
|
- pour les preuves
|
|
25
|
- etre capable d'inliner uniquement la def du symbole de tete du goal (pas indispensable)
|
|
26
|
- appeler coqide depuis why3ide (librairie QED bug)
|
|
27
|
- utiliser la tactic why3smt dans coq (a voir a la compil de why3)
|
|
28
|
- generer les fichiers why3 a la mai, en tout cas en shell
|
|
29
|
|
|
30
|
- coq3ide: ajouter une fonction de recherche dans la fenetre en haut a droite
|
|
31
|
|
|
32
|
- autre alternative:
|
|
33
|
appeler coq depuis frama-c: intros. unfold symbole_de_tete (unfold
|
|
34
|
P_trans_AltitudeControl). repeat split. puis appeler la tactic why3
|