Definition of Add_an_Invariant, a Specification Construction Process Operator
Identifieur interne : 000A41 ( Crin/Corpus ); précédent : 000A40; suivant : 000A42Definition of Add_an_Invariant, a Specification Construction Process Operator
Auteurs : N. LévySource :
English descriptors
- KwdEn :
Abstract
A specification construction process can be formalized by composition of operators allowing the construction, modification, reuse and observation of a specification. The inheritance mechanism first introduced within the object-oriented languages can be defined within algebraic languages by a familly of such operators. One of those allows the reuse of a type by restriction of its objects to the ones verifying a given property called an invariant. To add an invariant to an algebraic specification means to keep among the specified objects only some of them, the ones verifying the invariant. But the behaviour of the operations must be preserved. The operator Add_an_Invariant is defined and an application example is given that derives the specification of a continuum system from the one of a mail system. A property ensuring the resulting specification to have the required properties is introduced.
Links to Exploration step
CRIN:levy90aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="519">Definition of Add_an_Invariant, a Specification Construction Process Operator</title></titleStmt><publicationStmt><idno type="RBID">CRIN:levy90a</idno><date when="1990" year="1990">1990</date><idno type="wicri:Area/Crin/Corpus">000A41</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Definition of Add_an_Invariant, a Specification Construction Process Operator</title><author><name sortKey="Levy, N" sort="Levy, N" uniqKey="Levy N" first="N." last="Lévy">N. Lévy</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>algabraic specification of abstract data types</term><term>inheritance specification derivation</term><term>invariant</term><term>process operators</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="3989">A specification construction process can be formalized by composition of operators allowing the construction, modification, reuse and observation of a specification. The inheritance mechanism first introduced within the object-oriented languages can be defined within algebraic languages by a familly of such operators. One of those allows the reuse of a type by restriction of its objects to the ones verifying a given property called an invariant. To add an invariant to an algebraic specification means to keep among the specified objects only some of them, the ones verifying the invariant. But the behaviour of the operations must be preserved. The operator Add_an_Invariant is defined and an application example is given that derives the specification of a continuum system from the one of a mail system. A property ensuring the resulting specification to have the required properties is introduced.</div></front></TEI><BibTex type="techreport"><ref>levy90a</ref><crinnumber>90-R-222</crinnumber><category>13</category><equipe>PROGRAIS</equipe><author><e>Lévy, N.</e></author><title>Definition of Add_an_Invariant, a Specification Construction Process Operator</title><institution>Centre de Recherche en Informatique de Nancy</institution><year>1990</year><note>ICARUS ESPRIT Project 2537</note><keywords><e>process operators</e><e>invariant</e><e>inheritance specification derivation</e><e>algabraic specification of abstract data types</e></keywords><abstract>A specification construction process can be formalized by composition of operators allowing the construction, modification, reuse and observation of a specification. The inheritance mechanism first introduced within the object-oriented languages can be defined within algebraic languages by a familly of such operators. One of those allows the reuse of a type by restriction of its objects to the ones verifying a given property called an invariant. To add an invariant to an algebraic specification means to keep among the specified objects only some of them, the ones verifying the invariant. But the behaviour of the operations must be preserved. The operator Add_an_Invariant is defined and an application example is given that derives the specification of a continuum system from the one of a mail system. A property ensuring the resulting specification to have the required properties is introduced.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000A41 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 000A41 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:levy90a
|texte= Definition of Add_an_Invariant, a Specification Construction Process Operator
}}
| This area was generated with Dilib version V0.6.33. |  |