On hierarchies of abstract data types
Identifieur interne : 003823 ( Istex/Checkpoint ); précédent : 003822; suivant : 003824On hierarchies of abstract data types
Auteurs : Martin Wirsing [Allemagne] ; Peter Pepper [Allemagne] ; Helmut Partsch [Allemagne] ; Walter Dosch [Allemagne] ; Manfred Broy [Allemagne]Source :
- Acta Informatica [ 0001-5903 ] ; 1983-10-01.
English descriptors
- Teeft :
- Abstract data types, Abstract type, Abstract types, Additional properties, Algebra, Algebraic, Algebraic specification, Algebraic specifications, Automaton, Axiom, Bauer, Bool, Broy, Carrier sets, Category theory, Complete type, Computation structures, Computer science, Congruence relation, Data structures, Data types, Definedness, Definedness predicate, Ehrig, Equality predicate, Error algebras, Existential quantifier, Existential quantifiers, Extremal models, Finset, First order logic, Free variables, Funct, Function symbols, Generation principle, Goguen, Ground term, Ground terms, Guttag, Heidelberg, Heterogeneous algebras, Hierarchical, Hierarchical model, Hierarchical terminal model, Hierarchical type, Hierarchical types, Homomorphism, Incorp, Inequality, Initial algebras, Initial model, Initial models, Iselem, Isomorphic, Isomorphism, Lecture notes, Mathematical foundations, Maximal, Maximal definedness predicate, Maximal formula, Monomorphic, Natural numbers, Nonhierarchical types, Nonprimitive, Nonprimitive axiom, Nonprimitive axioms, Nullspace, Other hand, Other words, Overall type, Parameterized specifications, Partial algebras, Partial functions, Partial operations, Predicate, Previous section, Primitive axioms, Primitive bool, Primitive sort, Primitive term, Primitive type, Proc, Program construction, Program development, Programming languages, Provable, Quantifier, Same sort, Satisfiability relation, Satisfiable, Semantics, Seventh colloquium, Sixth colloquium, Software, Software engineering environment, Sort finset, Specification, Specification techniques, Springer, Structural induction, Sufficient completeness, Sufficient conditions, Terminal, Terminal algebra, Terminal model, Terminal models, Type finset, Universal algebra, Wirsing.
Abstract
Summary: Hierarchical abstract data types are algebraic specifications of computation structures where certain sorts, function symbols, and axioms are designated as being primitive. On hierarchical abstract data types additional structure is imposed. An algebraic specification is thus decomposed into several well-separated levels, such that both the understanding and the independent implementation of the levels is supported. This paper provides both model-theoretic and deduction-oriented conditions guaranteeing the soundness of a hierarchical specification. Furthermore necessary and sufficient conditions for the existence of initial and terminal models are investigated, and their close connection to the soundness of a hierarchy is demonstrated. In order to provide freedom and flexibility for specifications a wide class of axioms — namely universal-existential formulas — are admitted.
Url:
DOI: 10.1007/BF00264293
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:FFAA2CB3548CD009F8E813B42431F56749F1CF04Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">On hierarchies of abstract data types</title><author><name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name></author><author><name sortKey="Pepper, Peter" sort="Pepper, Peter" uniqKey="Pepper P" first="Peter" last="Pepper">Peter Pepper</name></author><author><name sortKey="Partsch, Helmut" sort="Partsch, Helmut" uniqKey="Partsch H" first="Helmut" last="Partsch">Helmut Partsch</name></author><author><name sortKey="Dosch, Walter" sort="Dosch, Walter" uniqKey="Dosch W" first="Walter" last="Dosch">Walter Dosch</name></author><author><name sortKey="Broy, Manfred" sort="Broy, Manfred" uniqKey="Broy M" first="Manfred" last="Broy">Manfred Broy</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FFAA2CB3548CD009F8E813B42431F56749F1CF04</idno><date when="1983" year="1983">1983</date><idno type="doi">10.1007/BF00264293</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-RB3DJC2T-G/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003D34</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003D34</idno><idno type="wicri:Area/Istex/Curation">003C89</idno><idno type="wicri:Area/Istex/Checkpoint">003823</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003823</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">On hierarchies of abstract data types</title><author><name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fakultät für Informatik, Universität Passau, Postfach 2540, D-8390, Passau</wicri:regionArea><wicri:noRegion>Passau</wicri:noRegion><wicri:noRegion>Passau</wicri:noRegion></affiliation></author><author><name sortKey="Pepper, Peter" sort="Pepper, Peter" uniqKey="Pepper P" first="Peter" last="Pepper">Peter Pepper</name><affiliation wicri:level="4"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Institut für Informatik, Technische Universität München, Postfach 202420, D-8000, München 2</wicri:regionArea><placeName><region type="land" nuts="1">Bavière</region><region type="district" nuts="2">District de Haute-Bavière</region><settlement type="city">Munich</settlement></placeName><orgName type="university">Université technique de Munich</orgName></affiliation></author><author><name sortKey="Partsch, Helmut" sort="Partsch, Helmut" uniqKey="Partsch H" first="Helmut" last="Partsch">Helmut Partsch</name><affiliation wicri:level="4"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Institut für Informatik, Technische Universität München, Postfach 202420, D-8000, München 2</wicri:regionArea><placeName><region type="land" nuts="1">Bavière</region><region type="district" nuts="2">District de Haute-Bavière</region><settlement type="city">Munich</settlement></placeName><orgName type="university">Université technique de Munich</orgName></affiliation></author><author><name sortKey="Dosch, Walter" sort="Dosch, Walter" uniqKey="Dosch W" first="Walter" last="Dosch">Walter Dosch</name><affiliation wicri:level="4"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Institut für Informatik, Technische Universität München, Postfach 202420, D-8000, München 2</wicri:regionArea><placeName><region type="land" nuts="1">Bavière</region><region type="district" nuts="2">District de Haute-Bavière</region><settlement type="city">Munich</settlement></placeName><orgName type="university">Université technique de Munich</orgName></affiliation></author><author><name sortKey="Broy, Manfred" sort="Broy, Manfred" uniqKey="Broy M" first="Manfred" last="Broy">Manfred Broy</name><affiliation wicri:level="1"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fakultät für Informatik, Universität Passau, Postfach 2540, D-8390, Passau</wicri:regionArea><wicri:noRegion>Passau</wicri:noRegion><wicri:noRegion>Passau</wicri:noRegion></affiliation></author></analytic><monogr></monogr><series><title level="j">Acta Informatica</title><title level="j" type="abbrev">Acta Informatica</title><idno type="ISSN">0001-5903</idno><idno type="eISSN">1432-0525</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="1983-10-01">1983-10-01</date><biblScope unit="volume">20</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="1">1</biblScope><biblScope unit="page" to="33">33</biblScope></imprint><idno type="ISSN">0001-5903</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0001-5903</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract data types</term><term>Abstract type</term><term>Abstract types</term><term>Additional properties</term><term>Algebra</term><term>Algebraic</term><term>Algebraic specification</term><term>Algebraic specifications</term><term>Automaton</term><term>Axiom</term><term>Bauer</term><term>Bool</term><term>Broy</term><term>Carrier sets</term><term>Category theory</term><term>Complete type</term><term>Computation structures</term><term>Computer science</term><term>Congruence relation</term><term>Data structures</term><term>Data types</term><term>Definedness</term><term>Definedness predicate</term><term>Ehrig</term><term>Equality predicate</term><term>Error algebras</term><term>Existential quantifier</term><term>Existential quantifiers</term><term>Extremal models</term><term>Finset</term><term>First order logic</term><term>Free variables</term><term>Funct</term><term>Function symbols</term><term>Generation principle</term><term>Goguen</term><term>Ground term</term><term>Ground terms</term><term>Guttag</term><term>Heidelberg</term><term>Heterogeneous algebras</term><term>Hierarchical</term><term>Hierarchical model</term><term>Hierarchical terminal model</term><term>Hierarchical type</term><term>Hierarchical types</term><term>Homomorphism</term><term>Incorp</term><term>Inequality</term><term>Initial algebras</term><term>Initial model</term><term>Initial models</term><term>Iselem</term><term>Isomorphic</term><term>Isomorphism</term><term>Lecture notes</term><term>Mathematical foundations</term><term>Maximal</term><term>Maximal definedness predicate</term><term>Maximal formula</term><term>Monomorphic</term><term>Natural numbers</term><term>Nonhierarchical types</term><term>Nonprimitive</term><term>Nonprimitive axiom</term><term>Nonprimitive axioms</term><term>Nullspace</term><term>Other hand</term><term>Other words</term><term>Overall type</term><term>Parameterized specifications</term><term>Partial algebras</term><term>Partial functions</term><term>Partial operations</term><term>Predicate</term><term>Previous section</term><term>Primitive axioms</term><term>Primitive bool</term><term>Primitive sort</term><term>Primitive term</term><term>Primitive type</term><term>Proc</term><term>Program construction</term><term>Program development</term><term>Programming languages</term><term>Provable</term><term>Quantifier</term><term>Same sort</term><term>Satisfiability relation</term><term>Satisfiable</term><term>Semantics</term><term>Seventh colloquium</term><term>Sixth colloquium</term><term>Software</term><term>Software engineering environment</term><term>Sort finset</term><term>Specification</term><term>Specification techniques</term><term>Springer</term><term>Structural induction</term><term>Sufficient completeness</term><term>Sufficient conditions</term><term>Terminal</term><term>Terminal algebra</term><term>Terminal model</term><term>Terminal models</term><term>Type finset</term><term>Universal algebra</term><term>Wirsing</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Summary: Hierarchical abstract data types are algebraic specifications of computation structures where certain sorts, function symbols, and axioms are designated as being primitive. On hierarchical abstract data types additional structure is imposed. An algebraic specification is thus decomposed into several well-separated levels, such that both the understanding and the independent implementation of the levels is supported. This paper provides both model-theoretic and deduction-oriented conditions guaranteeing the soundness of a hierarchical specification. Furthermore necessary and sufficient conditions for the existence of initial and terminal models are investigated, and their close connection to the soundness of a hierarchy is demonstrated. In order to provide freedom and flexibility for specifications a wide class of axioms — namely universal-existential formulas — are admitted.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Bavière</li><li>District de Haute-Bavière</li></region><settlement><li>Munich</li></settlement><orgName><li>Université technique de Munich</li></orgName></list><tree><country name="Allemagne"><noRegion><name sortKey="Wirsing, Martin" sort="Wirsing, Martin" uniqKey="Wirsing M" first="Martin" last="Wirsing">Martin Wirsing</name></noRegion><name sortKey="Broy, Manfred" sort="Broy, Manfred" uniqKey="Broy M" first="Manfred" last="Broy">Manfred Broy</name><name sortKey="Dosch, Walter" sort="Dosch, Walter" uniqKey="Dosch W" first="Walter" last="Dosch">Walter Dosch</name><name sortKey="Partsch, Helmut" sort="Partsch, Helmut" uniqKey="Partsch H" first="Helmut" last="Partsch">Helmut Partsch</name><name sortKey="Pepper, Peter" sort="Pepper, Peter" uniqKey="Pepper P" first="Peter" last="Pepper">Peter Pepper</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003823 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 003823 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Checkpoint
|type= RBID
|clé= ISTEX:FFAA2CB3548CD009F8E813B42431F56749F1CF04
|texte= On hierarchies of abstract data types
}}
| This area was generated with Dilib version V0.6.33. |  |