{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:19:45Z","timestamp":1721891985294},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,3,25]],"date-time":"2009-03-25T00:00:00Z","timestamp":1237939200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2009,7]]},"DOI":"10.1007\/s00236-009-0093-8","type":"journal-article","created":{"date-parts":[[2009,3,24]],"date-time":"2009-03-24T05:53:52Z","timestamp":1237874032000},"page":"255-284","source":"Crossref","is-referenced-by-count":22,"title":["Semantics, calculi, and analysis for object-oriented specifications"],"prefix":"10.1007","volume":"46","author":[{"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,3,25]]},"reference":[{"key":"93_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"93_CR2","volume-title":"Modeling in Event-B: System and Software Design","author":"J.R. Abrial","year":"2009","unstructured":"Abrial J.R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York (2009)"},{"issue":"1","key":"93_CR3","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W. Ahrendt","year":"2005","unstructured":"Ahrendt W., Baar T., Beckert B., Bubel R., Giese M., H\u00e4hnle R., Menzel W., Mostowski W., Roth A., Schlager S., Schmitt P.H.: The KeY tool. Softw. Syst. Model. 4(1), 32\u201354 (2005). doi: 10.1007\/s10270-004-0058-x","journal-title":"Softw. Syst. Model."},{"key":"93_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"Introduction to Mathematical Logic and Type Theory: To Truth through Proof","author":"P.B. Andrews","year":"2002","unstructured":"Andrews P.B.: Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edn. Kluwer, Dordrecht (2002)","edition":"2"},{"key":"93_CR5","first-page":"129","volume-title":"Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, IFIP Transactions, vol. A-10","author":"R. Boulton","year":"1993","unstructured":"Boulton R., Gordon A., Gordon M.J.C., Harrison J., Herbert J., Tassel J.V.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds) Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, IFIP Transactions, vol. A-10, pp. 129\u2013156. North-Holland, Nijmegen (1993)"},{"key":"93_CR6","unstructured":"Brucker, A.D.: An interactive proof environment for object-oriented specifications. Ph.D. thesis, ETH Zurich (2007). ETH Dissertation No. 17097"},{"key":"93_CR7","unstructured":"Brucker, A.D., Doser, J., Wolff, B.: An MDA framework supporting OCL. Electronic Communications of the EASST 5 (2006)"},{"key":"93_CR8","first-page":"306","volume-title":"MoDELS 2006: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science, vol. 4199","author":"A.D. Brucker","year":"2006","unstructured":"Brucker A.D., Doser J., Wolff B.: A model transformation semantics and analysis methodology for SecureUML. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds) MoDELS 2006: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science, vol. 4199, pp. 306\u2013320. Springer, Berlin (2006). doi: 10.1007\/11880240_22"},{"key":"93_CR9","unstructured":"Brucker, A.D., Wolff, B.: The HOL-OCL book. Tech. Rep. 525, ETH Zurich (2006)"},{"key":"93_CR10","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s10817-008-9108-3","volume":"41","author":"A.D. Brucker","year":"2008","unstructured":"Brucker A.D., Wolff B.: An extensible encoding of object-oriented data models in HOL. J. Autom. Reason. 41, 219\u2013249 (2008). doi: 10.1007\/s10817-008-9108-3","journal-title":"J. Autom. Reason."},{"issue":"2","key":"93_CR11","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"93_CR12","volume-title":"Labelled Deductive Systems, Oxford Logic Guides, vol. 1","author":"D.M. Gabbay","year":"1997","unstructured":"Gabbay D.M.: Labelled Deductive Systems, Oxford Logic Guides, vol. 1. Oxford University Press, New York (1997)"},{"key":"93_CR13","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-45669-4_6","volume-title":"Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science, vol. 2263","author":"M. Gogolla","year":"2002","unstructured":"Gogolla M., Richters M.: Expressing UML class diagrams properties with OCL. In: Clark, T., Warmer, J. (eds) Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science, vol. 2263, pp. 85\u2013114. Springer, Heidelberg (2002)"},{"key":"93_CR14","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R.: Efficient deduction in many-valued logics. In: International Symposium on Multiple-Valued Logics (ISMVL), pp. 240\u2013249. IEEE Computer Society, Los Alamitos (1994). doi: 10.1109\/ismvl.1994.302195","DOI":"10.1109\/ISMVL.1994.302195"},{"key":"93_CR15","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/978-94-017-1754-0_9","volume-title":"Handbook of Tableau Methods","author":"R. H\u00e4hnle","year":"1999","unstructured":"H\u00e4hnle R.: Tableaux for many-valued logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds) Handbook of Tableau Methods, pp. 529\u2013580. Kluwer, Dordrecht (1999)"},{"key":"93_CR16","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Upper Saddle River (1990) ISBN 0-13-880733-7","edition":"2"},{"key":"93_CR17","doi-asserted-by":"crossref","unstructured":"Kerber, M., Kohlhase, M.: A tableau calculus for partial functions. In: Collegium Logicum\u2014Annals of the Kurt-G\u00f6del-Society, vol. 2, pp. 21\u201349. Springer, New York (1996)","DOI":"10.1007\/978-3-7091-9461-4_2"},{"key":"93_CR18","volume-title":"MDA Explained. The Model Driven Architecture: Practice and Promise","author":"A. Kleppe","year":"2003","unstructured":"Kleppe A., Warmer J., Bast W.: MDA Explained. The Model Driven Architecture: Practice and Promise. Addison-Wesley, Reading (2003)"},{"issue":"10","key":"93_CR19","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/317665.317673","volume":"42","author":"C. Kobryn","year":"1999","unstructured":"Kobryn C.: UML 2001: a standardization odyssey. Commun. ACM 42(10), 29\u201337 (1999). doi: 10.1145\/317665.317673","journal-title":"Commun. ACM"},{"key":"93_CR20","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/11526841_4","volume-title":"FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582","author":"K.R.M. Leino","year":"2005","unstructured":"Leino K.R.M., M\u00fcller P.: Modular verification of static class invariants. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582, pp. 26\u201342. Springer, Heidelberg (2005). doi: 10.1007\/11526841_4"},{"key":"93_CR21","unstructured":"Leino, K.R.M., Nelson, G., Saxe, J.B.: ESC\/Java user\u2019s manual. Tech. Rep. SRC-2000-002, Compaq Systems Research Center (2000)"},{"key":"93_CR22","first-page":"179","volume-title":"Theorem Proving in Higher Order Logics (TPHOLS). Lecture Notes in Computer Science, vol. 3603","author":"C. March\u00e9","year":"2005","unstructured":"March\u00e9 C., Paulin-Mohring C.: Reasoning about Java programs with aliasing and frame conditions. In: Hurd, J., Melham, T.F. (eds) Theorem Proving in Higher Order Logics (TPHOLS). Lecture Notes in Computer Science, vol. 3603, pp. 179\u2013194. Springer, Heidelberg (2005). doi: 10.1007\/11541868_12"},{"key":"93_CR23","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283","author":"T. Nipkow","year":"2002","unstructured":"Nipkow T., Paulson L.C., Wenzel M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45949-9"},{"key":"93_CR24","unstructured":"Richters, M.: A precise approach to validating UML models and OCL constraints. Ph.D. thesis, Universit\u00e4t Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14 (2002)"},{"key":"93_CR25","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-45669-4_4","volume-title":"Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science, vol. 2263","author":"M. Richters","year":"2002","unstructured":"Richters M., Gogolla M.: OCL: Syntax, semantics, and tools. In: Clark, T., Warmer, J. (eds) Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science, vol. 2263, pp. 42\u201368. Springer, Heidelberg (2002)"},{"issue":"2","key":"93_CR26","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/MC.2006.58","volume":"39","author":"D.C. Schmidt","year":"2006","unstructured":"Schmidt D.C.: Guest editor\u2019s introduction: Model-driven engineering. Computer 39(2), 25\u201331 (2006). doi: 10.1109\/MC.2006.58","journal-title":"Computer"},{"key":"93_CR27","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Upper Saddle River (1992)","edition":"2"},{"key":"93_CR28","unstructured":"UML 2.0 OCL specification (2003). Available as OMG document. http:\/\/www.omg.org\/cgi-bin\/doc?ptc\/03-10-14"},{"key":"93_CR29","unstructured":"Unified modeling language specification (version 1.5) (2003). Available as OMG document. http:\/\/www.omg.org\/cgi-bin\/doc?formal\/03-03-01"},{"key":"93_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3208-5","volume-title":"Labelled Non-Classical Logics","author":"L. Vigan\u00f2","year":"2000","unstructured":"Vigan\u00f2 L.: Labelled Non-Classical Logics. Kluwer, Dordrecht (2000)"},{"key":"93_CR31","unstructured":"von Oheimb, D.: Analyzing Java in Isabelle\/HOL: formalization, type safety and Hoare logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2001)"},{"key":"93_CR32","first-page":"89","volume-title":"FME 2002: Formal Methods\u2014Getting IT Right. Lecture Notes in Computer Science, vol. 2391","author":"D. Oheimb von","year":"2002","unstructured":"von Oheimb D., Nipkow T.: Hoare logic for NanoJava: auxiliary variables, side effects, and virtual methods revisited. In: Eriksson, L.H., Lindsay, P.A. (eds) FME 2002: Formal Methods\u2014Getting IT Right. Lecture Notes in Computer Science, vol. 2391, pp. 89\u2013105. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45614-7_6"},{"key":"93_CR33","first-page":"351","volume-title":"TPHOLS 2007. Lecture Notes in Computer Science, vol. 4732","author":"M. Wenzel","year":"2007","unstructured":"Wenzel M., Wolff B.: Building formal method tools in the Isabelle\/Isar framework. In: Schneider, K., Brandt, J. (eds) TPHOLS 2007. Lecture Notes in Computer Science, vol. 4732, pp. 351\u2013366. Springer, Heidelberg (2007)"},{"key":"93_CR34","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":"Winskel G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)"},{"key":"93_CR35","volume-title":"Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science","author":"J. Woodcock","year":"1996","unstructured":"Woodcock J., Davies J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1996)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-009-0093-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-009-0093-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-009-0093-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T01:30:20Z","timestamp":1589679020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-009-0093-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,25]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,7]]}},"alternative-id":["93"],"URL":"https:\/\/doi.org\/10.1007\/s00236-009-0093-8","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,25]]}}}