{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:51Z","timestamp":1775790831685,"version":"3.50.1"},"reference-count":114,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural relational semantics covering both finite and infinite executions. This understanding of logics as abstractions of a semantics facilitates their comparisons through their respective abstractions of the semantics (rather that the much more difficult comparison through their formal proof systems). More importantly, the formalization provides a calculational method for constructively designing the sound and complete formal proof system by abstraction of the semantics. As an example, we extend Hoare logic to cover all possible behaviors of nondeterministic programs and design a new precondition (in)correctness logic.<\/jats:p>","DOI":"10.1145\/3632849","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"175-208","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0101-9953","authenticated-orcid":false,"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90066-X"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477355.3477359"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454076"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-8_2"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2310.18156"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245294"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_8"},{"issue":"1","key":"e_1_3_2_13_1","first-page":"61","article-title":"Logic and Sortal Incorrectness","volume":"31","author":"Bergmann Merrie","year":"1977","unstructured":"Merrie Bergmann. 1977. Logic and Sortal Incorrectness. The Review of Metaphysics 31, 1 (September 1977), 61\u201379. https:\/\/www.jstor.org\/stable\/20127017","journal-title":"The Review of Metaphysics"},{"key":"e_1_3_2_14_1","first-page":"379","article-title":"Declarative Incorrectness Diagnosis in Constraint Logic Programming","author":"Le Berre Fran\u00e7ois","year":"1996","unstructured":"Fran\u00e7ois Le Berre and Alexandre Tessier. 1996. Declarative Incorrectness Diagnosis in Constraint Logic Programming. In APPIA-GULP-PRODE. 379\u2013390.","journal-title":"APPIA-GULP-PRODE"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1142\/4566"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.29007\/VDFD"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/3612456"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1137\/0210045"},{"key":"e_1_3_2_22_1","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"Cousot Patrick","year":"1981","unstructured":"Patrick Cousot. 1981. Semantic Foundations of Program Analysis. In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (Eds.). Prentice-Hall, Inc., Englewood Cliffs, New Jersey, Chapter 10, 303\u2013342."},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00313-3"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_19"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_1"},{"key":"e_1_3_2_26_1","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation (1 ed.). MIT Press.","edition":"1"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot. 2024. Full version of \u201cCalculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation\u201d Proc. ACM Program. Lang. 8 POPL (2024) 7:1\u201310:33 https:\/\/doi.org\/10.1145\/3632849. Zenodo (Dec. 2024) 66 pages. https:\/\/doi.org\/10.5281\/zenodo.10439108 10.5281\/zenodo.10439108","DOI":"10.5281\/zenodo.10439108"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_31_1","first-page":"75","volume-title":"Tools & Notions for Program Construction: an Advanced Course","author":"Cousot Patrick","year":"1982","unstructured":"Patrick Cousot and Radhia Cousot. 1982. Induction principles for proving invariance properties of programs. In Tools & Notions for Program Construction: an Advanced Course, D. N\u00e9el (Ed.). Cambridge University Press, Cambridge, UK, 75\u2013119."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143184"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_58"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2008.03.025"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2537850"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384633"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_40_1","article-title":"Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties","volume":"2023","author":"Dardinier Thibault","year":"2023","unstructured":"Thibault Dardinier. 2023. Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. Arch. Formal Proofs 2023 (2023). https:\/\/www.isa-afp.org\/entries\/HyperHoareLogic.html","journal-title":"Arch. Formal Proofs"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-1898-5"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_44_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5695-3_39"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0025364"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_16"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2023.105077"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2011.09.021"},{"key":"e_1_3_2_53_1","volume-title":"General Lattice Theory","author":"Gr\u00e4tzer George","year":"1998","unstructured":"George Gr\u00e4tzer. 1998. General Lattice Theory (2nd ed.). Birkh\u00e4user.","edition":"2"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09237-4"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_56_1","volume-title":"Grundz\u00fcge der Theoretischen Logik","author":"Hilbert David","year":"1928","unstructured":"David Hilbert and Wilhelm Ackermann. 1928, 1949, reprinted 1959. Grundz\u00fcge der Theoretischen Logik (6 ed.). Springer. Engl. Trans. \u201cPrinciples of Mathematical Logic,\u201d Lewis M. Hammond, George G. Leckie, F. Steinhardt, AMS Chelsea, 1958, reprinted 2008.","edition":"6"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-41928-1"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322088"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571216"},{"key":"e_1_3_2_62_1","volume-title":"The Art of Computer Programming, Volume I: Fundamental Algorithms,","author":"Knuth Donald E.","year":"1968","unstructured":"Donald E. Knuth. 1968. The Art of Computer Programming, Volume I: Fundamental Algorithms,. Addison-Wesley."},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198538677.003.0019"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00276182"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.19"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(71)80035-1"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288637"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_16"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90033-X"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2013.09.014"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_2_74_1","volume-title":"Introduction to Set Theory","author":"Monk James Donald","year":"1969","unstructured":"James Donald Monk. 1969. Introduction to Set Theory. McGraw\u2013Hill. http:\/\/euclid.colorado.edu\/~monkd\/monk11.pdf"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1984.10017"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/359461.359466"},{"key":"e_1_3_2_77_1","article-title":"An Under-Approximate Relational Logic","volume":"2020","author":"Murray Toby","year":"2020","unstructured":"Toby Murray. 2020. An Under-Approximate Relational Logic. Arch. Formal Proofs 2020 (2020). https:\/\/www.isa-afp.org\/entries\/Relational-Incorrectness-Logic.html","journal-title":"Arch. Formal Proofs"},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01966091"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38828-6_2"},{"key":"e_1_3_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_81_1","first-page":"59","volume-title":"Machine Intelligence Volume 5","author":"Park David Michael Ritchie","year":"1969","unstructured":"David Michael Ritchie Park. 1969. Fixpoint Induction and Proofs of Program Properties. In Machine Intelligence Volume 5, Donald Mitchie and Bernard Meltzer (Eds.). Edinburgh Univ. Press, Chapter 3, 59\u201378."},{"key":"e_1_3_2_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10007-5_47"},{"key":"e_1_3_2_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-018-9818-4"},{"key":"e_1_3_2_84_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_3_2_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10007-5_48"},{"key":"e_1_3_2_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAP.2004.03.009"},{"key":"e_1_3_2_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_3_2_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0022460"},{"key":"e_1_3_2_89_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2022.100825"},{"key":"e_1_3_2_90_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.27"},{"key":"e_1_3_2_91_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_2_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_3_2_93_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2023.25"},{"key":"e_1_3_2_94_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2007.02.042"},{"key":"e_1_3_2_95_1","first-page":"49","volume-title":"Towards a Mathematical Semantics for Computer Languages","author":"Scott Dana S.","year":"1971","unstructured":"Dana S. Scott and Christopher Strachey. 1971. Towards a Mathematical Semantics for Computer Languages. Technical Report PRG-6. Oxford University Computer Laboratory. 49 pages. https:\/\/www.cs.ox.ac.uk\/files\/3228\/PRG06.pdf"},{"key":"e_1_3_2_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582185"},{"key":"e_1_3_2_97_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90048-X"},{"key":"e_1_3_2_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263765"},{"key":"e_1_3_2_99_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10503-015-9375-1"},{"key":"e_1_3_2_100_1","doi-asserted-by":"publisher","DOI":"10.2307\/2102968"},{"key":"e_1_3_2_101_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_102_1","first-page":"67","volume-title":"Report of a Conference on High Speed Automatic Calculating Machines","author":"Turing Alan","year":"1949","unstructured":"Alan Turing. 1949 [1950]. Checking a Large Routine. In Report of a Conference on High Speed Automatic Calculating Machines. University of Cambridge Mathematical Laboratory, Cambridge, England, 67\u201369. https:\/\/turingarchive.kings.cam.ac.uk\/publications-lectures-and-talks-amtb\/amt-b-8"},{"key":"e_1_3_2_103_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"e_1_3_2_104_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"e_1_3_2_105_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"e_1_3_2_106_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"e_1_3_2_107_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"e_1_3_2_108_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_11"},{"key":"e_1_3_2_109_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_19"},{"issue":"4","key":"e_1_3_2_110_1","first-page":"199","article-title":"Zur Einf\u00fchrung der transfiniten Zahlen","volume":"1","author":"von Neumann John","year":"1923","unstructured":"John von Neumann. 1923. Zur Einf\u00fchrung der transfiniten Zahlen. Acta Scientiarum Mathematicarum (Szeged) 1, 4-4 (1923), 199\u2013208. http:\/\/pub.acta.hu\/acta\/showCustomerArticle.action?id=4981&dataObjectType=article","journal-title":"Acta Scientiarum Mathematicarum (Szeged)"},{"key":"e_1_3_2_111_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_2_112_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527316"},{"key":"e_1_3_2_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498690"},{"key":"e_1_3_2_114_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527331"},{"key":"e_1_3_2_115_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632849","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632849","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:29Z","timestamp":1751659529000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632849"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":114,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632849"],"URL":"https:\/\/doi.org\/10.1145\/3632849","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}