Sémantique axiomatique

La sémantique axiomatique est une approche basée sur la logique mathématique qui sert à prouver qu'un programme informatique est correct. Cette sémantique tend à considérer un programme comme un transformateur de propriétés logiques, c'est-à-dire que la signification donnée au programme est un ensemble de prédicats qui sont vérifiés par l'état de la machine (caractérisé par sa mémoire) qui a exécuté le programme, à condition qu'un autre ensemble de prédicats ait été vérifié avant exécution. L'enjeu est en général de trouver la sémantique axiomatique la plus fine possible : étant donné une spécification de sortie que l'on veut en général la plus forte (restrictive) possible, on cherche les préconditions les plus faibles (larges) qui aboutissent à ce résultat. Les propriétés de sémantique axiomatique s'expriment, en général, sous la forme d'expressions de la logique de Hoare : {p}S{q} où p et q sont des propriétés exprimées dans la logique des prédicats, p censé être vérifié par la mémoire avant exécution du programme S (anglais : statement), et q devant être vérifié après exécution de S sur une machine vérifiant p. Du fait que l'exécution du programme ne termine pas forcément, il y a en fait 2 interprétations d'une expression de la logique de Hoare : {p}S{q} veut dire « Si l'état de la mémoire satisfait p et S termine, alors, après exécution, l'état de la mémoire satisfait q. » : correction partielle [p]S[q] veut dire « Si l'état de la mémoire satisfait p, alors S termine et après exécution, l'état de la mémoire satisfait q. » : correction totale Ces deux interprétations mènent à des sémantiques axiomatiques différentes. Donner la sémantique axiomatique d'un programme, c'est réaliser la preuve de certaines propriétés sur celui-ci. Cette sémantique, cette preuve, peut être représentée, en général, par deux méthodes : soit par l'arbre d'inférence qui utilise explicitement les règles d'inférence spécifiques à la sémantique axiomatique du langage informatique utilisé (preuve à la Hoare), soit par la réécriture du programme en son entier, mais décoré de prédicats entre chaque instruction (preuve à la Floyd).