Sémantique des langages de programmation

En sémantique opérationnelle[2], la signification d’un programme est la suite des états de la machine qui exécute le programme. Autrement dit, un programme est considéré comme la description d’un système de transition d'états.

Dans cette sémantique, les programmes :

a=1; b=0

et

a=1;
b=0

sont équivalents car ils ont la même signification.

Par contre le programme :

b=0; a=1

ne leur est pas équivalent. En effet, même si le résultat final est le même, les actions d'affectation de valeurs aux variables a et b n’ont pas lieu dans le même ordre.

Il est possible d'abstraire cette sémantique en n’observant qu’une partie de la mémoire de la machine, telle que :

• les interactions du programme avec l’extérieur
• la trace du programme.

Initiée par Christopher Strachey et Dana Scott, la sémantique dénotationnelle[3] est une approche dans laquelle une fonction mathématique appelée dénotation est associée à chaque programme, et représente en quelque sorte son effet, sa signification. Cette fonction prend par exemple pour argument l’état de la mémoire avant exécution, et a pour résultat l’état après exécution.

Dans cette sémantique, tous les exemples donnés ci-dessus pour la sémantique opérationnelle sont équivalents, mais le programme :

a=1;
b=1;

ne leur est pas équivalent.

Il existe plusieurs variantes de la sémantique dénotationnelle, dont l’une des plus célèbres est la sémantique dénotationnelle par continuation qui, au lieu d’associer à un programme une fonction qui transforme la mémoire, lui associe une fonction qui transforme la continuation (le futur) de la machine après exécution du programme en la continuation avant exécution du programme. Autrement dit, la sémantique dénotationnelle par continuation fonctionne à rebours du programme, elle considère ce qui se passe après une instruction pour en déduire ce qui doit se passer avant cette instruction[4].

Un des aspects importants de la sémantique dénotationnelle est la propriété de compositionnalité : la dénotation d'un programme est obtenue par combinaison des dénotations de ses constituants.

En sémantique axiomatique[5], le programme n’est plus qu’un transformateur de propriétés logiques sur l’état de la mémoire : si on a p vrai avant exécution, alors on a q vrai après. On ne s’intéresse plus à l’état précis de la mémoire tant que l’on sait dire si la propriété tient.

Si la propriété qui nous intéresse, c’est de savoir si a et b sont positifs après exécution du programme, alors tous les exemples précédents sont équivalents au sens où quel que soit l’état de la machine avant exécution du programme, la propriété en sortie tient. Ce que l’on note en logique de Hoare :

${\displaystyle \{{\text{vrai}}\}}$ a=1; b=0 ${\displaystyle \{a\geq 0\land b\geq 0\}}$

• Machine de Krivine
• Machine SECD