{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:47:34Z","timestamp":1762458454480},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1991,10,1]],"date-time":"1991-10-01T00:00:00Z","timestamp":686275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1991,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>An induction principle, called context induction, is presented which is appropriate for the verification of behavioural properties of abstract data types. The usefulness of the proof principle is documented by several applications: the verification of behavioural theorems over a behavioural specification, the verification of behavioural implementations and the verification of \u201cforget-restrict-identify\u201d implementations.<\/jats:p>\n          <jats:p>In particular, it is shown that behavioural implementations and \u201cforget-restrict-identify\u201d implementations (under certain assumptions) can be characterised by the same condition on contexts, i.e. (under the given assumptions) both concepts are equivalent. This leads to the suggestion to use context induction as a uniform proof method for correctness proofs of algebraic implementations.<\/jats:p>","DOI":"10.1007\/bf01642507","type":"journal-article","created":{"date-parts":[[2005,5,11]],"date-time":"2005-05-11T09:12:24Z","timestamp":1115802744000},"page":"326-345","source":"Crossref","is-referenced-by-count":50,"title":["Context induction: A proof principle for behavioural abstractions and algebraic implementations"],"prefix":"10.1145","volume":"3","author":[{"given":"Rolf","family":"Hennicker","sequence":"first","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau, Postfach 2540, D-8390, Passau, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Boyer R. S. and Moore J. S.: A Computational Logic Handbook . Academic Press 1988."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/14861.14864"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90086-0"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/12.1.41"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Ehrig H. and Mahr B.: Fundamentals of Algebraic Specification 1 . EATCS Monographs on Theoretical Computer Science Vo. 6 Springer-Verlag 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80001-7"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Garland S. J. and Guttag J. V.: Inductive Methods for Reasoning about Abstract Data Types. Proc. POPL'88 pp. 219\u2013228 1988.","DOI":"10.1145\/73560.73579"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Giarratana V. Gimona F. and Montanari U.: Observability Concepts in Abstract Data Type Specification. In: Proc. MFCS '76 5th Int. Symp. on Mathematical Foundations of Computer Science A. Mazurkiewicz (ed.) Lecture Notes in Computer Science 45 Springer-Verlag pp. 576\u2013587 1976.","DOI":"10.1007\/3-540-07854-1_231"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/947864.947865"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Hennicker R.: Context Induction: a Proof Principle for Behavioural Abstractions. In: Proc. DISCO '90 Int. Symp. on Design and Implementation of Symbolic Computation Systems A. Miola (ed.) Capri April 1990 Lecture Notes in Computer Science 429 Springer-Verlag pp. 101\u2013110 1990.","DOI":"10.1007\/3-540-52531-9_129"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178505"},{"key":"e_1_2_1_2_12_2","unstructured":"Hennicker R.: A Semi-Algorithm for Algebraic Implementation Proofs. Technische Berichte der Fakult\u00e4t f\u00fcr Mathematik und Informatik Universit\u00e4t Pasau MIP-9108 1991."},{"issue":"1","key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/357195.357202","article-title":"Final Data Types and Their Specification","volume":"5","author":"Kamin S.","year":"1983","journal-title":"ACM TOPLASS"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Nivela M a P. and Orejas F.: Initial Behaviour Semantics for Algebraic Specifications. In: Proc. 5th Workshop on Algebraic Specifications of Abstract Data Types D. T. Sannella and A. Tarlecki (eds) Lecture Notes in Computer Science 332 Springer-Verlag pp. 184\u2013207 1988.","DOI":"10.1007\/3-540-50325-0_10"},{"key":"e_1_2_1_2_15_2","first-page":"88","article-title":"Completeness of Many-Sorted Equational Logic Revisited","volume":"24","author":"Padawitz P.","year":"1984","journal-title":"Bulletin EATCS"},{"key":"e_1_2_1_2_16_2","first-page":"107","article-title":"Abstrakte Datentypen: Die algebraische Spezifikation von Rechenstrukturen","volume":"5","author":"Pepper P.","year":"1982","journal-title":"Informatik-Spektrum"},{"key":"e_1_2_1_2_17_2","unstructured":"Reichel H.: Initial Restrictions of Behaviour. IFIP Working Conference The role of Abstract Models in Information Processing 1985."},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Sannella D. T. and Wirsing M.: Implementation of Parameterized Specifications. In: Proc. ICALP '82 9th Coll. on Automata Languages and Programming M. Nielsen and E. M. Schmidt (eds) Lecture Notes in Computer Science 140 Springer-Verlag pp. 473\u2013488 1982.","DOI":"10.1007\/BFb0012793"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90011-4"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01642507.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01642507\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01642507","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:18:57Z","timestamp":1641482337000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01642507"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,10]]},"references-count":19,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1991,10]]}},"alternative-id":["10.1007\/BF01642507"],"URL":"https:\/\/doi.org\/10.1007\/bf01642507","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,10]]}}}