{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T16:46:58Z","timestamp":1648658818780},"reference-count":57,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4780,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1996,2]]},"abstract":"<jats:p>In this paper we try to shed some light on the similarities and differences in the different approaches denning the notions of implementation and implementation correctness. For obvious reasons, we do not discuss all existing approaches individually. Instead, a formal framework is introduced in order to discuss the most important ones. Additionally, we discuss some issues, which in our opinion are often misunderstood, concerning transitivity of implementation correctness and its role in the software development process. In particular, on the one hand, we show that for reasonable notions of implementation, it is almost impossible to prove transitivity of implementation correctness at the specification level. On the other hand, we show that this is not really important if the programming language satisfies the properties of horizontal and vertical composition.<\/jats:p>","DOI":"10.1017\/s0960129500000864","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:07Z","timestamp":1236157207000},"page":"33-67","source":"Crossref","is-referenced-by-count":5,"title":["Algebraic implementation of abstract data types: a survey of concepts and new compositionality results"],"prefix":"10.1017","volume":"6","author":[{"given":"Fernando","family":"Orejas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marisa","family":"Navarro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000864_ref041","first-page":"357","article-title":"A proof system for checking composability of implementations of abstract data types. Proc. of the Intl. Symp. on Semantics of Data Types, Sophia-Antipolis","volume":"173","author":"Orejas","year":"1984","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129500000864_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12896-4_366"},{"key":"S0960129500000864_ref045","doi-asserted-by":"crossref","unstructured":"Orejas F. , Navarro M. and S\u00e1nchez A. (1994): On the correctness of modular systems. Theoretical Computer Science (to appear).","DOI":"10.1016\/0304-3975(94)00207-Y"},{"key":"S0960129500000864_ref026","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"S0960129500000864_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035766"},{"key":"S0960129500000864_ref024","unstructured":"Goguen J. A. and Burstall R. M. (1980) CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, Computer Science Laboratory, SRI International."},{"key":"S0960129500000864_ref014","first-page":"79","article-title":"Concepts and compatibility requirements for implementations and transformation of specifications, Algebraic Specification Column Part 6","volume":"38","author":"Ehrig","year":"1989","journal-title":"EATCS Bulletin"},{"key":"S0960129500000864_ref013","first-page":"83","article-title":"Proving implementation correct \u2013 two alternative approaches","volume":"80","author":"Ehrich","year":"1980","journal-title":"Information Processing"},{"key":"S0960129500000864_ref042","first-page":"633","volume-title":"Algebra, Logics and Combinatorics in Computer Science","author":"Oreja","year":"1985"},{"key":"S0960129500000864_ref023","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357212"},{"key":"S0960129500000864_ref004","first-page":"139","volume-title":"Processings 2nd. AM AST","author":"Bernot","year":"1991"},{"key":"S0960129500000864_ref012","doi-asserted-by":"publisher","DOI":"10.1145\/322290.322303"},{"key":"S0960129500000864_ref051","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17660-8_50"},{"key":"S0960129500000864_ref009","first-page":"75","volume-title":"A Classical Mind: Essays in Honour of C. A. R. Hoare","author":"Burstall","year":"1994"},{"key":"S0960129500000864_ref027","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012775"},{"key":"S0960129500000864_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80001-7"},{"key":"S0960129500000864_ref018","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08860-1_16"},{"key":"S0960129500000864_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(86)90004-3"},{"key":"S0960129500000864_ref011","first-page":"83","volume-title":"Logical Environments","author":"Diaconescu","year":"1993"},{"key":"S0960129500000864_ref030","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028973"},{"key":"S0960129500000864_ref039","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10699-5_116"},{"key":"S0960129500000864_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90016-3"},{"key":"S0960129500000864_ref037","unstructured":"Nivela P. (1987) Sem\u00e1ntica de comportamiento para especificaciones algebraicas, Ph.D. Thesis, Universitat Polit\u00e8cnica de Catalunya, Barcelona."},{"key":"S0960129500000864_ref015","first-page":"102","article-title":"New compatibility results for implementations within the initial algebraic approach, Algebraic Specification Column Part 11","volume":"43","author":"Ehrig","year":"1981","journal-title":"EATCS Bulletin"},{"key":"S0960129500000864_ref038","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50325-0_10"},{"key":"S0960129500000864_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90121-9"},{"key":"S0960129500000864_ref049","unstructured":"S\u00e1nchez A. (1992) Implementati\u00f3n de Especificaciones Algebraicas, Ph.D. Thesis, Depto. de Leng. Y Sist. Inf., Basque Country University, Spain."},{"key":"S0960129500000864_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7"},{"key":"S0960129500000864_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56379-2_37"},{"key":"S0960129500000864_ref006","volume-title":"Formal Specification and Software Development","author":"Bj\u00f8rner","year":"1982"},{"key":"S0960129500000864_ref031","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178505"},{"key":"S0960129500000864_ref032","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"S0960129500000864_ref033","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_16"},{"key":"S0960129500000864_ref028","first-page":"80","volume-title":"Current Trends in Programming Methodology, Vol. 4. Data Structuring","author":"Goguen","year":"1976"},{"key":"S0960129500000864_ref043","first-page":"143","volume-title":"Proc. IFIP Congress 1986","author":"Orejas","year":"1986"},{"key":"S0960129500000864_ref029","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359666"},{"key":"S0960129500000864_ref034","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90015-9"},{"key":"S0960129500000864_ref035","first-page":"275","volume-title":"Proc. Logic Colloquium '87","author":"Meseguer","year":"1989"},{"key":"S0960129500000864_ref036","first-page":"459","volume-title":"Algebraic Methods in Semantics","author":"Meseguer","year":"1985"},{"key":"S0960129500000864_ref040","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12689-9_116"},{"key":"S0960129500000864_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16078-7_80"},{"key":"S0960129500000864_ref046","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51722-7_7"},{"key":"S0960129500000864_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51486-4_70"},{"key":"S0960129500000864_ref047","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030330"},{"key":"S0960129500000864_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56379-2_40"},{"key":"S0960129500000864_ref048","unstructured":"Reichel H. (1981) Behavioural equivalence \u2013 a unifying concept for initial and final specification methods. Proc. 3rd Hungarian Comp. Sci. Conference 27\u201339."},{"key":"S0960129500000864_ref050","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90023-7"},{"key":"S0960129500000864_ref054","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012793"},{"key":"S0960129500000864_ref055","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12689-9_122"},{"key":"S0960129500000864_ref020","volume-title":"Fundamentals of Algebraic Specifications 2","author":"Ehrig","year":"1989"},{"key":"S0960129500000864_ref044","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56379-2_36"},{"key":"S0960129500000864_ref056","unstructured":"Schoett O. (1987) Data Abstraction and the Correctness of Modular Programming, Ph.D. thesis (Report CST-42\u201387, Dept. of Computer Science, Univ. of Edinburgh)."},{"key":"S0960129500000864_ref057","first-page":"675","volume-title":"Handbook of Theoretical Computer Science, Vol. B; Formal Models and Semantics","author":"Wirsing","year":"1991"},{"key":"S0960129500000864_ref052","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90008-9"},{"key":"S0960129500000864_ref010","first-page":"78","article-title":"GSBL: an algebraic specification language based on inheritance. Proc. 1988 European Conf. on Object Oriented Programming, Oslo","volume":"322","author":"Cl\u00e9rici","year":"1988","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129500000864_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263582"},{"key":"S0960129500000864_ref053","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-50940-2_48"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000864","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T19:14:18Z","timestamp":1557774858000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000864\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,2]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,2]]}},"alternative-id":["S0960129500000864"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000864","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,2]]}}}