Implantation

5 Implantation

L'implantation est un cas particulier de raffinement en une machine qui ne pourra plus être raffinée.

La forme générale d'une machine d'implantation est :

IMPLEMENTATION nomI	/* nom de la machine d'implantation */
REFINES nom	/* nom de la machine raffinée */
· · ·
END

5.1 Principes

Les implantations respectent certaines règles :

Une implantation n'a pas de variables propres.
Une implantation utilise les opérations de machines qu'elle importe (primitives ou implantées par ailleurs) et dont elle ne peut voir les variables sauf pour exprimer les invariants.
Certaines restrictions sont appliquées aux substitutions apparaissant dans une implantation afin d'assurer qu'elle pourra être traduite en un programme exécutable :
- pas de choix non déterministe ou de composition parallèle,
- les conditions dans les substitutions IF-THEN-ELSE sont limitées à des expressions booléennes simples,
- les opérations ne s'appliquent qu'à des variables locales ou paramètres,
- les affectations mettent en jeu des expressions simples,
- ...
une implantation peut introduire des substitutions correspondant à des boucles WHILE, il faudra par contre indiquer pour chaque boucle WHILE, un invariant et un variant (quantité qui décroit à chaque passage dans la boucle).
Au moment de l'implantation, toutes les constantes déclarées ou les ensembles non énumérés doivent être instanciés (explicitement dans une clause VALUES ou dans une des machines importées).

5.2 Restrictions

5.2.1 Substitutions autorisées

Les substitutions autorisées dans une implantation sont :

L'introduction de variables locales par la substitution VAR IN END. Les variables introduites doivent être typées dans la substitution en apparaissant dans une substitution d'initialisation (affectation ou comme variable de sortie d'une opération).
La substitution BEGIN END qui permet de grouper une séquence de substitutions.
La substitution IF THEN ELSE END et ses variantes :
(IF THEN END, IF THEN ELSEIF THEN ELSE END ...)
La condition doit correspondre à une expression booléenne calculable.
La substitution CASE qui est une forme de SELECT mais dont les prédicats testent l'appartenance à un ensemble. La substitution s'écrit :
CASE e OF EITHER E₁ THEN S₁ OR E₂ THEN S₂ END END
Dans cette substitution, e est une expression simple, E_i un ensemble et S_i une substitution, le nombre de branches peut être quelconque et une clause ELSE peut également apparaître.
La séquence de deux substitutions.
Une boucle WHILE précisant un variant et un invariant.
L'affectation d'une expression simple à une variable qui peut être une variable locale ou une variable de sortie de l'opération.
Une opération d'une machine vue ou importée. La sortie de l'opération utilisée doit être formée de variables locales ou de variables de sortie de l'opération dans laquelle apparaît la substitution.

Toutes les autres substitutions ANY, SELECT, LET ... ne sont pas autorisées dans les implantations.

5.2.2 Expressions autorisées

Dans les affectations ou dans les boucles, les expressions qui peuvent être utilisées sont restreintes.

Une expression simple est une variable locale, ou une variable d'entrée ou bien une constante (des machines raffinées, importées ou vues) ou un littéral (constante entière, valeur booléenne TRUE ou FALSE).

Les expressions générales qui peuvent être utilisées dans une implantation peuvent être soit une expression simple ou bien une expression arithmétique construite à partir des opérateurs d'addition, de soustration, de multiplication, de division, de reste modulo ou d'exponentiation.

Dans les conditions des substitutions IF ou WHILE, les expressions peuvent être formées à partir des connecteurs ¬, Ù, Ú and Þ et des formules de comparaison d'expressions simples.

5.3 La clause IMPORTS

Si une implantation ne peut plus être raffinée, elle peut par contre importer des machines qui, elles, seront raffinées.

Une implantation va être construite en combinant d'autre machines plus élémentaires suivant un principe de développement en niveaux. En général on utilisera les descriptions abstraites des machines élémentaires qui elles-mêmes seront raffinées et implantées. On pourra utiliser les machines des bibliothèques présentes dans les outils de développement.

La clause IMPORTS se comporte dans les implémentations de manière analogue à la clause INCLUDES utilisée dans les spécifications. Cependant, les variables de la machine importée seront complètement cachées dans les opérations de la machine qui importe.

5.4 La clause VALUES

La clause VALUES apparait dans les machines d'implantation pour donner une valeur aux constantes concrètes de la clause CONSTANTS et aux ensembles abstraits de la clause SETS de la machine raffinée.

La clause VALUES est suivie d'un ensemble de déclarations id=valeur séparées par des points virgules. id est le nom de la donnée à valuer et valeur sa valeur. L'ordre des valuations est important. Une constante ne peut être utilisée dans la partie valeur que si elle a été préalablement définie.

Lorsqu'une constante ou un ensemble abstrait d'une implantation M apparaît avec le même nom dans une machine M' importée ou bien vue par M, alors la donnée de M est implicitement valuée par l'objet de même nom de la machine M'.

5.4.1 Valuation d'un ensemble abstrait

Un ensemble abstrait doit toujours être valué par un ensemble non vide d'entiers. Ce peut-être :

un intervalle d'entiers de la forme n₁..n₂
un ensemble abstrait d'une machine vue ou importée
un ensemble abstrait de la machine implantée qui a déjà été valué

5.4.2 Valuation d'une constante scalaire

Une constante scalaire a pour type INT, ou BOOL ou bien un ensemble abstrait ou énuméré. Elle doit être valuée par une expression appartenant au type correspondant.

5.4.3 Valuation d'une constante de tableau

Une constante de tableau peut être valuée

par une constante de machine vue ou importée,
par un tableau dont tous les éléments ont la même valeur, exprimé sous la forme D × {e} avec D le domaine du tableau et e la valeur des éléments du tableau, par exemple un tableau tab Î (0..2) --> N pourra être implanté par la clause :
VALUES tab = (0..2) × {0}
par un ensemble de maplets qui permettent de représenter des n-uplets, les n-1 premiers éléments représentent les indices du tableau et le dernier la valeur en ce point, par exemple un tableau tab Î (0..1) × (0..1) --> N pourra être implanté par la clause
VALUES tab = {0 |® 0 |® 0, 0|® 1 |® 1, 1|® 0 |® 2, 1|® 1 |® 3}

5.5 Substitution WHILE

Afin de pouvoir exprimer des programmes qui effectuent un nombre non borné d'itérations, le langage B autorise l'utilisation d'une substitution WHILE. La syntaxe d'une substitution WHILE est :

WHILE P DO S INVARIANT I VARIANT V END

P est un prédicat (la condition de la boucle, S est une substitution (le corps de la boucle), I est un prédicat, l'invariant et V est une expression, le variant qui représente une grandeur qui diminue à chaque passage dans la boucle mais reste positive.

L'action de cette substitution sur un prédicat R est défini comme la conjonction de plusieurs propriétés :

1	L'invariant I est satisfait à l'entrée de la boucle	I
2	L'invariant I est préservé par le passage dans la boucle	I Ù P Þ [S]I
3	Le variant est un entier	I Þ V Î N
4	Le variant décroit dans le passage dans la boucle	I Ù P Þ [n:=V][S](V < n)
5	En sortie de boucle, la propriété R découle de l'invariant et de la non-satisfaction de la condition	I Ù ¬ P Þ R

Dans la condition (4), n est une variable qui n'apparaît pas dans la substitution WHILE. La propriété [S](V < n) assure que la valeur de V après l'exécution de S est inférieure à n. La substitution [n:=V] remplace alors n par la valeur de V avant l'exécution de S.

Supposons que l'on veuille implanter une opération qui prend en argument un ensemble non vide c d'entiers positifs et renvoie le minimum de cet ensemble. Dans la machine de spécification, l'opération peut apparaître sous la forme :

r ¬¾ MinSet(c) = PRE c Î P₁(N) THEN r:=min(c) END

Si on cherche maintenant à en faire une implantation concrète, on peut choisir une méthode où on teste successivement les entiers à partir de 0, le premier qui apparaît dans l'ensemble est le minimum (cette méthode n'est intéressante d'un point de vue algorithmique que si le test pour savoir si un objet appartient à un ensemble est efficace ...)

Dans le raffinement, l'opération MinSet pourra être

r ¬¾ MinSet(c) =

PRE c Î P₁(N)

THEN r:=0;

WHILE r Ïc DO r:=r+1

INVARIANT r Î 0..min(c) VARIANT min(c)-r

END

5.6 Exemple

Nous prenons un exemple de machine représentant un ensemble fini (ici d'entiers non nuls), qui permet d'ajouter des éléments mais également de calculer le maximum de l'ensemble. La spécification de la machine est la suivante :

MACHINE MaxEns

VARIABLE ens

INVARIANT ens Î F(N₁)

INITIALISATION ens := Ø

OPERATIONS

enter(n) = PRE n Î N₁ THEN ens:=ensÈ {n} END;

m ¬¾ maximum = PRE ens ¹Ø THEN m:=max(ens) END

END

Comme la seule opération à réaliser sur l'ensemble stocké dans cette machine est de trouver le maximum, il n'est pas utile de garder un ensemble arbitraire, on peut se contenter d'une variable entière. On obtient donc le raffinement :

REFINEMENT MaxEns1

REFINES MaxEns

VARIABLES mEns

INVARIANT mEns=max(ensÈ {0})

INITIALISATION mEns := 0

OPERATIONS

enter(n) = PRE n Î N₁ THEN mEns:=max({mEns,n}) END;

m ¬¾ maximum = PRE z ¹0 THEN m:=mEns END

END

Exercice

Énoncer les obligations de preuve

Il est possible de faire plusieurs raffinement successifs, par exemple le corps de l'opération ajout peut être modifié pour faire disparaître l'appel à la fonction max.

REFINEMENT MaxEns2

REFINES MaxEns1

VARIABLES mEns

INITIALISATION mEns := 0

OPERATIONS

enter(n) = IF n ³ mEns THEN mEns:=n END;

m ¬¾ maximum = m:=mEns END

END

La variable de la machine MaxEns2 ayant le même nom que celle de la machine MaxEns1, un invariant implicite disant que ces deux variables sont égales est ajouté.

Pour implanter notre exemple, nous avons besoin d'une variable entière qui sera obtenue en important une machine implantant une variable entière :

MACHINE Scalar(initval)

CONSTRAINTS initval Î N

VARIABLES z

INVARIANT zÎ N

INITIALISATION z:=initval

OPERATIONS

v¬¾ valeur = v:=z;

modifie(v) = PRE v Î N THEN z:=v END

END

Nous pouvons alors écrire l'implémentation de la machine MaxEns.

IMPLEMENTATION MaxEns3

REFINES MaxEns2

IMPORTS Scalar(0)

INVARIANT z = mEns

OPERATIONS

enter(n) =

VAR v

IN v¬¾ value; IF n ³ v THEN modify(n) END

END;

m ¬¾ maximum = BEGIN m ¬¾ value END

END