44
Traducteurs de l’Atelier B - Manuel Utilisateur
type_tableau
PROPERTIES
type_tableau = (4..12) --> INT
/ * extension B0-HIA * /
VALUES
type_tableau = (4..12) --> INT / * inutilisé par le traducteur * /
CONCRETE_VARIABLES
var
INVARIANT
var : type_tableau / * typage explicite par identificateur imposé par B0-HIA * /
INITIALISATION
var := (4..12)*{1}
B.3
B.3.1
Traduction des articles
Principe
Pour pouvoir être traduite par le traducteur HIA, une donnée de type article doit impérativement
avoir été typée explicitement par un identificateur, c’est à dire par appartenance à une
donnée qui définit un type article (c’est une restriction par rapport au langage B0 classique).
Les données qui définissent les types articles sont des constantes concrètes, qui doivent
être typées par égalité avec un type “article” )) B. C’est ce type B définit dans la clause
PROPERTIES qui est utilisé pour la traduction ; la valuation est ignorée.
Nous préconisons de recopier le typage de la clause PROPERTIES dans la clause VALUES pour
éviter toute confusion. La possibilité de définir une constante concrète de type tableau est
une extension par rapport au langage B0 classique.
B.3.2
Exemple
Pour écrire en B0-HIA la déclaration d’une variable var de type (( article, dont le premier
champ tab est de type ’tableau d’entiers, dont les index sont entre 4 et 12’, et le deuxième
champ valid est de type ’booléen’ )), on écrira :
CONCRETE_CONSTANTS
type_tableau,
type_article
PROPERTIES
type_tableau = (4..12) --> INT / * extension B0-HIA * / &
type_article = struct(
tab : type_tableau,
valid : BOOL) / * extension B0-HIA * /
VALUES
type_tableau = (4..12) --> INT ; / * inutilisé par le traducteur * /
type_article = struct(
tab : type_tableau,
">
