Invariants assistés par IA

Analyse des invariants, pre/post conditions

Vous avez trois implémentations concrètes de set. Nous allons d’abord vérifier qu’il est possible de les unifier avec un même type abstrait (TAD).

Pour chacune des implementations sentinel, dynamic et link, faites calculer les invariants, pre/post conditions par l’IA, l’un ou l’autre des serveurs:

• Copiez le script invariant.py
• Lancer la commande sur le serveur fast, dans un shell:

  python3 invariant.py --base-url http://10.21.18.46:1234/fast --key pg116-SECRET --review MONREPERTOIRE/link/set_link.c
  

• Lancer la commande sur le serveur big, dans un shell:

  python3 invariant.py --base-url http://10.21.18.46:1234/big --key pg116-SECRET --review MONREPERTOIRE/link/set_link.c
  

Definition des tests à partir des invariants, pre/post conditions

Pour la fonction ‘set__add’:

• Trouver des conditions pre/post et un invariant pour le TAD qui soit compatible avec ceux des trois implémentations. Les ajouter en commentaire dans ‘set/set.h’
• Est-ce que les preconditions des implémentations sont des cas particuliers de celles du TAD, l’inverse ?
• Les tests fonctionnels doivent vérifier ce qui se passe quand les preconditions sont vraies/fausses, et vérifier l’invariant. Quels tests fonctionnels faut-il ecrire pour le ‘set__add’ du TAD, à partir de ses invariants et pre/post conditions ?