Spécification Algébrique

Les types sont des éléments importants dans la construction des programmes. Dans cette partie, nous présentons un cadre qui permet de définir formellement les types et les opérations sur les objets de ces types. Ce cadre est celui des spécifications algébriques.

Nous nous intéressons particulièrement à la sémantique d'une spécification algébrique, c'est à dire, à la définition du–ou des–types de données qu'elle décrit, et moins aux aspects méthodologiques pour écrire une spécification algébrique.

spécification algébrique

une spécification algébrique décrit un ou plusieurs types de données par une signature et un ensemble d'axiomes.

signature

un ensemble de noms de types appelés sortes et un ensemble de noms d'opérations tels que chaque nom d'opération est associé à un profil de la forme S1 S2… Sn → S0 où les S_i=0..n sont des sortes.

Voici l'exemple d'une signature en vue de spécifier le type des piles, en utilisant une notation CafeOBT-like.

Ici, Stack, Elt, et Bool sont des sortes, et new, puch, pop, top, empty?, true et false sont des noms d'opérations.

D'un point de vue méthodologique, pour écrire une spécification algébrique le spécificateur ¹⁾ peut distinguer parmi les noms des opérations

• ceux qui référent à des constructeurs : new, push, true, false
• ceux qui référent à d'autres opérations dites externes : pop, top, empty?

axiome

une équation t₁=t₂ où t₁ et t₂ sont des termes de même sorte.

Une signature et un ensemble de variables sortées (associées à une sorte) définit (engendre) un ensemble d'expressions bien formées appelées termes.

terme

un terme de sorte S est

• soit une variable de sorte S
• soit de la forme f(t1,t2,…tn) où f est un nom d'opération de profil S1 S2… Sn → S et où t1,t2,…tn sont des termes de sortes S1 S2… Sn respectivement.

Voici un exemple de terme de sorte Stack (telle que définit ci-dessus) : x, y, z, et t sont des variables de sort Elt.

push(push(pop(push((push(new,x),y)),z),t)

Vérifions push qui donne sorte Stack opère ici avec les sortes Stack et Elt. Ceci est-il de sorte Stack?

push(pop(push( (push(new,x),y) ),z)

Oui, si ceci est de sorte Stack (et les deux dernières imbrications aussi) :

pop(push( (push(new,x),y) )
push( (push(new,x),y)
push(new, x)

Intuitivement, les axiomes permettent au spécificateur de compléter la définition des opérations en précisant l'action des opérations externes sur les constructeurs.

Nous venons de voir qu'une signature définit un ensemble de termes (on peut assimiler une signature à une grammaire définissant la syntaxe d'un langage). Il faut se rappeler qu'une signature en elle-même n'attache aucune signification aux termes.

On aurait pu utiliser une autre signature pour les piles, telle que

et choisir de noter le terme précédent op2 ( op2( op3( op2( op2( opt1,x),y)),z),t). au lieu de push(push(pop(push2),z),t)

Cela n'a pas d'influence sur la sémantique de la spécification algébrique; mais pour notre compréhension il est plus facile d'utiliser des noms d'opération plus évocateurs.

La sémantique des termes (on parle plutôt dans ce cadre d'interprétation des termes) est définie dans une algèbre par représentation des termes, c'est à dire de chaque sorte et de chaque nom d'opération. Une telle algèbre associée à une signature, disons Σ, est appelé Σ-algèbre. ³⁾.

Σ-algèbre

étant donnée une signature Σ, une Σ-algèbre est une application A qui fait correspondre

• à chaque sorte S un ensemble bien connu (exemple, un ensemble mathématique) appelé ensemble support de S, et noté S_A
• à chaque nom de d'opération f de profil S1 S2… Sn → S0 une opération notée fA de type noté f_A : S_{1_A}\times S_{2_A}\times\ldots \times S_{n_A}\rightarrow S_{n_A}

Prenons une signature qui vise à spécifier les entiers naturels :

Une Σ-algèbre est par exemple l'algèbre Num définie par

• à la sorte Nat, elle fait correspondre \mathbb{N}
• à la sorte Bool, elle fait correspondre {vrai, faux}
• on note
  • Nat_Num = \mathbb{N}
  • Bool_Num = {vrai, faux}
• pour les opérations,

…

Une telle algèbre est qualifiée de multisorte car la signature comporte plusieurs sortes (ici Nat et Bool). Il s'agit d'une généralisation de la notion d'algèbre en maths où on définit une structure par un ensemble muni d'un certain nombre d'opérations vérifiant certaines propriétés qualifiées d'algébriques ⁴⁾ et ainsi de définir la structure caractéristique d'un type de données.

Il y a de nombreuses Σ-algèbres possibles pour un spécification Σ.

Une des autre Σ-algèbres possible pour Nat est Num4 :

• Nat_Num4 = {0,1,2,3} ⊆ N
• Bool_Num4 = {vrai, faux}
• zero_Num4 = 0
• v_Num4 = vrai
• f_Num4 = faux
• succ_Num4 : {0,1,2,3} → {0,1,2,3} : n \mapsto (n+1\; mod\; 4
• add_Num4 : {0,1,2,3}×{0,1,2,3} → {0,1,2,3} : n,m \mapsto (n+m\; mod\; 4
• sup_Num4 : {0,1,2,3}×{0,1,2,3} → {0,1,2,3} : n,m \mapsto vrai si n>m, faux sinon.

Un autre Σ-algèbre est l'algèbre des termes clos. On peut construire une Σ-algèbre à partir d'une signature Σ en faisant correspondre à chaque sorte S l'ensemble des termes de sorte S qui sont construits à partir des seuls noms des opérations de la signature Σ.

Par exemple, de tels termes

• de sorte Nat : zero, succ(zero), add(zero, succ(zero) )
• de sorte Bool : v, f, sup(zero,sero)

De tels termes qui ne contiennent pas de variables sont appelés termes clos et l'algèbre ainsi construite est appelée algèbre des termes clos et notée T_Σ où Σ est le nom de la signature. Elle fait correspondre à chaque nom d'opération f de profil S1 S2… Sn → S0 l'opération

Remarque : L'intérêt de cette Σ-algèbre est qu'elle ne dépend que de la signature Σ. Nous reviendrons dans la suite sur cette Σ-algèbre pour définir la sémantique d'une spécification.

Remarque : Etant donné un ensemble de variables sortées, on peut évidement définir une autre Σ-algèbre qui fait correspondre à chaque sorte S l'ensemble des termes de sorte S. Cette autre Σ-algèbre est appelée algèbre des termes.

Raffinement de Programmes ⇐ * ⇒ Sémantique d'une Spécification