Alloy contre modeles

Reflexion en cours.

Alloy répondrait à deux questions que le reste de la pile ne pose pas.

Le dataset est-il discriminant ? Existe-t-il au moins deux organisations, un utilisateur, un objet autorisé et un objet interdit ? Sinon le test ne prouve rien.

L’oracle laisse-t-il passer un monde incorrect ? C’est le coeur du bug. Si l’oracle dit seulement « aucun projet étranger ne doit être visible », Alloy produit le contre-modèle :

expected = [A1, A2]
observed = []

Aucun projet étranger visible, donc l’oracle passe, alors que la feature est cassée. Ça démontre que l’oracle manque une propriété : « tous les projets autorisés doivent être visibles ». La propriété forte devient observed = expected (égalité d’ensembles, pas juste inclusion).

Donc Alloy ne remplace pas l’ontologie : il explore les conséquences de sa formalisation et cherche les contre-modèles acceptés à tort. C’est le cran DISCRIMINATING de la preuve.

À creuser : coût de faire tourner Alloy par feature ? Est-ce qu’on ne le sort que pour les collections scopées, ou systématiquement ? Liés : inference-data-tests, semantic-proof-graph, monde-ferme-vs-owl, compiler-intention-en-preuve