{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T15:55:01Z","timestamp":1761580501930},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540440390"},{"type":"electronic","value":"9783540456858"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_8","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T20:47:53Z","timestamp":1179607673000},"page":"99-114","source":"Crossref","is-referenced-by-count":20,"title":["A Proposal for a Formal OCL Semantics in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"8_CR1","unstructured":"Manfred Broy, Christian Facchi, Radu Grosu, Rudi Hettler, Heinrich Hussmann, Dieter Nazareth, Oscar Slotosch, Franz Regensburger, and Ketil St\u00f8len. The requirement and design specification language Spectrum, an informal introduction (V 1.0). Technical Report TUM-I9312, TU M\u00fcnchen, 1993."},{"key":"8_CR2","unstructured":"Achim D. Brucker and Burkhart Wolff. A note on design decisions of a formalization of the OCL. Technical Report 168, Albert-Ludwigs-Universit\u00e4t Freiburg, 2002."},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0024651","volume-title":"FME\u201993: Industrial-Strength Formal Methods","author":"J. Dick","year":"1993","unstructured":"Jeremy Dick and Alain Faivre. Automating the generation and sequencing of test cases from model-based specications. In J.C.P. Woodcock and P.G. Larsen, editors, FME\u201993: Industrial-Strength Formal Methods, volume 670 of LNCS, pages 268\u2013284. Springer, 1993."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Reiner H\u00e4hnle. Automated Deduction in Multiple-valued Logics. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198539896.001.0001"},{"key":"8_CR5","unstructured":"Cliff B. Jones. Systematic Software Development Using VDM. Prentice Hall, 1990."},{"issue":"1","key":"8_CR6","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/502269.502306","volume":"45","author":"C. Kobryn","year":"2002","unstructured":"Cris Kobryn. Will UML 2.0 be agile or awkward? CACM, 45(1):107\u2013110, 2002.","journal-title":"CACM"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Luis Mandel and Mar\u00eca Victoria Cengarle. On the expressive power of OCL. FM\u201999, 1999.","DOI":"10.1007\/3-540-48119-2_47"},{"key":"8_CR8","series-title":"Lect Notes Comput Sci","volume-title":"UML 2001: The Unified Modeling Language. Modeling Languages, Concepts, and Tools","author":"L. Mandel","year":"2001","unstructured":"Luis Mandel and Mar\u00eca Victoria Cengarle. A formal semantics for OCL 1.4. In C. Kobryn M. Gogolla, editor, UML 2001: The Unified Modeling Language. Modeling Languages, Concepts, and Tools, volume 2185 of LNCS, Toronto, 2001. Springer."},{"key":"8_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BFb0055146","volume-title":"Theorem Proving in Higher Order Logics","author":"W. Naraschewski","year":"1998","unstructured":"Wolfgang Naraschewski and Markus Wenzel. Object-oriented verification based on record subtyping in Higher-Order Logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, volume 1479 of LNCS, pages 349\u2013366. Springer, 1998."},{"key":"8_CR10","unstructured":"Tobias Nipkow, David von Oheimb, and Cornelia Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In Friedrich L. Bauer and Ralf Steinbr\u00fcggen, editors, Foundations of Secure Computation, volume 175 of NATO Science Series F: Computer and Systems Sciences, pages 117\u2013144. IOS Press, 2000."},{"key":"8_CR11","volume-title":"Technical Report DITC 161\/90","author":"N. D. North","year":"1990","unstructured":"N. D. North. Automatic test generation for the triangle problem. Technical Report DITC 161\/90, National Physical Laboratory, Teddington, 1990."},{"key":"8_CR12","unstructured":"OMG. Object Constraint Language Specification. [13], chapter 6."},{"key":"8_CR13","unstructured":"OMG. Unified Modeling Language Specification (Version 1.4). 2001."},{"key":"8_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/978-3-540-49524-6_35","volume-title":"Proc. 17th Int. Conf. Conceptual Modeling (ER\u201998)","author":"M. Richters","year":"1998","unstructured":"Mark Richters and Martin Gogolla. On Formalizing the UML Object Constraint Language OCL. In Tok-Wang Ling, Sudha Ram, and Mong Li Lee, reditors, Proc. 17th Int. Conf. Conceptual Modeling (ER\u201998), volume 1507 of LNCS, pages 449\u2013464. Springer, 1998."},{"key":"8_CR15","unstructured":"Thomas Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. PhD thesis, Technical University Berlin, 1999."},{"key":"8_CR16","unstructured":"J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1992."},{"key":"8_CR17","volume-title":"The Object Contraint Language: Precise Modelling with UML","author":"J. Warmer","year":"1999","unstructured":"Jos Warmer and Anneke Kleppe. The Object Contraint Language: Precise Modelling with UML. Addison-Wesley Longman, Reading, USA, 1999."},{"key":"8_CR18","unstructured":"Jos Warmer, Anneke Kleppe, Tony Clark, Anders Ivner, Jonas H\u00f6gstr\u00f6m, Martin Gogolla, Mark Richters, Heinrich Hussmann, Steffen Zschaler, Simon Johnston, David S. Frankel, and Conrad Bock. Response to the UML 2.0 OCL RfP. Technical report, 2001."},{"key":"8_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, 1993."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,14]],"date-time":"2024-02-14T11:53:23Z","timestamp":1707911603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}