<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]] :

:&lt;tt&gt;

 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

&lt;/tt&gt;

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>