{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:00Z","timestamp":1725663480472},"publisher-location":"Berlin, Heidelberg","reference-count":58,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540563792"},{"type":"electronic","value":"9783540475453"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56379-2_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:06:30Z","timestamp":1330254390000},"page":"93-125","source":"Crossref","is-referenced-by-count":15,"title":["Implementation and behavioural equivalence: A survey"],"prefix":"10.1007","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":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"4_CR1","unstructured":"E. Astesiano, M. Cerioli: Commuting between institutions via simulation. Res. Report 2, University of Genoa (1990)."},{"key":"4_CR2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0890-5401(89)90016-3","volume":"80","author":"G. Bernot","year":"1989","unstructured":"G. Bernot: Correctness Proofs for Abstract Implementations. Information and Computation 80,121\u2013151 (1989).","journal-title":"Information and Computation"},{"key":"4_CR3","volume-title":"Report LEENS-91-8","author":"G. Bernot","year":"1991","unstructured":"G. Bernot, M. Bidoit: Proving the correctness of Algebraically Specified Software: Modularity and Observability Issues. Report LEENS-91-8, Dept. de Mathematiques et Informatique, Ecole Normale Superieur, Paris (1991)."},{"key":"4_CR4","first-page":"236","volume":"210","author":"G. Bernot","year":"1986","unstructured":"G. Bernot, M. Bidoit, C. Choppy: Abstract implementations and correctness proofs. Proc. 3rd. Symp. on Theoretical Aspects of Computer Science. Springer LNCS 210, 236\u2013251 (1986).","journal-title":"Springer LNCS"},{"key":"4_CR5","unstructured":"D. Bj\u00f8rner, C. Jones: Formal Specification and Software Development, Prentice Hall Int. (1982)."},{"key":"4_CR6","unstructured":"M. Breu: Bounded implementations of algebraic specifications. 8th Workshop on Specification of Abstract Data Types, Dourdan, France (1991)."},{"key":"4_CR7","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0167-6423(86)90004-3","volume":"7","author":"M. Broy","year":"1986","unstructured":"M. Broy, B. M\u00f6ller, P. Pepper, M. Wirsing: Algebraic implementations preserve program correctness. Science of Computer Programming 7, 35\u201353 (1986).","journal-title":"Science of Computer Programming"},{"issue":"2","key":"4_CR8","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF00263582","volume":"25","author":"F.L. Bauer","year":"1988","unstructured":"F.L. Bauer, M. Wirsing: Crypt-Equivalent Algebraic specifications. Acta Informatica 25(2), 11\u2013153(1988).","journal-title":"Acta Informatica"},{"key":"4_CR9","first-page":"78","volume":"322","author":"S. Cl\u00e9rici","year":"1988","unstructured":"S. Cl\u00e9rici, F. Orejas: GSBL: an algebraic specification language based on inheritance. Proc. 1988 European Conf. on Object Oriented Programming, Oslo. Springer LNCS 322, 78\u201392 (1988).","journal-title":"Springer LNCS"},{"key":"4_CR10","first-page":"83","volume":"80","author":"H.-D. Ehrich","year":"1980","unstructured":"H.-D. Ehrich, U. Lipeck: Proving implementation correct-two alternative approaches. Information Processing 80, 83\u201388 (1980).","journal-title":"Information Processing"},{"key":"4_CR11","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1145\/322290.322303","volume":"29","author":"H.-D. Ehrich","year":"1982","unstructured":"H.-D. Ehrich: On the theory of specification, implementation and parameterization of abstract data types. Journal of the Assoc. for Computing Machinery 29, 206\u2013207 (1982).","journal-title":"Journal of the Assoc. for Computing Machinery"},{"key":"4_CR12","unstructured":"H. Ehrig: Concepts and compatibility requirements for implementations and transformation of specifications, Algebraic Specification Column Part 6, EATCS Bulletin 38, April 1989."},{"key":"4_CR13","unstructured":"H. Ehrig, H. Adametz: New compatibility results for implementations within the initial algebraic approach, Algebraic Specification Column Part 11, EATCS Bulletin 43, February 1991."},{"key":"4_CR14","unstructured":"H. Ehrig, M. Baldamus, F. Cornelius, F. Orejas: Theory of algebraic module specifications including behavioural semantics and constraints, Proc. AMAST 91, to appear in Springer LNCS (1991)."},{"issue":"3","key":"4_CR15","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0304-3975(82)90121-9","volume":"27","author":"H. Ehrig","year":"1983","unstructured":"H. Ehrig, H.-J. Kreowski: Compatibility of parameter passing and implementation of parameterized data types. Theoretical Computer Science 27(3), 255\u2013286 (1983).","journal-title":"Theoretical Computer Science"},{"key":"4_CR16","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/S0304-3975(82)80001-7","volume":"20","author":"H. Ehrig","year":"1982","unstructured":"H. Ehrig, H.-J. Kreowski, B. Mahr, P. Padawitz: Algebraic implementation of abstract data types. Theoretical Computer Science 20, 209\u2013263 (1982).","journal-title":"Theoretical Computer Science"},{"key":"4_CR17","first-page":"205","volume":"62","author":"H. Ehrig","year":"1978","unstructured":"H. Ehrig, H.-J. Kreowski, P. Padawitz: Stepwise specification and implementation of abstract data types. Proc. 5th. Intl. Colloq. on Automata, Languages and Programming, Udine. Springer LNCS 62, 205\u2013226 (1978).","journal-title":"Springer LNCS"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"H. Ehrig, B. Mahr: Fundamentals of Algebraic Specifications 1, Springer 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"H. Ehrig, B. Mahr: Fundamentals of Algebraic Specifications 2, Springer 1989.","DOI":"10.1007\/978-3-642-61284-8"},{"key":"4_CR20","first-page":"225","volume":"379","author":"J. Farr\u00e9s-Casals","year":"1989","unstructured":"J. Farr\u00e9s-Casals: Proving Correctness of Constructor Implementations. Proc. MFCS 89, Springer LNCS 379, 225\u2013235 (1989).","journal-title":"Proc. MFCS 89, Springer LNCS"},{"issue":"3","key":"4_CR21","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1145\/2166.357212","volume":"5","author":"H. Ganzinger","year":"1983","unstructured":"H. Ganzinger: Parameterized specifications: parameter passing and implementation with respect to observability. ACM Trans. on Programming Languages and Systems 5 (3), 318\u2013354 (1983).","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"4_CR22","unstructured":"J.A. Goguen, R.M. Burstall: CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, Computer Science Laboratory, SRI International (1980)."},{"key":"4_CR23","first-page":"221","volume":"164","author":"J.A. Goguen","year":"1984","unstructured":"J.A. Goguen, R.M. Burstall: Introducing institutions. Proc. Logics of Programming Workshop, Carnegie-Mellon. Springer LNCS 164, 221\u2013256 (1984).","journal-title":"Springer LNCS"},{"key":"4_CR24","first-page":"576","volume":"45","author":"V. Giarratana","year":"1976","unstructured":"V. Giarratana, F. Gimona, U. Montanari: Observability concepts in abstract data type specification, Proc. MFCS76, Springer LNCS 45 (1976) 576\u2013587.","journal-title":"Springer LNCS"},{"key":"4_CR25","unstructured":"J.V. Guttag, E. Horowitz, D.R. Musser: Abstract data types and software validation. Research Report ISI\/RR-76-48, University of Southern California (1976). Also in: Communications of the ACM, Vol 21, 12, 1048\u20131063 (1978)."},{"key":"4_CR26","first-page":"265","volume":"140","author":"J.A. Goguen","year":"1982","unstructured":"J.A. Goguen, J. Meseguer: Universal realization, persistent interconnection and implementation of abstract modules. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 265\u2013281 (1982).","journal-title":"Springer LNCS"},{"key":"4_CR27","volume-title":"IBM Report RC-6487","author":"J.A. Goguen","year":"1976","unstructured":"J.A. Goguen, J.W. Thatcher, E.G. Wagner: An initial algebra approach to the specification, correctness and implementation of abstract data types. IBM Report RC-6487, IBM T.J. Watson Research Center, Yorktown Heights (1976). Also in: Current Trends in Programming Methodology, Vol. 4: Data Structuring (R.T. Yeh, ed.) Prentice-hall, 80\u2013149 (1978)."},{"key":"4_CR28","unstructured":"R. Hennicker: Beobachtungsorientierte Spezifikationen. Ph.D. thesis, Universit\u00e4t Passau (1988)."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"R. Hennicker: Observational implementations. Proc. 6th Symp. on Theoretical Aspects of Computer Science, Paderborn. Springer LNCS 349 (1989).","DOI":"10.1007\/BFb0028973"},{"key":"4_CR30","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BF01178505","volume":"28","author":"R. Hennicker","year":"1991","unstructured":"R. Hennicker: Observational implementation of algebraic specifications. Acta Informatica 28, 187\u2013230 (1991).","journal-title":"Acta Informatica"},{"key":"4_CR31","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare: Proofs of correctness of data representations, Acta Informatica 1, 271\u2013281 (1972).","journal-title":"Acta Informatica"},{"key":"4_CR32","unstructured":"J.P. Jouannaud, E. Kounalis: Proof by induction in equational theories without constructors. Proc. IEEE Symp. on Logic in Computer Science, Boston, 358\u2013366 (1986)."},{"key":"4_CR33","first-page":"317","volume":"173","author":"S. Kamin","year":"1984","unstructured":"S. Kamin, M. Archer: Partial Implementations of Abstract Data Types: A Dissenting View on Errors. Proc. Int. Symposium on Semantics of Data Types, Sophia-Antipolis. Springer LNCS 173, 317\u2013336 (1984).","journal-title":"Springer LNCS"},{"key":"4_CR34","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0167-6423(88)90015-9","volume":"10","author":"D. Kapur","year":"1988","unstructured":"D. Kapur, M. Srivas: Computability and implementability issues in abstract data types. Science of Computer Programming 10, 33\u201363 (1988).","journal-title":"Science of Computer Programming"},{"key":"4_CR35","volume-title":"Proc. Logic Colloquium '87","author":"J. Meseguer","year":"1989","unstructured":"J. Meseguer: General logics. Proc. Logic Colloquium '87, Granada. North Holland (1989)."},{"key":"4_CR36","unstructured":"J. Meseguer, J.A. Goguen: Initiality, induction and computability. In: Algebraic Methods in Semantics (M. Nivat and J. Reynolds, eds.). Cambridge Univ. Press, 459\u2013540 (1985)."},{"key":"4_CR37","volume-title":"Ph.D. Thesis","author":"P. Nivela","year":"1987","unstructured":"P. Nivela: Sem\u00e1ntica de comportamiento para especificaciones algebraicas. Ph.D. Thesis, Universitat Polit\u00e8cnica de Catalunya, Barcelona (1987)."},{"key":"4_CR38","first-page":"184","volume":"332","author":"P. Nivela","year":"1988","unstructured":"P. Nivela, F. Orejas: Initial behavioural semantics for algebraic specifications. Recent Trends in Data Type Specification, Selected Papers from the 5th Workshop on Specification of Abstract Data Types, Gullane, Scotland. Springer LNCS 332, 184\u2013207 (1988).","journal-title":"Springer LNCS"},{"key":"4_CR39","first-page":"419","volume":"107","author":"F. Orejas","year":"1981","unstructured":"F. Orejas: On the representation of data types. Proc. Intl. Coll. on Formalization of programming concepts. Springer LNCS 107, 419\u2013431 (1981).","journal-title":"Springer LNCS"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"F. Orejas: Characterizing composability of abstract implementations. Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. Springer LNCS 158 (1983).","DOI":"10.1007\/3-540-12689-9_116"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"F. Orejas: A proof system for checking composability of implementations of abstract data types. Proc. of the Intl. Symp. on Semantics of Data Types, Sophia-Antipolis. Springer LNCS 173 (1984).","DOI":"10.1007\/3-540-13346-1_18"},{"key":"4_CR42","unstructured":"F. Orejas: On implementability and computability in abstract data types. In: Algebra, Logics and Combinatorics in Computer Science. North-Holland (1985)."},{"key":"4_CR43","first-page":"143","volume-title":"Proc. IFIP Congress 1986","author":"F. Orejas","year":"1986","unstructured":"F. Orejas: The role of abstraction in program development (response). Proc. IFIP Congress 1986, Dublin. North-Holland, 143\u2013146 (1986)."},{"key":"4_CR44","first-page":"220","volume":"534","author":"F. Orejas","year":"1991","unstructured":"F. Orejas, P. Nivela: Constraints for behavioural specifications. Recent Trends in Data Type Specification, Selected Papers from the 7h Workshop on Specification of Abstract Data Types, Wusterhausen\/Dosse, Germany. Springer LNCS 534, 220\u2013245 (1991).","journal-title":"Springer LNCS"},{"key":"4_CR45","first-page":"220","volume":"393","author":"F. Orejas","year":"1989","unstructured":"F. Orejas, P. Nivela, H. Ehrig: Semantical constructions for categories of behavioural specifications. Proc. Workshop on Categorical Methods in Computer Science with Aspects from Topology. Springer LNCS 393, 220\u2013241 (1989).","journal-title":"Springer LNCS"},{"key":"4_CR46","first-page":"102","volume":"393","author":"F. Orejas","year":"1989","unstructured":"F. Orejas, V. Sacristan, S. Cl\u00e9rici: Development of algebraic specifications with constraints. Proc. Workshop on Categorical Methods in Computer Science with Aspects from Topology. Springer LNCS 393, 102\u2013123 (1989).","journal-title":"Springer LNCS"},{"key":"4_CR47","unstructured":"P. Padawitz: Correctness, completeness and consistency of equational data type specifications, PhD thesis, T.U. Berlin (1983)."},{"key":"4_CR48","first-page":"323","volume":"186","author":"P. Padawitz","year":"1989","unstructured":"P. Padawitz: Parameter preserving data type specifications Proc.1985 Intl. Conf. on Theory and Practice if Software Development. Springer LNCS 186, 323\u2013341 (1989)","journal-title":"Springer LNCS"},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"A. Poign\u00e9: Another look at parameterization using subsorts, Proc. MFCS 84, Springer LNCS 176 (1984).","DOI":"10.1007\/BFb0030330"},{"key":"4_CR50","unstructured":"H. Reichel: Behavioural equivalence \u2014 a unifying concept for initial and final specification methods. Proc. 3rd. Hungarian Comp. Sci. Conference, 27\u201339 (1981)."},{"key":"4_CR51","unstructured":"A. S\u00e1nchez: PhD Thesis (forthcoming)."},{"key":"4_CR52","unstructured":"O. Schoett: Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis; Report CST-42-87, Dept. of Computer Science, Univ. of Edinburgh (1987)."},{"key":"4_CR53","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1016\/0022-0000(87)90023-7","volume":"34","author":"D.T. Sannella","year":"1987","unstructured":"D.T. Sannella, A. Tarlecki: On observational equivalence and algebraic specification. Journal of Computer and System Sciences 34, 150\u2013178 (1987).","journal-title":"Journal of Computer and System Sciences"},{"key":"4_CR54","first-page":"96","volume":"249","author":"D.T. Sannella","year":"1987","unstructured":"D.T. Sannella, A. Tarlecki: Toward formal development of programs from algebraic specifications: implementations revisited. Extend abstract in: Proc. Joint Conf. on Theory and Practice of Software Development, Pisa, Springer LNCS 249, 96\u2013110 (1987); full version in Acta Informatica 25, 233\u2013281 (1988).","journal-title":"Springer LNCS"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"D.T. Sannella, A. Tarlecki: Toward formal development of ML programs: foundations and methodology. LFCS Report Series Department of Computer Science, University of Edinburgh ECS-LFCS-89-71(1989). Actualizar.","DOI":"10.1007\/3-540-50940-2_48"},{"key":"4_CR56","first-page":"473","volume":"140","author":"D.T. Sannella","year":"1982","unstructured":"D.T. Sannella, M. Wirsing: Implementation of parameterized specifications. Proc. 9th Intl. Colloq. on Automata, Languages and Programming, Aarhus. Springer LNCS 140, 473\u2013488 (1982).","journal-title":"Springer LNCS"},{"key":"4_CR57","first-page":"413","volume":"158","author":"D.T. Sannella","year":"1983","unstructured":"D.T. Sannella, M. Wirsing: A kernel language for algebraic specification and implementation. Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. Springer LNCS 158, 413\u2013427 (1983).","journal-title":"Springer LNCS"},{"key":"4_CR58","doi-asserted-by":"crossref","unstructured":"M. Wand, Final algebra semantics and data type extensions, JCSS 19 (1979).","DOI":"10.1016\/0022-0000(79)90011-4"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Data Type Specification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56379-2_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:27Z","timestamp":1605647007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56379-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540563792","9783540475453"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/3-540-56379-2_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}