Peut-on utiliser `\list` pour fire la même chose que Why3 ?

[eponier]

[lyonel2017]

Dans le cas ou des tableaux sont manipulés, je pense qu'il n'y a pas beaucoup intérêt d'utiliser '\liste', sauf si l'on veut faire toutes les preuves en logique. Cependant, '\liste" peut-être intéressante si des listes chaînées sont manipulées dans le code source.

[eponier]

Mais peut-être que vu ce que nous a dit Loïc, il vaut mieux laisser tomber les fonctionnalités avancées d'ACSL et jouer sur la modélisation (tout mettre dans un tableau, utiliser une fonction logique bien pensée...).

[lyonel2017]

Je pense qu'une combinaison des fonctionnalités avancées d'ACSL et joué sur la modélisation est la meilleure solution.