A First-order Logic with Frames
| Autor: | Adithya Murali, Lucas Peña, P. Madhusudan, Christof Löding |
|---|---|
| Rok vydání: | 2023 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Theoretical computer science Computer science 02 engineering and technology Separation logic Translation (geometry) Article Meaning (philosophy of language) Fragment (logic) Computer Science::Logic in Computer Science 0202 electrical engineering electronic engineering information engineering Program Verification First-Order Logic with Recursive Definitions First-Order Logic Frame (networking) 020207 software engineering Construct (python library) Logic in Computer Science (cs.LO) First-order logic Program Logics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Heap Verification 020201 artificial intelligence & image processing Software Program logic |
| Zdroj: | Cham, Switzerland : Springer, Lecture notes in computer science 12075, Theoretical Computer Science and General Issues 515-543 (2020). doi:10.1007/978-3-030-44914-8_19 Programming languages and systems : 29th European Symposium on Programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020: proceedings / Peter Müller (ed.) Programming languages and systems : 29th European Symposium on Programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020: proceedings / Peter Müller (ed.)29. European Symposium on Programming, ESOP 2020, online, 2020-04-25-2020-04-30 Programming Languages and Systems ISBN: 9783030449131 ESOP Programming Languages and Systems |
| ISSN: | 1558-4593 0164-0925 |
| DOI: | 10.1145/3583057 |
| Popis: | We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formulas -- the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL. This manuscript is an extended and revised version of the publication with the same title that appeared at ESOP 2022 (https://doi.org/10.1007/978-3-030-44914-8_19). It is currently under review |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|