.rs .\" Troff code generated by TPS Convert from ITU Original Files .\" Not Copyright ( c) 1991 .\" .\" Assumes tbl, eqn, MS macros, and lots of luck. .TA 1c 2c 3c 4c 5c 6c 7c 8c .ds CH .ds CF .EQ delim @@ .EN .nr LL 40.5P .nr ll 40.5P .nr HM 3P .nr FM 6P .nr PO 4P .nr PD 9p .po 4P .rs \v | 5i' .sp 1P .LP D.5.4 \fIDirectives applicables \*`a la repr\*'esentation en fonction des\fR \fI\*'etats et aux \*'el\*'ements graphiques\fR .sp 9p .RT .PP Le pr\*'esent paragraphe d\*'ecrit la repr\*'esentation en fonction des \*'etats du LDS/GR et des \*'el\*'ements graphiques utilis\*'es. .PP Le \(sc\ D.5.4.1 contient des observations d'ordre g\*'en\*'eral sur la repr\*'esentation en fonction des \*'etats: caract\*'eristiques, applications pertinentes et variantes. .PP Le \(sc\ D.5.4.2 explique la description d'\*'etats au moyen d'\*'el\*'ements graphiques. .RT .sp 1P .LP D.5.4.1 \fIObservations d'ordre g\*'en\*'eral sur la repr\*'esentation en fonction\fR \fIdes \*'etats\fR .sp 9p .RT .PP Le LDS/GR offre trois versions diff\*'erentes pour d\*'ecrire un diagramme de processus. .PP La premi\*`ere est appel\*'ee version du LDS/GR en fonction des transitions, dans laquelle les transitions sont d\*'ecrites exclusivement par des symboles d'action explicites. .PP La seconde est appel\*'ee version du LDS/GR orient\*'ee vers les \*'etats ou extension graphique du LDS orient\*'ee vers les \*'etats; les \*'etats d'un processus y sont d\*'ecrits \*`a l'aide d'illustrations d'\*'etats et les transitions ne sont donn\*'ees qu'implicitement, par les diff\*'erences entre les \*'etats de d\*'epart et d'arriv\*'ee. .PP La derni\*`ere est appel\*'ee version mixte; il s'agit d'une combinaison des deux versions pr\*'ec\*'edentes. .PP On trouvera des exemples de ces trois versions dans l'annexe\ E du pr\*'esent fascicule. .PP La version orient\*'ee vers les transitions convient lorsque la s\*'equence des actions pr\*'esente plus d'importance que la description d\*'etaill\*'ee des \*'etats. .PP La version orient\*'ee vers les \*'etats d\*'ecrit en d\*'etail les \*'etats par des \*'enonc\*'es; elle convient donc au cas o\*`u un \*'etat de processus pr\*'esente plus d'importance que la s\*'equence des actions \*`a l'int\*'erieur de chaque transition, alors que l'explication graphique intuitive est souhaitable et qu'il est int\*'eressant de conna\* | tre les ressources ainsi que leurs relations avec les \*'etats. .PP Les illustrations d'\*'etat sont g\*'en\*'eralement exprim\*'ees par des \*'el\*'ements graphiques indiquant les ressources pertinentes de l'\*'etat en cours du processus. Cette version convient \*`a des applications dans lesquelles sont d\*'efinis des \*'el\*'ements graphiques appropri\*'es; l'utilisateur peut donc employer cette repr\*'esentation pour n'importe quelle application en d\*'efinissant des \*'el\*'ements graphiques appropri\*'es selon les besoins. .PP La version mixte convient lorsqu'il faut conna\* | tre \*`a la fois la s\*'equence des actions int\*'erieures \*`a chaque transition et les descriptions d\*'etaill\*'ees des \*'etats. .RT .sp 2P .LP D.5.4.2 \fIIllustration d'\*'etat et \*'el\*'ement graphique\fR .sp 1P .RT .sp 1P .LP D.5.4.2.1\ \ \fIEl\*'ement graphique et texte qualificatif\fR .sp 9p .RT .PP Si l'on a choisi l'option illustration d'\*'etat, celle\(hyci se compose d'\*'el\*'ements graphiques et d'un texte qualificatif, comme indiqu\*'e dans la figure\ D\(hy5.4.1\ a) \*`a\ D\(hy5.4.1\ d). .PP Cette combinaison rend compr\*'ehensibles les illustrations d'\*'etat. A titre d'exemple, la figure\ D\(hy5.4.1\ a) donne la signification d'un r\*'ecepteur \*`a cadran manipul\*'e par le processus, l'exemple\ b) celle d'un \*'emetteur de tonalit\*'e de num\*'erotation \*'emettant un signal permanent vers l'environnement. .PP A noter que les signaux de sortie (signaux non permanents) et les ressources pertinentes ne sont pas d\*'ecrits dans les illustrations d'\*'etat; les signaux de sortie peuvent \* | tre d\*'ecrits dans un diagramme de transition. .PP L'exemple c) montre un temporisateur dont l'expiration est toujours repr\*'esent\*'ee par une entr\*'ee. A noter que l'illustration graphique recommand\*'ee pour le temporisateur comporte le signal d'entr\*'ee pertinent\ t1. .PP Le dernier exemple, d), signifie qu'un enregistreur de messages vocaux est en cours de fonctionnement. .PP L'identit\*'e de la ressource peut \* | tre consid\*'erablement abr\*'eg\*'ee et devrait, si possible, \* | tre plac\*'ee \*`a l'int\*'erieur de l'illustration graphique appropri\*'ee. Ainsi, les \*'el\*'ements graphiques qui sont qualifi\*'es sont tout \*`a fait \*'evidents. .RT .sp 1P .LP D.5.4.2.2\ \ \fIIllustrations d'\*'etat compl\*`etes\fR .sp 9p .RT .PP Chaque illustration d'\*'etat doit comporter un nombre suffisant d'\*'el\*'ements graphiques afin de montrer: .RT .LP a) quelles ressources le processus met en oeuvre au cours de l'\*'etat repr\*'esent\*'e. Exemples: trajets de commutation, r\*'ecepteurs de signalisation, \*'emetteurs de signaux permanents et modules de commutation; .LP b) s'il y a en ce moment un ou plusieurs temporisateurs qui contr\* | lent le processus; .LP c) dans le cas o\*`u le processus concerne le traitement des appels, si la taxation est ou non actuellement en cours et quels abonn\*'es sont tax\*'es au cours de cette phase de l'appel; .bp .LP d) quels objets appartenant effectivement \*`a un autre processus (environnement) sont consid\*'er\*'es comme en relation avec des ressources du processus pendant l'\*'etat en cours; .LP e) les signaux permanents de sortie qui sont \*'emis dans cet \*'etat; .LP f ) la relation entre les signaux et ressources existants dans l'\*'etat; .LP g) l'inventaire des ressources concernant l'\*'etat en cours du processus. .LP .rs .sp 31P .ad r \fBFigura D\(hy5.4.1, (N), p. 1\fR .sp 1P .RT .ad b .RT .sp 1P .LP D.5.4.2.3\ \ \fIExemple\fR .sp 9p .RT .PP A titre d'exemple d'application des principes expos\*'es ci\(hydessus, consid\*'erons l'\*'etat de la figure\ D\(hy5.4.2. On peut voir que, dans cet \*'etat: .RT .LP a) les ressources affect\*'ees aux processus sont: un r\*'ecepteur de chiffres \*`a cadran, un \*'emetteur de tonalit\*'es de num\*'erotation, un poste d'abonn\*'e appartenant \*`a l'environnement et des trajets de communication reliant ces organes; .LP b) un temporisateur\ t0 surveille le processus; .LP c) aucune taxation n'est en cours; .LP d) l'abonn\*'e est identifi\*'e comme l'abonn\*'e\ A mais aucune autre information de cat\*'egorie n'est prise en consid\*'eration; .LP e) les signaux d'entr\*'ee suivants sont attendus: A \(ulon \(ulhook (A\ raccroch\*'e), digit (chiffre) (chiffre num\*'erot\*'e) et\ t0 (le temporisateur de supervision t0\ fonctionne); .LP f ) le signal permanent de sortie DT (tonalit\*'e de num\*'erotation) a \*'et\*'e mis avant cet \*'etat et pendant celui\(hyci. .bp .LP .rs .sp 23P .ad r \fBFigure D\(hy5.4.2, (N), p. 2\fR .sp 1P .RT .ad b .RT .sp 1P .LP D.5.4.2.4\ \ \fIV\*'erification de la coh\*'erence de diagrammes LDS avec \*'el\*'ements\fR \fIgraphiques\fR .sp 9p .RT .PP On constate que l'illustration d'\*'etat est plus compacte et que, d'une certaine mani\*`ere, elle offre au lecteur plus d'informations; cependant, l'identification de la s\*'erie exacte d'op\*'erations accomplies au cours de la transition exige un examen tr\*`es attentif des ressources. .PP En outre, une simple observation de l'illustration d'\*'etat ne permet pas de d\*'eterminer l'ordre des actions dans la transition. .PP Les \*'el\*'ements graphiques repr\*'esent\*'es \*`a l'ext\*'erieur du bloc sont des \*'el\*'ements qui ne sont pas directement command\*'es par le processus donn\*'e: ceux qui sont repr\*'esent\*'es \*`a l'int\*'erieur du symbole <> sont directement command\*'es par ce processus. Par exemple, le processus d'appel partiellement sp\*'ecifi\*'e dans la figure\ D\(hy5.4.3 peut allouer ou lib\*'erer l'\*'emetteur de tonalit\*'e d'appel, l'\*'emetteur de sonnerie et les trajets de conversation; il peut \*'egalement d\*'eclencher ou arr\* | ter le temporisateur\ T4, mais il ne peut commander directement la condition du combin\*'e de l'abonn\*'e. .PP En concevant la logique \*`a partir d'une sp\*'ecification LDS avec \*'el\*'ements graphiques, seuls les \*'el\*'ements graphiques repr\*'esent\*'es \*`a l'int\*'erieur des limites du bloc ont une influence sur les actions ex\*'ecut\*'ees pendant les s\*'equences de la transition. Les \*'el\*'ements graphiques complexes repr\*'esent\*'es \*`a l'int\*'erieur des limites de ce bloc sont normalement inlus dans une illustration d'\*'etat: .RT .LP a) soit parce qu'ils indiquent les ressources et l'\*'etat de l'environnement concern\*'es par le signal d'entr\*'ee du processus pendant l'\*'etat donn\*'e; .LP b) soit pour am\*'eliorer l'intelligibilit\*'e du diagramme. .sp 1P .LP D.5.4.2.5\ \ \fIUtilisation du symbole <>\fR .sp 9p .RT .PP Que l'on emploie ou non des \*'el\*'ements graphiques, l'expiration d'un d\*'elai de temporisation est toujours repr\*'esent\*'ee par une entr\*'ee. .PP La pr\*'esence d'un symbole de temporisateur dans une illustration d'\*'etat implique qu'un temporisateur fonctionne pendant cet \*'etat. .bp .RT .LP .rs .sp 38P .ad r \fBFigure D\(hy5.4.3, (N), p. 3\fR .sp 1P .RT .ad b .RT .PP Conform\*'ement au principe g\*'en\*'eral expos\*'e dans les Recommandations, le d\*'emarrage, l'arr\* | t, le red\*'emarrage et l'expiration du temporisateur sont repr\*'esent\*'es \*`a l'aide d'\*'el\*'ements graphiques de la mani\*`ere suivante: .RT .LP a) pour montrer qu'une temporisation commence au cours d'une transition donn\*'ee, le symbole temporisateur doit appara\* | tre sur l'illustration d'\*'etat qui correspond \*`a la fin de cette transition et non sur celle qui correspond \*`a son d\*'ebut; .LP b) inversement, pour montrer qu'une temporisation s'arr\* | te au cours d'une transition, le symbole temporisateur doit appara\* | tre sur l'illustration d'\*'etat qui correspond au d\*'ebut de cette transition et non sur celle qui correspond \*`a sa fin; .LP c) pour montrer qu'une temporisation est relanc\*'ee au cours d'une transition un symbole explicite de t\* | che doit \* | tre repr\*'esent\*'e dans cette transition (on en voit deux exemples sur la figure\ D\(hy5.4.4); .LP d) l'expiration du d\*'elai d'une temporisation donn\*'ee est repr\*'esent\*'ee par un symbole d'entr\*'ee associ\*'e \*`a un \*'etat dont l'illustration porte le symbole <> correspondant. Il peut naturellement arriver que plusieurs temporisateurs surveillent \*`a la fois le m\* | me processus (voir la figure\ D\(hy5.4.5). .bp .LP .rs .sp 47P .ad r \fBFigure D\(hy5.4.4, (N), p. 4\fR .sp 1P .RT .ad b .RT .LP .bp .LP .rs .sp 37P .ad r \fBFigure D\(hy5.4.5, (N), p. 5\fR .sp 1P .RT .ad b .RT .sp 1P .LP D.5.5 \fIDiagrammes auxiliaires\fR .sp 9p .RT .PP Pour faciliter la lecture et la compr\*'ehension de diagrammes de processus de grande taille et/ou complexes, l'auteur peut y ajouter des diagrammes auxiliaires informels. De tels documents ont pour but de donner une description synoptique ou simplifi\*'ee du comportement du processus (ou d'une partie de celui\(hyci). Les documents auxiliaires ne remplacent pas les documents en LDS mais constituent une introduction \*`a ceux\(hyci. .PP On trouvera dans la pr\*'esente section des exemples de certains diagrammes auxiliaires couramment utilis\*'es, notamment des diagrammes synoptiques d'\*'etat, des matrices \*'etat/signal, et des diagrammes de s\*'equencement. (Le diagramme en arbre de bloc d\*'ecrit au \(sc\ D.4.4 est \*'egalement un diagramme auxiliaire.) .RT .sp 1P .LP D.5.5.1 \fIDiagramme synoptique d'\*'etat\fR .sp 9p .RT .PP Son objectif est de donner une vue d'ensemble des \*'etats d'un processus, et d'indiquer quelles transitions sont possibles entre eux. Etant donn\*'e qu'il s'agit de donner un aper\*,cu, l'on peut n\*'egliger les \*'etats ou les transitions de peu d'importance. .bp .PP Les diagrammes se composent de symboles d'\*'etat, de fl\*`eches repr\*'esentant des transitions et, \*'eventuellement, de symboles de d\*'ebut et d'arr\* | t. .PP Le symbole d'\*'etat doit indiquer le nom de l'\*'etat r\*'ef\*'erenc\*'e. Plusieurs noms d'\*'etat peuvent \* | tre inscrits dans le symbole, et il est possible d'employer un ast\*'erisque (*) pour d\*'esigner tous les \*'etats. .PP Chacune des fl\*`eches peut, de m\* | me que chacune des sorties possibles pendant la transition, \* | tre associ\*'ee au nom du signal ou de l'ensemble de signaux qui d\*'eclenchent la transition. .PP On trouvera dans la figure\ D\(hy5.5.1 un exemple de diagramme synoptique d'\*'etat. .RT .LP .rs .sp 23P .ad r \fBFigure D\(hy5.5.1, (MC), p. 6\fR .sp 1P .RT .ad b .RT .PP Il est possible de r\*'epartir sur plusieurs diagrammes le diagramme synoptique d'\*'etat d'un processus; chacun des diagrammes obtenus porte alors sur un aspect particulier, comme <>, traitement en cas de d\*'efaillance,\ etc. .LP .rs .sp 14P .ad r \fBFigure D\(hy5.5.2, (N), p. 7\fR .sp 1P .RT .ad b .RT .LP .bp .sp 1P .LP D.5.5.2 \fIMatrice \*'etat/signal\fR .sp 9p .RT .PP La matrice \*'etat/signal doit servir de document <> \*`a un diagramme de processus important. Elle indique les endroits o\*`u existent des combinaisons entre un \*'etat et un signal dans le diagramme. .PP Le diagramme se compose d'une matrice bidimensionnelle; celle\(hyci pr\*'esente sur un axe tous les \*'etats d'un processus, et sur l'autre tous les signaux d'entr\*'ee valides d'un processus. L'\*'etat suivant est donn\*'e pour chaque \*'el\*'ement de matrice, de m\* | me que les sorties possibles au cours de la transition. Une r\*'ef\*'erence peut \* | tre indiqu\*'ee pour permettre de trouver la combinaison donn\*'ee par les indices, si elle existe. .PP L'\*'el\*'ement correspondant \*`a l'\*'etat fictif ou <> et au signal fictif <> sert \*`a indiquer l'\*'etat initial du processus. .RT .LP .rs .sp 24P .ad r \fBFigure D\(hy5.5.3, (MC), p. 8\fR .sp 1P .RT .ad b .RT .PP Il est possible de fractionner la matrice en sous\(hyparties r\*'eparties sur plusieurs pages. Les r\*'ef\*'erences sont celles qu'emploie normalement l'usager dans la documentation. .PP Les signaux et les \*'etats doivent \* | tre de pr\*'ef\*'erence regroup\*'es de fa\*,con que chaque partie de la matrice porte sur un aspect particulier du comportement du processus. .RT .sp 1P .LP D.5.5.3 \fIDiagramme de s\*'equencement\fR .sp 9p .RT .PP Le diagramme de s\*'equencement peut servir \*`a montrer l'\*'echange des s\*'equences de signaux autoris\*'ees entre un ou plusieurs processus et leur environnement. .PP Ce diagramme doit donner une vue d'ensemble de l'\*'echange de signaux entre les parties du syst\*`eme. Ce diagramme peut repr\*'esenter l'ensemble ou une partie de l'\*'echange de signaux, en fonction des aspects \*`a mettre en \*'evidence. .PP Les colonnes du diagramme indiquent les entit\*'es en communication (services, processus, blocs ou l'environnement). .PP Leurs interactions sont illustr\*'ees par un ensemble de lignes fl\*'ech\*'ees, dont chacune repr\*'esente un signal ou un ensemble de signaux. .bp .RT .LP .rs .sp 27P .ad r \fBFigure D\(hy5.5.4, (N), p. 9\fR .sp 1P .RT .ad b .RT .PP On peut annoter chaque s\*'equence afin de faire appara\* | tre clairement l'ensemble d'informations \*'echang\*'ees. Chaque ligne est accompagn\*'ee d'une annotation qui donne les renseignements requis (noms des signaux ou de proc\*'edures). .PP On peut placer un symbole de d\*'ecision dans les colonnes pour indiquer que la s\*'equence suivante est valide si la condition indiqu\*'ee est vraie. Dans ce cas, le symbole de d\*'ecision appara\* | t g\*'en\*'eralement plusieurs fois; il indique les diff\*'erentes s\*'equences produites par chacune des valeurs de la condition. .PP Ce diagramme peut repr\*'esenter la totalit\*'e ou seulement un sous\(hyensemble significatif des s\*'equences de signaux \*'echang\*'es. .PP La repr\*'esentation de l'interaction r\*'eciproque des services r\*'esultant de la subdivision d'un processus repr\*'esente une application utile de ce type de diagramme. .PP Les diagrammes de s\*'equencement ne comprennent g\*'en\*'eralement pas toutes les s\*'equences possibles; ils constituent souvent un pr\*'ealable \*`a la d\*'efinition compl\*`ete. .RT .sp 2P .LP D.6 \fID\*'efinition des donn\*'ees en LDS\fR .sp 1P .RT .sp 1P .LP D.6.1 \fIDirectives applicables aux\fR \fIdonn\*'ees en LDS\fR .sp 9p .RT .PP On trouvera dans la pr\*'esente section des renseignements compl\*'ementaires sur les concepts d\*'efinis au \(sc\ 5 de la Recommandation concernant le LDS. La principale diff\*'erence entre la pr\*'esente section et l'ancienne Recommandation\ Z.104 est que cette derni\*`ere a fait l'objet d'une r\*'evision \*`a des fins de clarification et d'harmonisation avec l'ISO. Certains des mots cl\*'es ont \*'et\*'e modifi\*'es et des adjonctions ont \*'et\*'e faites mais la coh\*'erence de la s\*'emantique a \*'et\*'e assur\*'ee avec le Livre rouge. L'emploi des donn\*'ees d\*'ecrites aux \(sc\ 2, 3 et\ 4 de la nouvelle Recommandation (auparavant\ Z.101\(hyZ.103) est rest\*'e tel quel. .bp .RT .sp 1P .LP D.6.1.1 \fIIntroduction g\*'en\*'erale\fR .sp 9p .RT .PP Les types de donn\*'ees du LDS sont fond\*'es sur l'approche de <>: on ne d\*'ecrit pas la mani\*`ere dont un type doit \* | tre mis en oeuvre, mais on se borne \*`a dire quel sera le r\*'esultat des op\*'erateurs appliqu\*'e aux valeurs. .PP Lorsque l'on d\*'efinit des donn\*'ees abstraites, chaque segment de la d\*'efinition, appel\*'ee <> est introduit par le mot\(hycl\*'e NEWTYPE. Chaque d\*'efinition de type partielle a une incidence sur les autres, de sorte que toutes les d\*'efinitions de type partielles au niveau du syst\*`eme constituent une d\*'efinition de type de donn\*'ees unique. Si plusieurs d\*'efinitions de type partielles sont introduites \*`a un niveau inf\*'erieur (niveau de bloc, par exemple), leur ensemble constitue, avec les d\*'efinitions de niveau sup\*'erieur, une d\*'efinition de type de donn\*'ees. Cela signifie qu'en un point quelconque de la sp\*'ecification, il n'existe qu'\fIune seule\fR d\*'efinition de type de donn\*'ees. .PP En substance, la d\*'efinition de type de donn\*'ees comprend trois parties: .RT .LP a) d\*'efinitions de sortes; .LP b) d\*'efinitions d'op\*'erateurs; .LP c) \*'equations. .PP Chacune de ces parties fait l'objet d'explications dans les paragraphes qui suivent. La d\*'efinition de type de donn\*'ees est structur\*'ee en d\*'efinitions de type de donn\*'ees partielles, chacune introduisant une sorte. Les d\*'efinitions d'op\*'erateurs et les \*'equations recouvrent les d\*'efinitions de type de donn\*'ees partielles. .sp 1P .LP D.6.1.2 \fISortes\fR .sp 9p .RT .PP Une sorte est un ensemble de valeurs qui peut avoir un nombre fini ou infini d'\*'el\*'ements mais ne peut \* | tre vide. .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) l'ensemble de valeurs de la sorte bool\*'eenne est { rue (vrai), False (faux } .LP b) l'ensemble de valeurs de la sorte Natural (naturel) est l'ensemble infini des nombres naturesls { ,\ 1, 2,\ . | \ } .LP c) l'ensemble de valeurs de la sorte Couleur \(ulprimaire est { ert, Rouge, Ble } .PP Tous les \*'el\*'ements d'une sorte ne doivent pas \* | tre directement fournis par l'utilisateur (cela exigerait un temps infini dans le cas des nombres naturels), mais le nom de la sorte doit \* | tre indiqu\*'e. Dans la syntaxe concr\*`ete, le mot\(hycl\*'e NEWTYPE est directement suivi par le nom de la sorte (certaines autres possibilit\*'es seront indiqu\*'ees plus loin). Ce nom est surtout utilis\*'e dans les d\*'efinitions d'op\*'erateurs, comme expliqu\*'e au \(sc\ D.6.1.3, et dans les d\*'eclarations de variables. .sp 1P .LP D.6.1.3 \fIOp\*'erateurs, litt\*'eraux et termes\fR .sp 9p .RT .PP Les valeurs d'une sorte peuvent \* | tre d\*'efinies de trois mani\*`eres: .RT .LP a) par une \*'enum\*'eration: les valeurs sont d\*'efinies dans la section des litt\*'eraux; .LP b) par des op\*'erateurs: les valeurs sont donn\*'ees comme les r\*'esultats d'<> d'op\*'erateurs; .LP c) par une combinaison d'\*'enum\*'erations et d'op\*'erateurs. .PP La combinaison de litt\*'eraux et d'op\*'erateurs donne des termes. Les relations entre les termes sont exprim\*'ees \*`a l'aide d'\*'equations. Les paragraphes qui suivent traitent des litt\*'eraux, des op\*'erateurs et des termes; le \(sc\ D.6.1.4 traite des \*'equations. .sp 1P .LP D.6.1.3.1\ \ \fILitt\*'eraux\fR .sp 9p .RT .PP Les litt\*'eraux sont des valeurs \*'enum\*'er\*'ees d'une sorte. Une d\*'efinition de type partiel ne doit pas n\*'ecessairement comporter de litt\*'eraux: tous les \*'el\*'ements de la sorte peuvent \* | tre d\*'efinis au moyen d'op\*'erateurs. Les litt\*'eraux peuvent \* | tre consid\*'er\*'es comme des op\*'erateurs d\*'epourvus d'arguments. Une relation entre les litt\*'eraux peut \* | tre exprim\*'ee dans des \*'equations. Dans la syntaxe concr\*`ete, les litt\*'eraux sont introduits apr\*`es le mot\(hycl\*'e LITERALS. .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) La d\*'efinition de la sorte bool\*'eenne contient deux litt\*'eraux, \*`a savoir True (vrai) et False (faux). Ainsi, la d\*'efinition du type bool\*'een se pr\*'esente comme suit: .LP NEWTYPE Boolean .LP \ \ LITERALS True, False .LP \ \ . | | .LP ENDNEWTYPE Boolean; .bp .LP b) la sorte naturelle peut \* | tre d\*'efinie \*`a l'aide d'un litt\*'eral, le z\*'ero. Les autres valeurs peuvent \* | tre g\*'en\*'er\*'ees au moyen de ce litt\*'eral et d'op\*'erateurs; .LP c) les valeurs de la sorte couleur \(ulprimaire peuvent \* | tre d\*'efinies de la m\* | me mani\*`ere que les litt\*'eraux bool\*'eens; .LP NEWTYPE Primary \(ulcolour .LP \ \ LITERALS Red, Green, Blue .LP \ \ . | | .LP ENDNEWTYPE Primary \(ulcolour; .LP d) au \(sc D.6.1.3.2, le troisi\*`eme exemple\ c) pr\*'esente une d\*'efinition de type partielle sans litt\*'eraux. .sp 1P .LP D.6.1.3.2\ \ \fIOp\*'erateurs\fR .sp 9p .RT .PP Un op\*'erateur est une fonction math\*'ematique qui met en concordance une ou plusieurs valeurs (\*'eventuellement de sortes diff\*'erentes) avec une valeur r\*'esultante. Les op\*'erateurs sont introduits apr\*`es le mot\(hycl\*'e OPERATORS, la ou les sortes de leur ou leurs arguments et la sorte de r\*'esultat sont \*'egalement indiqu\*'ees (on parle de signature des op\*'erateurs). .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) dans le type bool\*'een, un op\*'erateur appel\*'e <> peut \* | tre d\*'efini; il aura un argument de sorte bool\*'een et \*'egalement un r\*'esultat de sorte bool\*'een. Dans la d\*'efinition du type bool\*'een, il se pr\*'esente comme suit: .LP NEWTYPE Boolean .LP \ \ LITERALS True, False .LP \ \ OPERATORS <>: Boolean\(hy>Boolean; .LP \ \ . | | .LP ENDNEWTYPE Boolean; .LP b) l'op\*'erateur susmentionnn\*'e n\*'ecessaire pour construire tous les nombres naturels est Next. Cet op\*'erateur prend un argument de sorte naturelle et donne une valeur naturelle (la valeur sup\*'erieure suivante) en tant que r\*'esultat; .LP c) il est possible de d\*'efinir pour des couleurs un nouveau type qui n'a pas de litt\*'eraux mais utilise des litt\*'eraux de la sorte couleur primaire et certains op\*'erateurs: .LP NEWTYPE Color .LP \ \ OPERATORS .LP \ \ \ \ Take: Primary \(ulcolour\(hy>Colour; .LP \ \ \ \ Mix: Primary \(ulcolour, Colour\(hy>Colour; .LP \ \ \ . | | .LP ENDNEWTYPE Colour; .PP Il s'agissait de prendre une couleur primaire et de la consid\*'erer comme une couleur puis de commencer \*`a m\*'elanger plusieurs couleurs primaires afin d'obtenir d'autres couleurs. .sp 1P .LP D.6.1.3.3\ \ \fITermes\fR .sp 9p .RT .PP A l'aide de litt\*'eraux et d'op\*'erateurs, il est possible de construire comme suit l'ensemble des termes: .RT .LP 1) Rassembler tous les litt\*'eraux dans un ensemble de la sorte dans laquelle ils sont d\*'efinis \(em\ chaque litt\*'eral est un terme. .LP 2) Un nouvel ensemble de termes est cr\*'e\*'e pour chaque op\*'erateur lorsque l'op\*'erateur est appliqu\*'e \*`a toutes les combinaisons possibles de termes de la sorte correcte cr\*'e\*'es pr\*'ec\*'edemment: .LP a) pour la sorte <>, l'ensemble de litt\*'eraux est { rue (vrai), False (faux } Le r\*'esultat de cette \*'etape est { ot (True), Not (False } parce que nous avons seulement l'op\*'erateur Not (non); .LP b) pour la sorte <>, le r\*'esultat de cette \*'etape est { ext(0 } .LP c) pour la sorte <> l'ensemble de litt\*'eraux est vide mais le r\*'esultat de cette \*'etape est { ake(Red), Take(green), Take(Blue } .LP 3) Les termes des ensembles cr\*'e\*'es au cours de l'\*'etape pr\*'ec\*'edente sont tous la sorte du r\*'esultat de l'op\*'erateur appliqu\*'e; par exemple, tous les r\*'esultats de l'op\*'erateur Not sont de la sorte bool\*'eenne. Alors, on r\*'eunit tous les ensembles de la m\* | me sorte, aussi bien des ensemble initiaux que les ensembles nouvellement cr\*'e\*'es: .LP a) pour la sorte bool\*'eenne, on obtient l'ensemble { rue, False, Not(True), Not(False } .LP b) pour les nombres naturels cette \*'etape donne l'ensemble { ,\ Next(0 } .bp .LP 4) Les deux derni\*`eres \*'etapes sont r\*'ep\*'et\*'ees \*`a maintes reprises, et d\*'efinissent en g\*'en\*'eral un ensemble infini de termes: .LP a) l'ensemble de termes bool\*'eens g\*'en\*'er\*'es par les litt\*'eraux True et False et l'op\*'erateur Not est { rue, False, Not(True), Not(False), Not(Not(True)), Not(Not(False)), Not(Not(Not(True))),\ . | | } .LP b) l'ensemble des termes naturels g\*'en\*'er\*'es par le litt\*'eral\ 0 et l'op\*'erateur Next est { ,\ Next(0), Next(Next(0)), Next(Next(Next(0))),\ . | | } .LP c) l'ensemble des termes de couleur g\*'en\*'er\*'es par les litt\*'eraux Red, Green et Blue de la sorte Primary \(ulcolour et les op\*'erateurs Take et Mix est { ake(Red), Take(Green), Take(Blue), Mix(Red, Take(Red)), Mix(Red, Take(Green)), Mix(Red, Take(Blue)), Mix(Green, Take(Red)), Mix(Green, Take(Green)), Mix(Green, Take(Blue)), Mix(Blue, Take(Red)), Mix(Blue, Take(Green)), Mix(Blue, Take(Blue)),\ . | | } .sp 1P .LP D.6.1.4 \fIEquations et axiomes\fR .sp 9p .RT .PP D'une mani\*`ere g\*'en\*'erale, le nombre de termes g\*'en\*'er\*'es au paragraphe pr\*'ec\*'edent est sup\*'erieur au nombre de valeurs de la sorte. A titre d'exemple, il existe deux valeurs bool\*'eennes mais l'ensemble de termes bool\*'eens a un nombre infini d'\*'el\*'ements. Il existe cependant une possibilit\*'e d'\*'etablir des r\*`egles sp\*'ecifiant quels sont les termes consid\*'er\*'es comme d\*'esignant la m\* | me valeur. Ces r\*`egles sont appel\*'ees \*'equations et font l'objet du paragraphe suivant. Deux types particuliers d'\*'equations, les axiomes et les \*'equations conditionnelles, font l'objet des \(sc\ D.6.1.4.2 et\ D.6.1.4.3. .PP Les \*'equations, les axiomes et les \*'equations conditionnelles sont donn\*'es, dans la syntaxe concr\*`ete apr\*`es le mot\(hycl\*'e AXIOMS. Ce mot\(hycl\*'e a \*'et\*'e conserv\*'e pour des raisons d'ordre historique. .RT .sp 1P .LP D.6.1.4.1\ \ \fIEquations\fR .sp 9p .RT .PP Une \*'equation indique quels sont les termes consid\*'er\*'es comme d\*'esignant la m\* | me valeur. Une \*'equation relie deux termes s\*'epar\*'es par le symbole d'\*'equivalence\ ==. .PP Par exemple <> indique que les termes Not(True) et False sont \*'equivalents; chaque fois que l'on trouve Not(True), on peut le remplacer par False sans changement de sens et vice versa. .PP Dans certaines \*'equations, l'ensemble de termes est divis\*'e en sous\(hyensembles discontinus de termes qui d\*'esignent la m\* | me valeur. Ces sous\(hyensembles sont appel\*'es classes d'\*'equivalence. Dans le langage courant, les classes d'\*'equivalence sont identifi\*'ees aux valeurs. .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) L'ensemble de termes de la sorte bool\*'eenne est divis\*'e en deux classes d'\*'equivalence de termes par les deux axiomes suivants: .LP Not(True) ==\ False; .LP Not(False) ==\ True; .LP Les classes d'\*'equivalence qui en r\*'esultent sont: .LP { rue, Not(False), Not(Not(True)), Not(Not(Not(False))), .LP Not(Not(Not(Not(True)))), Not(Not(Not(Not(Not(False))))),\ . | | } .LP et .LP { alse, Not(True), Not(Not(False)), Not(Not(Not(True))), .LP Not(Not(Not(Not(False)))), Not(Not(Not(Not(Not(True))))) } . | | .LP Ces deux classes d'\*'equivalence sont identifi\*'ees aux valeurs True (Vrai) et False (Faux); .LP b) Dans le cas de couleurs, on peut d\*'esirer sp\*'ecifier que le m\*'elange d'une couleur primaire avec une couleur qui contient cette couleur primaire ne fait pas de diff\*'erence. De plus, l'ordre dans lequel les primaires sont m\*'elang\*'es est sans importance. Cela peut \* | tre \*'enonc\*'e dans les \*'equations suivantes: .LP Mix(Red, Take(Red)) ==\ Take(Red); .LP Mix(Red, Mix(Red, Take(Green))) ==\ Mix(Red, Take(Green)); .LP Mix(Red, Mix(Red, Take(Blue))) ==\ Mix(Red Take(Blue)); .LP Mix(Red, Mix(Green, Take(Red))) ==\ Mix(Green, Take(Red)); .LP Mix(Red, Mix(Blue, Take(Red))) ==\ Mix(Blue, Take(Red));\ etc. .bp .LP Cela demande beaucoup de travail car des \*'equations similaires apparaissent pour toutes les permutations de Red, Green et Blue. C'est pourquoi le LDS comporte la construction FOR\(hyALL qui introduit les noms de valeur repr\*'esentant une classe d'\*'equivalence arbitraire (ou la valeur associ\*'ee \*`a cette classe d'\*'equivalence). Cela peut \* | tre tr\*`es utile dans la situation ci\(hydessus; toutes les \*'equations susmentionn\*'ees et celles qui sont indiqu\*'ees par\ etc. peuvent \* | tre d\*'ecrites en quelques lignes sous la forme suivante: .LP FOR ALL p1, p2 IN Primary \(ulcolour .LP /*1*/\ \ \ Mix(p1, Take(p1))\ ==\ Take(p1); .LP /*2*/\ \ \ Mix(p1, Mix(p1, Take(p2)))\ ==\ Mix(p1, Take(p2)); .LP /*3*/\ \ \ Mix(p1, Mix(p2, Take(p1)))\ ==\ Mix(p2, Take(p1)); .LP /*4*/\ \ \ Mix(p1, Take(p2))\ ==\ Mix(p2, Take(p1)); .LP /*4*/\ \ \ FOR ALL c IN Colour .LP /*5*/\ \ \ (\ Mix(p1, Mix(p2, c))\ ==\ Mix(p2, Mix(p1, c)); .LP /*6*/\ \ \ (\ Mix(p1, Mix(p2, c))\ ==\ Mix(Mix(p1, Take(p2))\ c)) .LP /*4*/\ \ \ ) .LP Dans les \*'equations ci\(hydessus, il y a chevauchement mais cela ne pose pas de probl\*`emes pour autant que les \*'equations ne se contredisent pas mutuellement. .LP Les \*'equations susmentionn\*'ees cr\*'eent 7 classes d'\*'equivalence dans l'ensemble de termes de la sorte Colour, de sorte qu'avec ces \*'equations, il y a sept valeurs de couleurs. Les termes suivants sont dans les classes d'\*'equivalence diff\*'erentes: .LP Take(Red), Take(Green), Take(Blue), .LP Take(Red, Take(Green)), .LP Mix(Green, Take(Blue)), .LP Mix(Blue, Take(Red)), .LP Mix(Blue, Mix(Green, Take(Red))). .LP Tous les autres termes de la sorte Colour sont \*'equivalents \*`a l'un des termes ci\(hydessus. .LP Dans les exemples d'\*'equations comportant la construction FOR\(hyALL, appel\*'ees \*'equations explicitement quantifi\*'ees, l'information que p1 et p2 sont des identificateurs de valeur de sorte Primary \(ulcolour est redondante; l'argument de l'op\*'erateur Take et le premier argument de l'op\*'erateur Mix ne peuvent \* | tre de la sorte Primary \(ulcolour. En g\*'en\*'eral, les \*'equations explicitement quantifi\*'ees deviennent plus lisibles mais il est possible d'omettre la quantification si la sorte des identificateurs de valeur peut \* | tre d\*'eduite du contexte. Dans ce cas, on dit que l'\*'equation est implicitement quantifi\*'ee. .sp 1P .LP \fIExemple:\fR .sp 9p .RT .LP Les \*'equations 4 et 5 ci\(hydessus sont les m\* | mes que: .LP Mix(p1, Take(p2)) , c)) \ \ \ ==\ Mix(p2, Take(p1)); .LP Mix(p1, Mix(p2, c))\ \ \ ==\ Mix(p2, Mix(p1,\ c)); .sp 1P .LP D.6.1.4.2\ \ \fIAxiomes\fR .sp 9p .RT .PP Les axiomes sont simplement des esp\*`eces particuli\*`eres d'\*'equation, introduites parce que dans des situations pratiques, de nombreuses \*'equations se rapportent \*`a des bool\*'eens. Dans ce cas, les \*'equations tendent \*`a prendre la forme\ . | | \ ==\ True (vrai), c'est\(hy\*`a\(hydire qu'elles indiquent qu'un terme donn\*'e est \*'equivalent \*`a True. .RT .sp 1P .LP \fIExemple:\fR .sp 9p .RT .LP Admettons qu'un op\*'erateur soit d\*'efini pour une couleur type: Contains: Colour, Primary \(ulcolour\(hy> Boolean; ce qui doit donner la r\*'eponse True (vrai) si la couleur primaire est contenue dans la couleur et False (faux) dans le cas contraire. Voici un exemple des \*'equations dont il s'agit: .LP FOR ALL p IN Primary \(ulcolour .LP (\ Contains(Take(p), p) == True; .LP FOR ALL c IN Colour .LP (\ Contains(Mix(p,c), p) == True) .LP ) .LP La partie <<== True>> de ces \*'equations peut \* | tre omise et les r\*'esultats sont appel\*'es axiomes. Des axiomes peuvent se reconna\* | tre \*`a l'absence du symbole d'\*'equivalence\ ==; ils d\*'esignent des termes qui sont \*'equivalents \*`a la valeur True (vrai) de la sorte bool\*'eenne. .LP La construction de la seconde \*'equation peut para\* | tre quelque peu forc\*'ee. Une meilleure mani\*`ere d'\*'ecrire ces \*'equations est indiqu\*'ee apr\*`es l'introduction de certaines constructions utiles. .bp .sp 1P .LP D.6.1.4.3\ \ \fIEquations conditionnelles\fR .sp 9p .RT .PP Les \*'equations conditionnelles constituent un moyen d'\*'ecrire des \*'equations qui ne sont valables que dans certaines conditions. Ces conditions sont d\*'esign\*'ees par la m\* | me syntaxe que les \*'equations non conditionnelles et sont s\*'epar\*'ees par un symbole\ ==> de l'\*'equation qui est valable si la condition est remplie. .RT .sp 1P .LP \fIExemple:\fR .sp 9p .RT .LP L'exemple type d'une \*'equation conditionnelle est la d\*'efinition de la division en type r\*'eel o\*`u: .LP FOR ALL x, z IN Real .LP (\ \ z/= 0 == True\ \ \ \ ==>\ \ \ \ (x/z) * z == x) .LP indique que, si la condition <> est valable, la division par\ z suivie de la multiplication par\ z donne la valeur originale. Cette \*'equation conditionnelle n'indique rien quant \*`a ce qui devrait arriver si une valeur de la sorte Real \*'etait divis\*'ee par\ 0. Si l'on veut sp\*'ecifier ce qui se passe en cas de division par z\*'ero, il faudrait cr\*'eer une \*'equation conditionnelle de la forme suivante: .LP FOR ALL x, z IN Real .LP (\ \ z = 0 == True\ \ \ \ ==>\ \ \ \ (x/z) * z == . | | ). .LP En pareil cas, cependant, il est recommand\*'e de placer un <> du c\* | t\*'e droit, pour faciliter la lecture. Dans le cas ci\(hydessus l'\*'equation deviendrait: .LP FOR ALL x, z IN Real .LP (\ \ (x/z) * z\ \ \ \ ==\ \ \ IF z/=0 .LP (\ \ (x/z) * z\ \ \ \ ==\ \ \ THEN x .LP (\ \ (x/z) * z\ \ \ \ ==\ \ \ ELSE . | | .LP (\ \ (x/z) * z\ \ \ \ ==\ \ \ FI .LP ) .sp 1P .LP D.6.1.5 \fIInformations compl\*'ementaires concernant les \*'equations et les\fR \fIaxiomes\fR .sp 9p .RT .PP Les deux sections qui suivent traitent de certaines difficult\*'es que l'on peut rencontrer lorsque des op\*'erateurs donnent des r\*'esultats appartenant \*`a une sorte d\*'ej\*`a d\*'efinie. Le \(sc\ D.6.1.5.3 explique la notion d'erreur en tant que terme d'une \*'equation. .RT .sp 1P .LP D.6.1.5.1\ \ \fICoh\*'erence de la hi\*'erarchie\fR .sp 9p .RT .PP En un point quelconque d'une sp\*'ecification en LDS, il existe une seule et unique d\*'efinition de type de donn\*'ees. Cette d\*'efinition de type de donn\*'ees contient les sortes, op\*'erateurs et \*'equations pr\*'ed\*'efinis et l'ensemble des sortes, op\*'erateurs et \*'equations d\*'efinis par l'utilisateur dans les d\*'efinitions de type partielles visibles en ce point. (C'est la raison pour laquelle un texte NEWTYPE\ . | | ENDNEWTYPE est appel\*'e d\*'efinition de type \fIpartielle\fR .) .PP Il en r\*'esulte certaines cons\*'equences pour les d\*'efinitions de type aux niveaux inf\*'erieurs. Cette influence sur le type pourrait \* | tre peu souhaitable. A titre d'exemple, on pourrait sp\*'ecifier de fa\*,con erron\*'ee que deux termes sont \*'equivalents, les rendant ainsi \*'equivalents alors qu'ils ne sont pas dans une port\*'ee englobante. .PP Il n'est pas admis de donner des \*'equations telles que: .RT .LP a) les valeurs d'une sorte qui sont diff\*'erentes dans une port\*'ee \*`a un niveau sup\*'erieur soient rendues \*'equivalentes; .LP b) de nouvelles valeurs soient ajout\*'ees \*`a une sorte d\*'efinie dans une port\*'ee de niveau sup\*'erieur. .PP Cela signifie par exemple que, dans un bloc au niveau du syst\*`eme, des d\*'efinitions de type partielles sp\*'ecifi\*'ees par l'utilisateur contenant un op\*'erateur ayant un r\*'esultat pr\*'ed\*'efini doivent rapporter tous les termes produits par cet op\*'erateur \*`a des valeurs de cette sorte de r\*'esultat. .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) Si, pour une raison quelconque, on donne l'axiome: .LP FOR ALL n, m IN Integer .LP (\ (Fact(n) = Fact(m))\ \ \ \ =>\ \ \ \ (n = m)) .LP afin de sp\*'ecifier que si les r\*'esultats de l'op\*'erateur Fact sont les m\* | mes, les arguments sont alors les m\* | mes. (A noter que\ => est l'implication bool\*'eenne; cela a peu de relation avec le signe d'\*'equation conditionnellle\ ==>). Ainsi, par accident, les valeurs sont unifi\*'ees. Des \*'equations des exemples pr\*'ec\*'edents on peut d\*'eduire que Fact(0)\ =\ Fact(1) et cette derni\*`ere \*'equation indique que\ 0 et\ 1 sont des notations diff\*'erentes de la m\* | me valeur. Sur la base de cette derni\*`ere \*'equation, on peut prouver que les nombres d'\*'el\*'ements de la sorte Integer sont r\*'eduits \*`a un. .bp .LP Avec l'aide d'une \*'equation conditionnelle, on peut indiquer que, pourvu que\ n et\ m ne soient pas \*'egaux \*`a\ 0, le m\* | me r\*'esultat de l'op\*'erateur Fact sur\ n et\ m implique n\ =\ m. En Led: .LP FOR ALL n, m IN Integer .LP (\ n/=0, m/=0 ==> (Fact(n) = Fact(m))\ \ \ \ =>\ \ \ \ (n = m)) .LP A noter que cette derni\*`ere \*'equation n'ajoute rien \*`a la s\*'emantique des nombres entiers; c'est un th\*'eor\*`eme qui peut \* | tre d\*'eduit des autres \*'equations. Par ailleurs, l'adjonction d'une \*'equation prouvable ne pr\*'esente pas d'inconv\*'enient. .LP b) Admettons que l'on d\*'ecouvre la n\*'ecessit\*'e d'un op\*'erateur pour les factorielles lors de la sp\*'ecification d'un type donn\*'e. Dans la d\*'efinition de type partielle de ce type, l'op\*'erateur Fact est introduit: .LP Fact:\ Integer \(hy> Integer; .LP et les \*'equations suivantes sont donn\*'ees pour d\*'efinir cet op\*'erateur: .LP Fact(0) == 1; .LP FOR ALL n IN Integer .LP (\ n > 0 ==> Fact(n) == n * Fact(n\(em1)) .LP Ces \*'equations ne d\*'efinissent pas Fact(\(em1) et ainsi, c'est un terme de la sorte Integer qui n'a pas de relation avec d'autres termes de cette sorte. En cons\*'equence, Fact(\(em1) est une nouvelle valeur de la sorte entier (et il en va de m\* | me pour Fact(\(em2), Fact(\(em3),\ etc). Cela n'est pas admis. L'exemple\ b) du \(sc\ D.6.1.5.3 donne une d\*'efinition correcte de fact. .sp 1P .LP D.6.1.5.2\ \ \fIEgalit\*'e et in\*'egalit\*'e\fR .sp 9p .RT .PP Dans chaque type, les op\*'erateurs d'\*'egalit\*'e et d'in\*'egalit\*'e sont implicites. Ainsi, si une d\*'efinition de type partielle introduit une sorte\ S, il y a alors des d\*'efinitions implicites d'op\*'erateur: .RT .LP "=": S, S \(hy> Boolean; .LP "/=": S, S \(hy> Boolean; .PP (\fIRemarque\fR \ \(em\ Les guillemets sp\*'ecifient que = et/= sont utilis\*'es comme op\*'erateurs infixes.) .PP L'op\*'erateur d'\*'egalit\*'e pr\*'esente les propri\*'et\*'es pr\*'evisibles: .PP a = a, .PP a = b => b = a, .PP a = b AND b = c => a = c, .PP a = b => a == b, .PP a = b => op(a) = op(b) for all operators op. .PP Ces propri\*'et\*'es ne sont pas \*'ecrites en syntaxe LDS et ne doivent pas \* | tre \*'enonc\*'ees dans des axiomes ou des \*'equations car elles sont implicites. La valeur bool\*'eenne obtenue lorsque cet op\*'erateur est appliqu\*'e est True (vrai) si les termes de la partie gauche et de la partie droite sont de m\* | me classe d'\*'equivalence; sinon la valeur obtenue est False (faux). S'il n'est pas explicitement sp\*'ecifi\*'e, que la valeur est True (vrai) ou False (faux), la sp\*'ecification est incompl\*`ete. .PP Pour l'op\*'erateur d'in\*'egalit\*'e, c'est par une \*'equation en LDS que l'on peut le mieux expliquer la s\*'emantique: .RT .LP FOR ALL a, b IN S .LP (\ a/= b == Not(a = b)) .PP Il n'y a pas de diff\*'erence entre l'\*'egalit\*'e et l'\*'equivalence. Deux termes qui sont \*'equivalents d\*'esignent la m\* | me valeur et l'op\*'erateur d'\*'egalit\*'e entre eux donne le r\*'esultat True (vrai). .sp 1P .LP D.6.1.5.3\ \ \fIErreur\fR .sp 9p .RT .PP On a jug\*'e n\*'ecessaire, pour les exemples qui pr\*'ec\*`edent, de sp\*'ecifier que l'application de l'op\*'erateur \*`a certaines valeurs est consid\*'er\*'ee comme une erreur. Le LDS a un moyen de le sp\*'ecifier formellement: l'\*'el\*'ement ERROR. L'erreur devrait servir \*`a exprimer: .RT .LP <>. .PP Dans la syntaxe concr\*`ete, cela est indiqu\*'e par le terme Error!, qui ne peut \* | tre utilis\*'e comme argument d'un op\*'erateur. .bp .PP Lorsque Error r\*'esulte de l'application d'un op\*'erateur et que cette application est un argument d'un autre op\*'erateur, l'application d'op\*'erateur ext\*'erieur porte \*'egalement Error dans son r\*'esultat (propagation\(hyd'erreurs). Dans un terme conditionnel, la partie THEN \fIou\fR la partie ELSE est \*'evalu\*'ee, de sorte que l'une d'elle peut \* | tre une erreur sans que celle\(hyci soit \*'evalu\*'ee (\*'etant donn\*'ee que l'autre partie de l'alternative est \*'evalu\*'ee). .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) Dans l'exemple de division de valeurs de sorte Real, les poids peuvent \* | tre remplac\*'es comme suit: .LP FOR ALL x, z IN Real .LP (\ (x/z) * z\ ==\ IF z/=0 .LP (\ (x/z) * z\ ==\ THEN \ \ \ x .LP (\ (x/z) * z\ ==\ ELSE \ \ \ Error! .LP (\ (x/z) * z\ ==\ FI .LP ) .LP Pour plus de clart\*'e, on pourrait ajouter: .LP FOR ALL x IN Real .LP (\ x/0 == Error!) .LP b) Dans l'exemple comportant l'op\*'erateur Fact, on pourrait sp\*'ecifier que l'application de cet op\*'erateur sur des entiers n\*'egatifs est consid\*'er\*'ee comme une erreur (Error). Cela permet d'\*'eviter que Fact(\(em1), Fact(\(em2),\ . | | ne deviennent de nouvelles valeurs de la sorte Integer (entier). Il conviendrait de d\*'efinir l'op\*'erateur Fact comme suit: .LP n < 0 ==> Fact(n) == Error!; .LP Fact(0) == 1; .LP n > 0 ==> Fact(n) == Fact(n\(em1) * n; .LP Ces trois lignes sont beaucoup plus claires que l'\*'equation du style programmation indiqu\*'ee ci\(hyapr\*`es. En g\*'en\*'eral, le terme conditionnel devrait \* | tre utilis\*'e s'il y a deux cas compl\*'ementaires; l'embo\* | tage de termes conditionnels rend l'\*'equation illisible, comme on peut le voir ci\(hydessous: .LP Fact(n)\ \ \ ==\ \ \ IF n > 0 .LP Fact(n)\ \ \ ==\ \ \ THEN Fact(n\(em1) * n .LP Fact(n)\ \ \ ==\ \ \ ELSE\ \ IF n = 0 .LP Fact(n)\ \ \ ==\ \ \ ELSE\ \ THEN 1 .LP Fact(n)\ \ \ ==\ \ \ ELSE\ \ ELSE Error! .LP Fact(n)\ \ \ ==\ \ \ ELSE\ \ FI .LP Fact(n)\ \ \ ==\ \ \ FI .sp 1P .LP D.6.2 \fIG\*'en\*'erateurs et h\*'eritage\fR .sp 9p .RT .PP Le pr\*'esent paragraphe traite de deux constructions qui peuvent \* | tre utilis\*'ees pour sp\*'ecifier des types ayant des parties communes. Le g\*'en\*'erateur sp\*'ecifie non un type mais un sch\*'ema, qui devient un type lorsque les sortes, op\*'erateurs, litt\*'eraux et constantes formels sont remplac\*'es par des termes r\*'eels. .PP L'h\*'eritage offre la possibilit\*'e de cr\*'eer un nouveau type en partant d'un type d\*'ej\*`a existant. Les noms de litt\*'eraux et d'op\*'erateurs peuvent \* | tre renomm\*'es et il est possible de sp\*'ecifier des litt\*'eraux, des op\*'erateurs et des \*'equations suppl\*'ementaires. .RT .sp 1P .LP D.6.2.1 \fIG\*'en\*'erateurs\fR .sp 9p .RT .PP Une d\*'efinition de g\*'en\*'erateur d\*'efinit un sch\*'ema param\*'etr\*'e par des noms formels de sortes, de litt\*'eraux, de constantes et d'op\*'erateurs. Les g\*'en\*'erateurs sont destin\*'es \*`a des types qui repr\*'esentent des <>, tels que des ensembles d'\*'el\*'ements, des cha\* | nes d'\*'el\*'ements, des fichiers d'enregistrement, des tables de consultation, des tableaux. .PP On peut l'expliquer \*`a l'aide d'un exemple pour lequel des variations peuvent \* | tre envisag\*'ees. Admettons qu'il soit n\*'ecessaire qu'un type ressemble \*`a la notion math\*'ematique d'un ensemble d'entiers. La partie suivante du texte fait partie de la d\*'efinition de type de cet ensemble d'entiers. .bp .RT .LP .rs .sp 24P .ad r \fBFigure D.6.2.1 (comme tableau) [T37.100], p. 10\fR .sp 1P .RT .ad b .RT .LP .sp 6 .PP Toutes les \*'equations ont une quantification implicite. La premi\*`ere \*'equation indique que la suppression d'un \*'el\*'ement de l'ensemble vide donne l'ensemble vide pour r\*'esultat. La seconde \*'equation indique que la suppression apr\*`es insertion du m\* | me \*'el\*'ement donne pour r\*'esultat l'ensemble tel qu'il \*'etait avant l'insertion (\*`a condition que l'ensemble ne contienne pas l'\*'el\*'ement); sinon l'ordre d'insertion et de suppression peut \* | tre interchangeable. La troisi\*`eme \*'equation indique que l'\*'el\*'ement vide ne contient pas d'\*'el\*'ements. La quatri\*`eme \*'equation indique qu'un \*'el\*'ement se trouve dans un ensemble s'il est le dernier \*'el\*'ement ajout\*'e ou s'il se trouvait dans l'ensemble avant l'adjonction du dernier \*'el\*'ement. La derni\*`ere \*'equation indique que l'ordre d'addition des \*'el\*'ements ne fait aucune diff\*'erence. .PP Dans l'exemple de la figure D\(hy6.2.1 Int \(ulset (ensemble \(uld'entiers) n'est qu'un exemple d'un ensemble et si l'on a \*'egalement besoin d'un PId \(ulset, d'un Subscriber \(ulset (ensemble \(uld'abonn\*'es) et d'un Exchange \(ulname \(ulset (ensemble \(ulde \(ulnoms \(ulde \(ulcentral) dans la sp\*'ecification, personne ne sera surpris qu'il contienne tous les op\*'erateurs Add (ajouter), Delete (supprimer) et Is \(ulin (est \(uldans) et un litt\*'eral pour l'ensemble vide. Les \*'equations donn\*'ees pour ces op\*'erateurs facilitent la g\*'en\*'eralisation \*`a d'autres ensembles. .PP Tel est le cas o\*`u la notion de g\*'en\*'erateur se r\*'ev\*`ele utile; le texte commun peut \* | tre donn\*'e une fois et \* | tre utilis\*'e plusieurs fois. La figure\ D\(hy6.2.2 pr\*'esente le g\*'en\*'erateur. (A noter que les noms de sortes formels sont introduits par le mot cl\*'e TYPE, cela uniquement pour des raisons d'ordre historique.) .RT .PP Au lieu d'utiliser Integer (entier), on utilise le type formel Item et, pour pouvoir donner diff\*'erents noms \*`a l'ensemble entier vide et aux ensembles vides dans d'autres types, on fait \*'egalement de ce litt\*'eral un param\*`etre formel. .bp .RT .LP .rs .sp 24P .ad r \fBFigure D.6.2.2 (comme tableau) [T38.100], p. 11\fR .sp 1P .RT .ad b .RT .PP .sp 1 Avec ce g\*'en\*'erateur, le type Int \(ulset peut \* | tre construit comme suit: .RT .LP NEWTYPE Int \(ulset Set (Integer, empty \(ulint \(ulset) .LP ENDNEWTYPE Int \(ulset; .PP Si l'on compare les figures D\(hy6.2.1 et D\(hy6.2.2, on constate que: .LP a) GENERATOR et ENDGENERATOR sont remplac\*'es par NEWTYPE et ENDNEWTYPE respectivement; .LP b) les param\*`etres formels de g\*'en\*'erateur (le texte entre parenth\*`eses apr\*`es le nom de g\*'en\*'erateur) sont supprim\*'es; .LP c) Set, Item et empty \(ulset sont remplac\*'es dans tout le g\*'en\*'erateur par Int \(ulset, Integer et empty \(ulint \(ulset, respectivement. .PP Ainsi, il n'y a en fait aucune diff\*'erence entre cet Int \(ulset et celui de la figure\ D\(hy6.2.1, mais\ . | | .LP \(em si l'on a besoin d'un ensemble de valeurs Pid, on peut cr\*'eer le type \*`a l'aide de: .LP NEWTYPE PId\(hyset Set(PId, empty \(ulpid \(ulset) .LP ENDNEWTYPE PId \(ulset; .LP \(em si l'on a besoin d'un ensemble d'abonn\*'es, dans lequel les abonn\*'es sont repr\*'esent\*'es par un type introduisant la sorte Subscr, l'ensemble d'abonn\*'es peut \* | tre cr\*'e\*'e \*`a l'aide de: .LP NEWTYPE Subscr \(ulset Set(Subscr, empty \(ulsubscr \(ulset) .LP ENDNEWTYPE Subscr \(ulset; .LP Cela permet d'\*'economiser du papier, de plus, le travail est facilit\*'e parce qu'il suffit de penser une fois aux ensembles et que ce travail peut \* | tre d\*'el\*'egu\*'e \*`a des sp\*'ecialistes qualifi\*'es sur les types de donn\*'ees abstraites. .bp .sp 1P .LP \fIExemple:\fR .sp 9p .RT .LP Cet exemple montre un g\*'en\*'erateur utilisant une sorte, un op\*'erateur, un litt\*'eral et une constante formels. Il d\*'ecrit une rang\*'ee d'\*'el\*'ements ayant une longueur maximale max \(ullength. La sorte comprend un litt\*'eral d\*'esignant la rang\*'ee vide et les op\*'erateurs pour insertion et suppression d'\*'el\*'ements dans une rang\*'ee ou de celle\(hyci, l'encha\* | nement de rang\*'ees, le choix d'une sous\(hyrang\*'ee et la d\*'etermination de la longueur d'une rang\*'ee. Ce dernier op\*'erateur est rendu formel ce qui permet de la nommer \*`a nouveau. .LP GENERATOR Row (TYPE Item, OPERATOR Length, LITERAL Empty, .LP \ \ \ \ \ \ \ \ \ \ \ \ CONSTANT max \(ullength) .LP \ \ LITERALS Empty .LP \ \ OPERATORS .LP \ \ \ \ Length: Row \(hy> Integer; .LP \ \ \ \ Insert: Row, Item, Integer \(hy> Row; .LP \ \ \ \ Delete: Row, Integer, Integer \(hy> Row; .LP \ \ \ \ "//": Row, Row \(hy> Row; .LP \ \ \ \ Select: Row, Integer, Integer \(hy> Row .LP \ \ \ \ /* and other operators relevant for rows of items */ .LP \ \ AXIOMS .LP \ \ \ \ /* The equations for the operators above, among * .LP \ \ \ \ / * which the following two (or equivalents) */ .LP \ \ \ \ Length(r) = max \(ullength ==> Insert(r, itm, int) == Error!; .LP \ \ \ \ Length(r1) + Length(r2) > max \(ullength ==> r1//r2 == Error! .LP ENDGENERATOR Row; .LP A noter que l'op\*'erateur formel Length (longueur) et le litt\*'eral Empty (vide) sont donn\*'es une fois de plus dans le corps du g\*'en\*'erateur parce qu'ils sont renomm\*'es lors de leur instantiation. Dans le cas de l'op\*'erateur, les arguments et la sorte de r\*'esultat ne sont donn\*'es que dans le corps. Le g\*'en\*'erateur Row (rang\*'ee) peut servir \*`a faire des lignes, des pages et des livres, comme suit: .LP NEWTYPE Line Row(Character, Width, Empty \(ulline, 80) .LP ENDNEWTYPE Line; .LP NEWTYPE Page Row(Line, Length, Empty \(ulpage, 66) .LP ENDNEWTYPE Page; .LP NEWTYPE Book Row(Page, Nr \(ulof \(ulpages, Empty \(ulbook,\ 10000) .LP ENDNEWTYPE Book; .sp 1P .LP D.6.2.2 \fIH\*'eritage\fR .sp 9p .RT .PP L'h\*'eritage constitue un moyen d'\*'etablir toutes les valeurs de la sorte dite parente, certains ou tous les op\*'erateurs du type parent et toutes les \*'equations du type parent. Pour les litt\*'eraux et les op\*'erateurs, il existe une possibilit\*'e de les nommer \*`a nouveau. En g\*'en\*'eral, c'est une m\*'ethode satisfaisante parce que, dans ce cas, le lecteur peut d\*'eduire du contexte qu'il s'agit d'un autre type, m\* | me si les litt\*'eraux sont les m\* | mes. .PP Si un op\*'erateur n'est pas h\*'erit\*'e, on lui attribue syst\*'ematiquement un autre nom inaccessible \*`a l'utilisateur. Le fait que les op\*'erateurs sont encore pr\*'esents signifie que toutes les \*'equations du type parent sont encore pr\*'esentes (avec des op\*'erateurs portant un autre nom). Cela garantit que les valeurs parentes sont h\*'erit\*'ees. .PP Avec la possibilit\*'e d'emp\* | cher l'utilisation d'un op\*'erateur (lorsqu'il n'est pas h\*'erit\*'e), on assure la possibilit\*'e d'ajouter de nouveaux op\*'erateurs. Apr\*`es le mot cl\*'e ADDING, on peut donner des litt\*'eraux, des op\*'erateurs et des \*'equations comme dans un type ordinaire. Toutefois, il faut faire attention aux nouveaux litt\*'eraux et aux confusions possibles entre op\*'erateurs h\*'erit\*'es et ajout\*'es. .PP Lorsque les litt\*'eraux sont ajout\*'es, le r\*'esultat des op\*'erateurs h\*'erit\*'es, appliqu\*'es \*`a des nouveaux litt\*'eraux, doit \* | tre d\*'efini (par des \*'equations). Lorsque des op\*'erateurs sont ajout\*'es, il ne faut pas oublier les op\*'erateurs nomm\*'es \*`a nouveau de mani\*`ere invisible et les \*'equations associ\*'ees. Les \*'equations de d\*'efinition des op\*'erateurs ajout\*'es devraient \* | tre compatibles avec les \*'equations comportant des op\*'erateurs h\*'erit\*'es et non h\*'erit\*'es. .bp .PP Apr\*`es cette liste d'avertissements, prenons quelques exemples: .RT .LP a) Supposons que le newtype couleur est complet et disponible. Ce type est fond\*'e sur le choix et le m\*'elange de faisceaux de lumi\*`ere de couleur primaire. Il faudrait de longues r\*'eflexions et un long texte et/ou copie pour d\*'efinir quelque chose de semblable pour le choix et le m\*'elange de peinture. .LP Une solution commode \*`a ce probl\*`eme consiste \*`a faire du newtype Colour (couleur) un g\*'en\*'erateur en effectuant uniquement deux remplacements: .LP 1) la premi\*`ere ligne .LP \ \ NEWTYPE Colour .LP devient .LP \ \ GENERATOR Colour (TYPE Primary \(ulcolour) .LP 2) le mot\(hycl\*'e ENDNEWTYPE devient ENDGENERATOR. .LP On peut maintenant nommer \*`a nouveau le g\*'en\*'erateur lorsqu'il est instanci\*'e. Supposons que la sorte ant\*'erieure Primary \(ulcolour soit appel\*'ee Light \(ulprimary, et que la sorte Paint \(ulprimary soit d\*'efinie comme: .LP NEWTYPE Paint \(ulprimary .LP \ \ LITERALS Red, Yellow, Blue .LP ENDNEWTYPE Paint \(ulprimary; .PP Il est maintenant tr\*`es facile de d\*'efinir deux types similaires, un pour la lumi\*`ere et un pour la peinture: .LP NEWTYPE Light \(ulcolours Colour (Light \(ulprimary) ENDNEWTYPE; .LP NEWTYPE Paint \(ulcolours Colour (Paint \(ulprimary) ENDNEWTYPE; .PP Il n'y a pas de probl\*`eme jusqu'ici, mais comment peut\(hyon voir la diff\*'erence entre Take (Red) de Light \(ulcolour et celui de Paint \(ulcolour avec la m\* | me syntaxe? S'il est n\*'ecessaire de distinguer entre ces deux termes, on peut avoir recours \*`a l'h\*'eritage. Au lieu de Light \(ulcolours et Paint \(ulcolours, les types Light (lumi\*`ere) et Palette sont d\*'efinis par h\*'eritage et le nom de l'op\*'erateur Take (prendre) est modifi\*'e: .LP NEWTYPE Light .LP \ \ INHERITS Light \(ulcolours .LP \ \ OPERATORS (Beam=Take, Mix, Contains) .LP \ \ ADDING .LP \ \ \ \ LITERALS White .LP \ \ \ \ AXIOMS .LP \ \ \ \ \ \ White == Mix (Red, Mix (Yellow, Beam (Blue))) .LP ENDNEWTYPE Light; .LP Maintenant le newtype Light (lumi\*`ere) a les litt\*'eraux de Light \(ulcolours et le litt\*'eral White (blanc). Light \(ulcolours n'a pas de litt\*'eraux qui lui soient propres (car il utilise les litt\*'eraux de Light \(ulprimary), de sorte que White est le seul litt\*'eral de Light. Les op\*'erateurs et les \*'equations de Light sont les m\* | mes que ceux de Light \(ulcolours, \*`a l'exception du fait que le nom d'op\*'erateur Take est remplac\*'e par Beam (faisceau) et que l'\*'equation pour White a \*'et\*'e ajout\*'ee. L'axiome ajout\*'e indique que ce litt\*'eral ajout\*'e devient un \*'el\*'ement de l'ensemble de termes dans lequel les trois couleurs primaires sont m\*'elang\*'ees. .LP Le newtype Palette a les litt\*'eraux de Paint \(ulcolours et l'op\*'erateur Take est remplac\*'e par Paint (peinture): .LP NEWTYPE Palette .LP \ \ INHERITS Paint \(ulcolours .LP \ \ OPERATORS (Paint \(ulTake, Mix, Contains) .LP ENDNEWTYPE Palette; .LP b) Admettons que l'on veuille \*'etendre l'ensemble de types entiers (sorte Int \(ulset), introduit dans la section pr\*'ec\*'edente, par un op\*'erateur qui trouve le plus petit entier de l'ensemble. Tout d'abord, il faut se demander si cet op\*'erateur peut \* | tre introduit dans la d\*'efinition de g\*'en\*'erateur pour le rendre disponible \*`a tous les ensembles et autres choses. .bp .LP S'il est vrai que cela peut \* | tre fait, cela limiterait l'\*'el\*'ement \*`a la d\*'efinition de > et <. Cela ne convient pas \*`a tous les \*'el\*'ements (PId par exemple) et il peut \* | tre pr\*'ef\*'erable de cr\*'eer un newtype ayant la sorte New \(ulint \(ulset comportant un op\*'erateur Min. .LP NEWTYPE New \(ulint \(ulset .LP \ \ INHERITS Int \(ulset .LP \ \ OPERATORS ALL .LP \ \ ADDING .LP \ \ \ \ OPERATORS .LP \ \ \ \ \ \ Min: New \(ulint \(ulset\(hy> Integer .LP \ \ \ \ AXIOMS .LP \ \ \ \ \ \ Min(Empty \(ulint \(ulset) == Error!; .LP \ \ \ \ \ \ Min(Add(Empty \(ulint \(ulset, x))==x; .LP \ \ \ \ \ \ Min(Add(Add(nis,x),y))== .LP \ \ \ \ \ \ \ \ IF y >); .LP b) tous les \*'enonc\*'es vrais peuvent \* | tre tir\*'es des \*'equations. Ils sont soit indiqu\*'es comme des axiomes, soit d\*'eduits par substitution de termes \*'equivalents dans les \*'equations; .LP c) aucune incoh\*'erence doit \* | tre d\*'ecel\*'ee, c'est\(hy\*`a\(hydire que l'on ne peut d\*'eduire des \*'equations que Vrai\ =\ Faux. .PP Une proc\*'edure permettant de trouver des \*'equations peut \* | tre exprim\*'ee en LDS informel, comme indiqu\*'e dans la figure\ D\(hy6.3.1. .sp 1P .LP D.6.3.2 \fIApplication de fonctions aux\fR \fIconstructeurs\fR .sp 9p .RT .PP D'une mani\*`ere g\*'en\*'erale, l'ensemble d'op\*'erateurs poss\*`ede un sous\(hyensemble d'op\*'erateurs appel\*'es <> et <>. Les constructeurs peuvent servir \*`a g\*'en\*'erer toutes les valeurs (classes d'\*'equivalence) de la sorte. Dans cette approche, les litt\*'eraux sont consid\*'er\*'es comme des op\*'erateurs sans argument. .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) le type bool\*'een a ses litt\*'eraux pour constructeurs; .LP b) le type naturel a le litt\*'eral 0 et l'op\*'erateur Next comme constructeurs; un naturel quelconque peut \* | tre construit seulement avec\ 0 et\ Next; .LP c) le g\*'en\*'erateur pour les ensembles a le litt\*'eral ensemble \(ulvide et l'op\*'erateur \(uladditif comme constructeurs; un ensemble quelconque ne peut \* | tre construit qu'en utilisant Empty \(ulset (ensemble \(ulvide) et Add (ajouter); .LP d) le type entier peut \* | tre construit au moyen des litt\*'eraux 0 et\ 1, des op\*'erateurs\ + et moins unaires. .bp .LP .rs .sp 33P .ad r \fBFigura D\(hy6.3.1, (N), p. 12\fR .sp 1P .RT .ad b .RT .PP A noter qu'il y a parfois plusieurs choix possibles pour l'ensemble de constructeurs. Tout choix sera valable pour le reste de la pr\*'esente section mais les petits ensembles sont g\*'en\*'eralement les meilleurs. .PP Ensuite, les fonctions sont trait\*'ees une par une. Pour chaque argument d'une fonction, seuls sont \*'enum\*'er\*'es tous les termes possibles compos\*'es de constructeurs. Pour \*'eviter le probl\*`eme que posent les nombres infinis de termes, il faut appliquer la quantification. .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) Pour les nombres naturels, cette liste peut \* | tre r\*'eduite \*`a: .LP 0 .LP Next (n) o\*`u n est tout nombre naturel. .LP b) Pour les ensembles, la liste \*'eventuelle peut \* | tre: .LP empty \(ulset .LP Add (s,i) o\*`u s est tout ensemble et i tout \*'el\*'ement (item). .PP Si, dans le terme de droite d'une \*'equation ayant (s,i) du c\* | t\*'e gauche, il y a une diff\*'erence entre s \*'etant vide ou n'\*'etant pas vide, on peut r\*'e\*'ecrire la liste comme suit: .LP empty \(ulset .LP Add (empty \(ulset,i) o\*`u i est un \*'el\*'ement (item) quelconque, .LP Add (Add (s,i),j) o\*`u s est un ensemble quelconque et i, j, un \*'el\*'ement quelconque. .bp .PP Apr\*`es la cr\*'eation de cette liste, on obtient les parties de gauche des \*'equations en appliquant chaque fonction \*`a une combinaison d'arguments tir\*'es de la liste. Les identificateurs de valeurs de diff\*'erents arguments re\*,coivent des noms diff\*'erents. La proc\*'edure indiqu\*'ee ci\(hydessus pour les fonctions peut \* | tre appliqu\*'ee aux constructeurs; dans ce cas, elle donne les relations entre des termes o\*`u les constructeurs sont utilis\*'es dans diff\*'erents ordres. .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP a) Pour l'op\*'erateur de multiplication de nombres naturels portant la signature .LP <<*>>:Natural, Natural \(hy> Natural .LP Cette proc\*'edure donne la partie de gauche des \*'equations (incompl\*`etes) suivantes. L'utilisateur devra ajouter la partie de droite. .LP Next (n) 0*0 == . | | ; .LP Next (n) 0*Next (n) == . | | ; .LP Next (n)*0 == . | | ; .LP Next (n)*Next (m) == . | | ; .LP b) Pour les op\*'erateurs Is \(ulin (est \(uldans) et Delete (supprimer, dans le g\*'en\*'erateur Set (voir le \(sc\ D.6.2.1), cette approche est d\*'ej\*`a appliqu\*'ee. .LP c) Pour la sorte Colour, les constructeurs sont Take et Mix. Un op\*'erateur analogue \*`a Contains dans le \(sc\ D.6.1.4.2 doit \* | tre d\*'efini pour les arguments. .LP Take(p) o\*`u p est toute couleur primaire .LP Mix(p,c) o\*`u p est toute couleur primaire et c une couleur quelconque. .LP Etant donn\*'e que l'on avait annonc\*'e au \(sc D.6.1.4.2 que les \*'equations compl\*`etes seraient donn\*'ees pour cet op\*'erateur: .LP Contains(Take(p),q) ==p=q; .LP Contains(Mix(p,c),q) ==(p=q) OR Contains(c,q); .PP Cette proc\*'edure de construction peut donner plus d'\*'equations que cela n'est n\*'ecessaire, mais elle est tr\*`es s\* | re. Dans l'exemple susmentionn\*'e de multiplication des nombres naturels, il est vraisemblable que la propri\*'et\*'e de commutativit\*'e de la multiplication sera indiqu\*'ee et qu'en cons\*'equence, seule la derni\*`ere (ou la seconde) \*'equation des trois premi\*`eres sera n\*'ecessaire. .PP La proc\*'edure d\*'ecrite dans cette section peut \* | tre appliqu\*'ee en combinaison avec la proc\*'edure d\*'ecrite dans la section pr\*'ec\*'edente, o\*`u elle est utile pour la t\* | che <>. .RT .sp 1P .LP D.6.3.3 \fISp\*'ecification d'ensemble d'essai\fR .sp 9p .RT .PP On peut aussi consid\*'erer les \*'equations du point de vue de la mise en oeuvre. Si les op\*'erateurs sont mis en oeuvre sous la forme de fonctions dans un langage de programmation, les \*'equations montrent comment ces fonctions doivent \* | tre test\*'ees. .PP Il convient d'\*'evaluer les expressions correspondant \*`a la partie de gauche d'une \*'equation, de faire de m\* | me pour la partie droite de cette \*'equation et de voir si elles sont \*'equivalentes. C'est la construction FOR ALL qui pourrait poser certains probl\*`emes. Ceux\(hyci peuvent souvent \* | tre r\*'esolus de mani\*`ere pragmatique: .RT .LP Au lieu de tif de test peut utiliser \ \ FOR ALL i IN Integer .LP le dispositif de test peut utiliser\ \ FOR ALL i IN { (em10,\(em1,0,1,1 } et proc\*'eder ainsi dans la plupart des cas. .PP Consid\*'erer des \*'equations comme n\*'ecessaires \*`a la mise en oeuvre peut \* | tre utile pour ce qui est de la t\* | che <> dans la proc\*'edure du \(sc\ D.6.3.1. .sp 1P .LP D.6.4 \fICaract\*'eristiques\fR .sp 9p .RT .PP La pr\*'esente section d\*'ecrit certains dispositifs du LDS qui sont rarement n\*'ecessaires dont on peut pratiquement se passer, mais qui rendent quelquefois la t\* | che plus facile. .RT .sp 1P .LP D.6.4.1 \fIOp\*'erateurs cach\*'es\fR .sp 9p .RT .PP Il arrive que l'ensemble des \*'equations puisse \* | tre simplifi\*'e ou rendu plus lisible gr\* | ce \*`a l'introduction d'un op\*'erateur suppl\*'ementaire, mais cet op\*'erateur ne devrait pas \* | tre utilis\*'e dans les processus. Cela signifie que l'op\*'erateur est visible de l'int\*'erieur mais cach\*'e en dehors de la d\*'efinition de type. .bp .PP On peut atteindre ce r\*'esultat en d\*'efinissant un <>, c'est\(hy\*`a\(hydire un type que l'utilisateur ne doit pas employer. A partir de ce type cach\*'e, l'utilisateur peut h\*'eriter de tous les op\*'erateurs auxquels il peut avoir acc\*`es; c'est le type h\*'erit\*'e qui doit \* | tre utilis\*'e. On peut s'assurer qu'il est correctement employ\*'e en examinant toutes les d\*'eclarations de variables (aucune variable de sorte introduite par le type cach\*'e ne doit appara\* | tre). .PP Ce qui caract\*'erise les op\*'erateurs cach\*'es, c'est qu'ils peuvent \* | tre atteints par une restriction de leur visibilit\*'e aux seules \*'equations. On peut le faire en pla\*,cant un point d'exclamation apr\*`es l'op\*'erateur. .RT .sp 1P .LP \fIExemple:\fR .sp 9p .RT .PP La mani\*`ere courante de faire un ensemble d'un \*'el\*'ement \*`a partir du g\*'en\*'erateur Set est la suivante: .RT .LP Add(empty \(ulset,x) .LP et c'est ainsi que doit le faire chaque utilisateur. Dans les \*'equations, le sp\*'ecificateur peut utiliser un op\*'erateur sp\*'ecial, par exemple: .LP Mk \(ulset!:Item\(hy>Set; .LP d\*'efini par l'\*'equation: .LP Mk \(ulset!(itm) == Add(empty \(ulset,itm); .LP qui peut \* | tre utilis\*'e dans des d\*'efinitions de type partiel mais non dans le corps de processus en LDS. .sp 1P .LP D.6.4.2 \fIRelations d'ordre\fR .sp 9p .RT .PP Lorsqu'il faut sp\*'ecifier une relation d'ordre sur les \*'el\*'ements d'une sorte, cela signifie en g\*'en\*'eral qu'il faut d\*'efinir quatre op\*'erateurs (<,<=,>,>=) et les propri\*'et\*'es math\*'ematiques ordinaires (transitivit\*'e, etc.). S'il y a de nombreux litt\*'eraux, il faut \*'egalement donner de nombreuses \*'equations. Par exemple, le type de donn\*'ees pr\*'ed\*'efinies Character est d\*'efini de cette mani\*`ere. .PP Le LDS comporte une caract\*'eristique qui permet d'abr\*'eger ces d\*'efinitions de type longues, peu lisibles et ennuyeuses: c'est l'abr\*'eviation ORDERING (relation d'ordre). .PP ORDERING est donn\*'e dans la liste d'op\*'erateurs, de pr\*'ef\*'erence au d\*'ebut ou \*`a la fin de celle\(hyci. Cela permet d'introduire des op\*'erateurs de relation d'ordre et les \*'equations normales. Lorsque ORDERING est sp\*'ecifi\*'e, il faut donner les litt\*'eraux, s'il en existe, dans l'ordre ascendant. .RT .sp 1P .LP \fIExemple:\fR .sp 9p .RT .LP NEWTYPE Even \(uldecimal \(uldigit .LP \ \ LITERALS 0,2,4,6,8 .LP \ \ OPERATORS .LP \ \ \ \ ORDERING .LP ENDNEWTYPE Even \(uldecimal \(uldigit; .PP Maintenant, l'ordre 0<2<4<6<8 est implicite. .PP Au \(sc D.6.2.2 (H\*'eritage), on soulignait qu'il fallait s'assurer que les litt\*'eraux \*'etaient ajout\*'es \*`a une sorte h\*'erit\*'ee. Il convient d'en indiquer ici la raison. .PP Admettons que l'on d\*'esire l'extension suivante de la sorte Even \(uldecimal \(uldigit: .RT .LP NEWTYPE Decimal \(uldigit .LP \ \ INHERITS Even \(uldecimal \(uldigit .LP \ \ OPERATORS ALL .LP \ \ ADDING .LP \ \ \ \ LITERALS 1,3,5,7,9 .LP \ \ \ \ AXIOMS .LP \ \ \ \ \ \ 0<1; 1<2; .LP \ \ \ \ \ \ 2<3; 3<4; .LP \ \ \ \ \ \ 4<5; 5<6; .LP \ \ \ \ \ \ 6<7; 7<8; .LP \ \ \ \ \ \ 8<9 .LP ENDNEWTYPE Decimal \(uldigit; .bp .PP Les axiomes donn\*'es ici ne peuvent \* | tre omis. Sans ces axiomes, il ne peut y avoir qu'un ordre dit partiel: .LP 0<2<4<6<8 .LP et .LP 1<3<5<7<9. .PP Avec les axiomes ci\(hydessus, on obtient un ordre complet: .LP 0<1<2<3<4<5<6<7<8<9 .LP mais avec l'axiome <<9<0>> au lieu de l'ensemble d'axiomes ci\(hydessus, l'ordre complet serrait le suivant: .LP 1<3<5<7<9<0<2<4<6<8. .sp 1P .LP D.6.4.3 \fISortes avec champs\fR .sp 9p .RT .PP Comme indiqu\*'e au \(sc 5.4.1.10 de la Recommandation, on peut d\*'efinir une sorte structur\*'ee sans constructions sp\*'eciales, mais les sortes structur\*'ees sont \*`a la fois courantes et utiles, ce qui justifie certaines constructions suppl\*'ementaires dans le langage. .PP Une sorte structur\*'ee devrait \* | tre utilis\*'ee lorsqu'une valeur d'objet est form\*'ee par l'association de valeurs de plusieurs sortes. Chaque valeur de cette association est caract\*'eris\*'ee par un nom, appel\*'e nom de champ. La sorte d'un champ est fixe. .RT .sp 1P .LP \fIExemples:\fR .sp 9p .RT .LP NEWTYPE Subscriber .LP \ \ STRUCT numbers Number \(ulkey; .LP \ \ \ \ \ \ name Name \(ulkey; .LP \ \ \ \ \ \ admin Administrative; .LP ENDNEWTYPE Subscriber; .LP NEWTYPE Name \(ulkey .LP \ \ STRUCT name, .LP \ \ \ \ \ \ street Charstring; .LP \ \ \ \ \ \ number Integer; .LP \ \ \ \ \ \ city Charstring; .LP ENDNEWTYPE Name \(ulKey; .PP Avec une sorte structur\*'ee, certains op\*'erateurs sont d\*'efinis implicitement: .LP a) l'op\*'erateur constructeur, <<(.<>.)>> apr\*`es les valeurs de champ; .LP b) les op\*'erateurs de s\*'election de champ, les variables de la sorte structur\*'ee suivies par un ! et le nom de champ, ou suivies par le nom de champ entre parenth\*`eses. Il ne faut pas confondre la variable suivie d'un ! avec l'op\*'erateur cach\*'e (\(sc\ D.6.4.1). .PP On trouvera un exemple dans la figure D\(hy6.4.1. .LP .rs .sp 12P .ad r \fBFigure D.6.4.1 (comme tableau) [T39.100], p. 13\fR .sp 1P .RT .ad b .RT .LP .bp .sp 1P .LP D.6.4.4 \fISortes index\*'ees\fR .sp 9p .RT .PP Une sorte index\*'ee est une sorte pour laquelle le type a pour nom d'op\*'erateur Extract! (extraction). Dans les types de donn\*'ees pr\*'ed\*'efinies, le g\*'en\*'erateur Array est un tel type. Array est l'un des exemples les plus courants de type index\*'e. .PP Pour l'op\*'erateur cach\*'e Extract!, il existe une syntaxe concr\*`ete sp\*'eciale qui doit \* | tre appliqu\*'ee en dehors des d\*'efinitions de type. .PP On peut penser que le type Index dans le g\*'en\*'erateur pr\*'ed\*'efini Array doit \* | tre un type <> comme Integer, Natural ou Character. Toutefois, il n'y a pas de raison pour qu'une structure comme Name \(ulkey ne puisse pas \* | tre utilis\*'ee comme Index. .RT .sp 1P .LP \fIExemple:\fR .sp 9p .RT .LP NEWTYPE Subsc \(uldata \(ulbase .LP \ \ Array (Name \(ulkey, Subscriber) .LP ENDNEWTYPE Subsc \(uldata \(ulbase; .PP Les sortes Name \(ulkey et Subscriber sont celles qui ont \*'et\*'e d\*'efinies dans la section pr\*'ec\*'edente. Supposons qu'il existe une proc\*'edure Bill comportant un param\*`etre de sorte Subscriber et que cette proc\*'edure soit d\*'efinie dans un processus qui comporte aussi une variable Sub \(uldb de la sorte Subsc \(uldata \(ulbase. Dans ce processus, l'appel suivant pourrait appara\* | tre. .LP CALL Bill (Sub \(uldb) (. `P.M.`, `Downingstreet`10. `Londres`.))); .sp 1P .LP D.6.4.5 \fIValeur par d\*'efaut de variables\fR .sp 9p .RT .PP Comme indiqu\*'e dans la section concernant la d\*'eclaration de variables (\(sc\ D.3.10.1), il est possible d'affecter des valeurs \*`a une variable imm\*'ediatement apr\*`es la d\*'eclaration. Cependant, certains types ont une valeur qui sera (presque) toujours la valeur initiale d'une variable. Il existe une caract\*'eristique qui permet d'\*'eviter d'\*'ecrire la valeur initiale pour chaque d\*'eclaration: la clause DEFAULT. .PP A titre d'exemple, on peut consid\*'erer l'ensemble. Il est tr\*`es probable que presque toutes les variables, de tout ensemble imaginaire, seront initialis\*'ees avec empty \(ulset. .PP La notation: .RT .LP DEFAULT empty \(ulset .LP apr\*`es la liste d'\*'equations indique que chaque variable de chaque instantiation de ce g\*'en\*'erateur sera initialis\*'ee \*`a la valeur empty \(ulset de cette instantiation, sauf s'il y a une initialisation explicite (voir le \(sc\ D.3.10.1.) .PP S'il n'est par s\* | r que la valeur initiale de toutes les variables d'une sorte soit la m\* | me, il ne faut pas utiliser la clause DEFAULT, sinon il est difficile d'\*'eviter des surprises. .sp 1P .LP D.6.4.6 \fIOp\*'erateurs actifs\fR .sp 9p .RT .PP Les utilisateurs qui connaissent la Recommandation Z.104 de 1984 concernant le LDS pourraient se demander ce qui est arriv\*'e aux op\*'erateurs dits actifs. En fait, cette caract\*'eristique a \*'et\*'e supprim\*'ee, pour les raisons suivantes: .RT .LP a) elle n'est pas n\*'ecessaire car les op\*'erateurs courants et les proc\*'edures et/ou macros offrent la m\* | me capacit\*'e d'expression; .LP b) elle compromet la lisibilit\*'e des \*'equations; .LP c) de nombreux utilisateurs ont eu des difficult\*'es \*`a l'utiliser correctement; .LP d) elle ne s'int\*`egre pas au mod\*`ele de type de donn\*'ees abstrait fond\*'e sur les alg\*`ebres initiales qui constituent le mod\*`ele choisi comme base math\*'ematique de cette partie du LDS. .LP .rs .sp 6P .sp 2P .LP \fBMONTAGE: \(sc D.7 SUR LE RESTE DE CETTE PAGE\fR .sp 1P .RT .LP .bp