{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:29:00Z","timestamp":1707521340014},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"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":[[2010,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>For a number of programming languages, among them Eiffel, C, Java, and Ruby, Hoare-style logics and dynamic logics have been developed. In these logics, pre- and postconditions are typically formulated using potentially effectful programs. In order to ensure that these pre- and postconditions behave like logical formulae (that is, enjoy some kind of referential transparency), a notion of purity is needed. Here, we introduce a generic framework for reasoning about purity and effects. Effects are modelled abstractly and axiomatically, using Moggi\u2019s idea of encapsulation of effects as monads. We introduce a dynamic logic (from which, as usual, a Hoare logic can be derived) whose logical formulae are pure programs in a strong sense. We formulate a set of proof rules for this logic, and prove it to be complete with respect to a categorical semantics. Using dynamic logic, we then develop a relaxed notion of purity which allows for observationally neutral effects such writing on newly allocated memory.<\/jats:p>","DOI":"10.1007\/s00165-010-0153-4","type":"journal-article","created":{"date-parts":[[2010,4,20]],"date-time":"2010-04-20T14:45:36Z","timestamp":1271774736000},"page":"363-384","source":"Crossref","is-referenced-by-count":4,"title":["A generic complete dynamic logic for reasoning about purity and effects"],"prefix":"10.1145","volume":"22","author":[{"given":"Till","family":"Mossakowski","sequence":"first","affiliation":[{"name":"Safe and secure cognitive systems, DFKI GmbH, Bremen, Germany"},{"name":"Department of Computer Science, University of Bremen, Bremen, Germany"}]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[{"name":"Safe and secure cognitive systems, DFKI GmbH, Bremen, Germany"},{"name":"Department of Computer Science, University of Bremen, Bremen, Germany"}]},{"given":"Sergey","family":"Goncharov","sequence":"additional","affiliation":[{"name":"Safe and secure cognitive systems, DFKI GmbH, Bremen, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002998"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Beckert B (2001) A dynamic logic for the formal verification of Java card programs. In: Attali I Jensen T (eds) Java on smart cards: programming and security. Revised papers Java card 2000 International workshop Cannes France vol 2041 of LNCS Springer Berlin pp 6\u201324","DOI":"10.1007\/3-540-45165-X_2"},{"key":"e_1_2_1_2_3_2","unstructured":"Bonniot D Keller B (2003) The Nice user\u2019s manual. http:\/\/nice.sourceforge.net 2003"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4474"},{"issue":"2","key":"e_1_2_1_2_5_2","first-page":"36","article-title":"The D programming language","volume":"27","author":"Bright W","year":"2002","journal-title":"Dr. Dobb\u2019s J Softw Tools"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Cok DR Kiniry JR (2005) ESC\/Java2: uniting ESC\/Java and JML: progress and issues in building and using ESC\/Java2 including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe G Burdy L Huisman M Lanet J-L Muntean T (eds) Construction and analysis of safe secure and interoperable smart devices (CASSIS 2004) vol 3362 of Lecture Notes in Computer Science Springer Berlin pp 108\u2013128","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Findler RB Felleisen M (2002) Contracts for higher-order functions. In: ICFP pp 48\u201359","DOI":"10.1145\/583852.581484"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"F\u00fchrmann C (2002) Varieties of effects. In: Foundations of software science and computation structures vol 2303 of LNCS Springer Berlin pp 144\u2013158","DOI":"10.1007\/3-540-45931-6_11"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Goncharov S Schr\u00f6der L Mossakowski T (2006) Completeness of global evaluation logic. In: Mathematical foundations of computer science MFCS 06 vol 4162 of LNCS Springer Berlin pp 447\u2013458","DOI":"10.1007\/11821069_39"},{"key":"e_1_2_1_2_10_2","unstructured":"Hindley JR (1964) The Church\u2013Rosser property and a result in combinatory logic. PhD thesis University of Newcastle-upon-Tyne"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. CACM p 12","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_12_2","unstructured":"Huisman M (2001) Java program verification in higher order logic with PVS and Isabelle. PhD thesis University of Nijmegen"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00366-3"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_2_1_2_15_2","volume-title":"Categories for the working mathematician","author":"Mac Lane S","year":"1997"},{"key":"e_1_2_1_2_16_2","unstructured":"Meyer B (1992) Eiffel: the language. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.5555\/2383063.2383070"},{"key":"e_1_2_1_2_19_2","first-page":"199","volume-title":"Fundamental approaches to software engineering (FASE 2008), vol 4961 of Lecture Notes in Computer Science.","author":"Mossakowski T","year":"2008"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.004"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"e_1_2_1_2_22_2","volume-title":"The Sather language. Technical report","author":"Omohundro SM","year":"1991"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Pitts A (1991) Evaluation logic. In: Higher Order Workshop Workshops in computing. Springer Berlin pp 162\u2013189","DOI":"10.1007\/978-1-4471-3182-3_11"},{"key":"e_1_2_1_2_24_2","unstructured":"Peyton-Jones S (ed) (2003) Haskell 98 language and libraries\u2014the revised report. Cambridge 2003. also: J Funct Program 13"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Pratt V (1976) Semantical considerations on Floyd-Hoare logic. In: Foundations of conputer science FOCS 76. IEEE pp 109\u2013121","DOI":"10.1109\/SFCS.1976.27"},{"key":"e_1_2_1_2_26_2","unstructured":"Sonntag B Colnet D (2002) Lisaac: the power of simplicity at work for operating system. In: Technology of object-oriented languages and systems TOOLS Pacific 02 vol 10 of CRPIT. ACS pp 45\u201352"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Schr\u00f6der L Mossakowski T (2003) Monad-independent Hoare logic in HasCasl . In Fundamental aspects of software engineering FASE 03 vol 2621 of LNCS pp 261\u2013277","DOI":"10.1007\/3-540-36578-8_19"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.571"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Schr\u00f6der L Mossakowski T (2004) Generic exception handling and the Java monad. In: Algebraic methodology and software technology AMAST 04 vol 3116 of LNCS Springer Berlin pp 443\u2013459","DOI":"10.1007\/978-3-540-27815-3_34"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Stenzel K (2004) A formally verified calculus for full java card. In: Rattray C Maharaj S Shankland C (eds) AMAST vol 3116 of Lecture Notes in Computer Science Springer Berlin pp 491\u2013505","DOI":"10.1007\/978-3-540-27815-3_37"},{"key":"e_1_2_1_2_31_2","unstructured":"Thielecke H (1997) Categorical structure of continuation passing style. PhD thesis University of Edinburgh"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"van den Berg J Jacobs B (2001) The LOOP compiler for java and JML. In: Margaria T Yi W (eds) TACAS vol 2031 of Lecture Notes in Computer Science Springer Berlin pp 299\u2013312","DOI":"10.1007\/3-540-45319-9_21"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.598"},{"key":"e_1_2_1_2_34_2","unstructured":"Walter D (2005) Monadic dynamic logic: application and implementation. Master\u2019s thesis University of Bremen 2005. Available at http:\/\/www.cs.chalmers.se\/~denniswa"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Walter D Schr\u00f6der L Mossakowski T (2005) Parametrized exceptions. In: Algebra and coalgebra in computer science CALCO 05 vol 3629 of LNCS. Springer Berlin pp 424\u2013438","DOI":"10.1007\/11548133_27"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-010-0153-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-010-0153-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-010-0153-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:52:38Z","timestamp":1641484358000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-010-0153-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1007\/s00165-010-0153-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-010-0153-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5]]}}}