{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:06:45Z","timestamp":1725505605824},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787426"},{"type":"electronic","value":"9783540787433"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78743-3_15","type":"book-chapter","created":{"date-parts":[[2008,4,1]],"date-time":"2008-04-01T19:53:27Z","timestamp":1207079607000},"page":"199-214","source":"Crossref","is-referenced-by-count":3,"title":["A Generic Complete Dynamic Logic for Reasoning About Purity and Effects"],"prefix":"10.1007","author":[{"given":"Till","family":"Mossakowski","sequence":"first","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]},{"given":"Sergey","family":"Goncharov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards: Programming and Security","author":"B. Beckert","year":"2001","unstructured":"Beckert, B.: A dynamic logic for the formal verification of Java Card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol.\u00a02041, pp. 6\u201324. Springer, Heidelberg (2001)"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/4472.4474","volume":"7","author":"H.-J. Boehm","year":"1985","unstructured":"Boehm, H.-J.: Side effects and aliasing can have simple axiomatic descriptions. ACM Trans. Program. Lang. Syst\u00a07, 637\u2013655 (1985)","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"15_CR3","unstructured":"Bonniot, D., Keller, B.: The Nice user\u2019s manual (2003), http:\/\/nice.sourceforge.net"},{"issue":"2","key":"15_CR4","first-page":"36","volume":"27","author":"W. Bright","year":"2002","unstructured":"Bright, W.: The D programming language. Dr. Dobb\u2019s Journal of Software Tools\u00a027(2), 36\u201340 (2002)","journal-title":"Dr. Dobb\u2019s Journal of Software Tools"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: ICFP, pp. 48\u201359 (2002)","DOI":"10.1145\/581478.581484"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/11821069_39","volume-title":"Mathematical Foundations of Computer Science 2006","author":"S. Goncharov","year":"2006","unstructured":"Goncharov, S., Schr\u00f6der, L., Mossakowski, T.: Completeness of global evaluation logic. In: Kr\u00e1lovi\u010d, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol.\u00a04162, pp. 447\u2013458. Springer, Heidelberg (2006)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Hoare,: An axiomatic basis for computer programming. CACM\u00a012 (1969)","DOI":"10.1145\/363235.363259"},{"key":"15_CR9","unstructured":"Huisman, M.: Java program verification in higher order logic with PVS and Isabelle. PhD thesis, University of Nijmegen (2001)"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0304-3975(02)00366-3","volume":"291","author":"B. Jacobs","year":"2003","unstructured":"Jacobs, B., Poll, E.: Coalgebras and Monads in the Semantics of Java. Theoret. Comput. Sci.\u00a0291, 329\u2013349 (2003)","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR11","volume-title":"Categories for the Working Mathematician","author":"S. Mac Lane","year":"1997","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1997)"},{"key":"15_CR12","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"15_CR13","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inform. and Comput.\u00a093, 55\u201392 (1991)","journal-title":"Inform. and Comput."},{"key":"15_CR14","doi-asserted-by":"crossref","first-page":"117","DOI":"10.3233\/FI-1995-22126","volume":"22","author":"E. Moggi","year":"1995","unstructured":"Moggi, E.: A semantics for evaluation logic. Fund. Inform.\u00a022, 117\u2013152 (1995)","journal-title":"Fund. Inform."},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/j.tcs.2007.02.004","volume":"376","author":"D.A. Naumann","year":"2007","unstructured":"Naumann, D.A.: Observational purity and encapsulation. Theoret. Comput. Sci\u00a0376, 205\u2013224 (2007)","journal-title":"Theoret. Comput. Sci"},{"key":"15_CR16","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"15_CR17","unstructured":"Omohundro, S.M.: The Sather language. Technical report, International Computer Science Institute, Berkeley (1991)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Peyton-Jones, S. (ed.): Haskell 98 Language and Libraries \u2014 The Revised Report, Cambridge (2003), also: J. Funct. Programming 13 (2003)","DOI":"10.1017\/S0956796803001515"},{"key":"15_CR19","first-page":"162","volume-title":"Higher Order Workshop, Workshops in Computing","author":"A. Pitts","year":"1991","unstructured":"Pitts, A.: Evaluation logic. In: Higher Order Workshop, Workshops in Computing, pp. 162\u2013189. Springer, Heidelberg (1991)"},{"key":"15_CR20","first-page":"109","volume-title":"Foundations of Conputer Science, FOCS 1976","author":"V. Pratt","year":"1976","unstructured":"Pratt, V.: Semantical considerations on Floyd-Hoare logic. In: Foundations of Conputer Science, FOCS 1976, pp. 109\u2013121. IEEE, Los Alamitos (1976)"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-36578-8_19","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Schr\u00f6der","year":"2003","unstructured":"Schr\u00f6der, L., Mossakowski, T.: Monad-independent Hoare logic in HasCASL. In: Pezz\u00e8, M. (ed.) FASE 2003. LNCS, vol.\u00a02621, pp. 261\u2013277. Springer, Heidelberg (2003)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/978-3-540-27815-3_34","volume-title":"Algebraic Methodology and Software Technology","author":"L. Schr\u00f6der","year":"2004","unstructured":"Schr\u00f6der, L., Mossakowski, T.: Generic Exception Handling and the Java Monad. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 443\u2013459. Springer, Heidelberg (2004)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1093\/logcom\/14.4.571","volume":"14","author":"L. Schr\u00f6der","year":"2004","unstructured":"Schr\u00f6der, L., Mossakowski, T.: Monad-independent dynamic logic in HASCASL. J. Logic Comput.\u00a014, 571\u2013619 (2004)","journal-title":"J. Logic Comput."},{"key":"15_CR24","unstructured":"Sonntag, B., Colnet, D.: Lisaac: the power of simplicity at work for operating system. In: Technology of Object-Oriented Languages and Systems, TOOLS Pacific 2002. CRPIT, vol.\u00a010, pp. 45\u201352. ACS (2002)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-27815-3_37","volume-title":"Algebraic Methodology and Software Technology","author":"K. Stenzel","year":"2004","unstructured":"Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 491\u2013505. Springer, Heidelberg (2004)"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Berg van den","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 299\u2013312. Springer, Heidelberg (2001)"},{"key":"15_CR27","doi-asserted-by":"publisher","first-page":"1173","DOI":"10.1002\/cpe.598","volume":"13","author":"D. Oheimb von","year":"2001","unstructured":"von Oheimb, D.: Hoare logic for Java in Isabelle\/HOL. Concurrency and Computation: Practice and Experience\u00a013, 1173\u20131214 (2001)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"15_CR28","unstructured":"Walter, D.: Monadic dynamic logic: Application and implementation. Master\u2019s thesis, University of Bremen (2005), http:\/\/www.cs.chalmers.se\/~denniswa"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/11548133_27","volume-title":"Algebra and Coalgebra in Computer Science","author":"D. Walter","year":"2005","unstructured":"Walter, D., Schr\u00f6der, L., Mossakowski, T.: Parametrized exceptions. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol.\u00a03629, pp. 424\u2013438. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78743-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:15:22Z","timestamp":1606166122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78743-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787426","9783540787433"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78743-3_15","relation":{},"subject":[]}}