search

lyonel2017 / VerifyThis-2017

2 stars 0 forks source link

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

Open eponier opened 7 years ago

lyonel2017 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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