<page> <title>Sémantique axiomatique</title> <id>98420</id> <revision> <id>25896312</id> <timestamp>2008-02-08T11:28:10Z</timestamp> <contributor> <username>DumZiBoT</username> <id>280295</id> </contributor> <minor /> <comment>Robot : Passage au modèle {{ébauche}} : {{ébauche|informatique}}</comment> <text xml:space="preserve">{{ébauche|informatique}} La '''sémantique axiomatique''' est une approche basée sur la [[logique mathématique]] qui sert à prouver qu'un [[programme informatique]] est correct. ==L'idée== 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. ==Le langage : la logique de Hoare== 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. ==Preuves== 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ègle d'inférence|règles d'inférence]] spécifiques à la sémantique axiomatique du langage informatique utilisé (preuve à la [[C.A.R. Hoare|Hoare]]), soit par la réécriture du programme en son entier, mais décoré de prédicats entre chaque instruction (preuve à la [[Robert Floyd|Floyd]]). La preuve à la Floyd donne de plus une méthode systématique très pratique pour obtenir cette preuve dans les programmes impératifs séquentiels : on part de ce qui doit être vérifié après le programme, puis on remonte instruction par instruction en cherchant à chaque pas la précondition la plus faible. ''Exemple : preuve à la Floyd de l'[[algorithme d'Euclide étendu]]'' Ceci est l'algorithme d'Euclide étendu, qui calcule le [[plus grand commun diviseur|pgcd]] des entrées ''a'' et ''b'', ainsi que les coefficients ''p'' et ''q'' de l'[[identité de Bézout]] : :<tt> a0 = a; b0 = b; p = 1; q = 0; r = 0; s = 1; tant que b != 0 faire c = a modulo b; quotient = a / b; a = b; b = c; nouveau_r = p - quotient * r; nouveau_s = q - quotient * s; p = r; q = s; r = nouveau_r; s = nouveau_s; fait </tt> Une des propriétés voulues à la fin est : ''a = p*a0 + q*b0''. Nous allons remonter le programme instruction par instruction pour obtenir la preuve (à la Floyd) que cela est bien vérifié. // à compléter // ==La sémantique axiomatique et les autres== La sémantique axiomatique est l'une des sémantiques les plus grossières (anglais : ''coarse-grained'') que l'on rencontre pour les langages de programmation. Elle est en effet une approximation, ou [[abstraction]] de la [[sémantique dénotationnelle]], qui voit le programme comme une fonction qui transforme la mémoire et elle-même approxime la [[sémantique opérationnelle]] qui voit le programme comme une succession d'états de la machine. ''Voir aussi :'' *[[Sémantique des langages de programmation]] *[[Logique de Hoare]] *[[Sémantique dénotationnelle]] *[[Sémantique opérationnelle]] [[Catégorie:Informatique théorique]] [[Catégorie:Méthode formelle]] [[de:Axiomatische Semantik]] [[en:Axiomatic semantics]] [[hr:Aksiomatska semantika]] [[ja:å…¬ç†çš„æ„å‘³è«–]] [[pt:Semântica axiomática]]</text> </revision> </page>