Semantic proof graph

Reflexion en cours.

La traçabilité classique relie une ligne de spec à un test. Je veux plus : conserver toute la dérivation.

texte source → terme → concept ontologique → relation → règle métier
→ propriété formelle → obligation → donnée témoin → assertion générée
→ observation runtime → verdict → mutants rejetés

Je l’appellerais Semantic Proof Graph. Chaque noeud porte sa provenance : le range L42-L44 du doc source, les termes mappés vers leurs concepts, les relations d’ontologie, la règle, la propriété, les policies appliquées, l’instanciation (Alice, OrgA, visible [A1,A2], interdit [B1]), l’assertion générée, l’évidence runtime (observed []), le verdict (failed, expected vs observed), et les mutants tués (missing-org-id, wrong-org-id, disabled-rls).

La littérature sur la traçabilité des exigences parle de récupérer et maintenir des liens exigence/artefact. Là le lien n’est pas documentaire : il porte la dérivation sémantique et la preuve d’exécution. C’est ce qui permet de dire « l’intention de la phrase initiale n’a pas été perdue jusqu’au comportement observé ».

À creuser : comment on visualise ce graphe sans que ça devienne illisible sur une vraie app de centaines de features ? Liés : alloy-contre-modeles, evolution-ontologique, compiler-intention-en-preuve