Sémantique axiomatique

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.

Sommaire

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}

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è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).

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 pgcd des entrées a et b, ainsi que les coefficients p et q de l'identité de Bézout :

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

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é.

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


Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Sémantique axiomatique de Wikipédia en français (auteurs)

Игры ⚽ Поможем решить контрольную работу

Regardez d'autres dictionnaires:

  • Semantique axiomatique — 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. Sommaire 1 L idée 2 Le langage : la logique de Hoare 3 Preuves …   Wikipédia en Français

  • Semantique des langages de programmation — Sémantique des langages de programmation En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. Sommaire 1 Lien avec la… …   Wikipédia en Français

  • AXIOMATIQUE — La méthode axiomatique est un mode d’exposition des sciences exactes fondé sur des propositions admises sans démonstration et nettement formulées et des raisonnements rigoureux. On se limitera ici à quelques indications méthodologiques et… …   Encyclopédie Universelle

  • Semantique denotationnelle — Sémantique dénotationnelle En informatique, la sémantique dénotationnelle est une des approches permettant de formaliser la signification d un programme en utilisant les mathématiques. Parmi les autres approches, on trouve la sémantique… …   Wikipédia en Français

  • Sémantique des langages de programmation — En informatique théorique, la sémantique formelle (des langages de programmation) est l’étude de la signification des programmes informatiques vus en tant qu’objets mathématiques. Sommaire 1 Lien avec la linguistique 2 Sémantiques usuelles d’un… …   Wikipédia en Français

  • Sémantique opérationnelle — En informatique, la sémantique opérationnelle est l une des approches qui servent à donner une signification aux programmes informatiques d une manière rigoureuse, mathématiquement parlant (voir Sémantique des langages de programmation). Une… …   Wikipédia en Français

  • Sémantique dénotationnelle — En informatique, la sémantique dénotationnelle est une des approches permettant de formaliser la signification d un programme en utilisant les mathématiques. Parmi les autres approches, on trouve la sémantique axiomatique et la sémantique… …   Wikipédia en Français

  • Décidabilité — En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique. L indécidabilité est la négation de la décidabilité. Dans les deux cas il s agit de formaliser l idée qu… …   Wikipédia en Français

  • Calcul Des Prédicats — Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin du XIXe siècle et …   Wikipédia en Français

  • Calcul des predicats — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”