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 Si=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.

[Stack Elt Bool ]
new: → Stack
push: Stack*Elt → Stack
pop: Stack → Stack
top: Stack → Elt
empty?: Stack → Bool
true: → Bool
false: → Bool

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 1) 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 t1=t2 où t1 et t2 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)
Exemples d'axiomes pour [Stack Elt Bool]
pop(push(p,x)) = p
top(push(p,x)) = x
empty?(new) = true
empty?(push(p,x) ) = false

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.

Sémantique des termes

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

[ T1 T2 T3 ]
op1: →T1
op2: T1 * T2 → T1
et cetera

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

Σ-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é SA
  • à 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 :

[Nat Bool ]
zero: → Nat
v, f: → Bool
succ: Nat → Nat
add: Nat*Nat → Nat
sup: Nat*Nat → Bool

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
    • NatNum = \mathbb{N}
    • BoolNum = {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 4) 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 :

  • NatNum4 = {0,1,2,3} ⊆ N
  • BoolNum4 = {vrai, faux}
  • zeroNum4 = 0
  • vNum4 = vrai
  • fNum4 = faux
  • succNum4 : {0,1,2,3} → {0,1,2,3} : n \mapsto (n+1\; mod\; 4
  • addNum4 : {0,1,2,3}×{0,1,2,3} → {0,1,2,3} : n,m \mapsto (n+m\; mod\; 4
  • supNum4 : {0,1,2,3}×{0,1,2,3} → {0,1,2,3} : n,m \mapsto vrai si n>m, faux sinon.

Algèbre des Termes Clos

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

\begin{eqnarray}f_{T_\Sigma} : & S_{1_{T_\Sigma}}\times S_{2_{T_\Sigma}} \times \cdots \times S_{n_{T_\Sigma}} \rightarrow S_{0_{T_\Sigma}} \\ & \left(t_1, t_2, \ldots t_n\right) \rightarrow f\left(t_1, t_2, \ldots t_n\right) \end{eqnarray}

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

1) spécifieur n'est pas un mot
2) push(new,x),y
3) sigma majuscule, à ne pas confondre avec σ-algèbre, plus communément appelé tribu en français mathématique
4) e.g., (Z, + , * ) forme un anneau
 
m1ilc/semantics_a.txt · Dernière modification: 2010/05/27 21:39 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki