Verifying Graph Programs with First-Order Logic
| Autor: | Detlef Plump, Gia Septiana Wulandari |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Programming language Computer science computer.software_genre Logic in Computer Science (cs.LO) First-order logic Precondition TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Formal specification Postcondition Graph (abstract data type) Graph property Nested loop join computer |
| Zdroj: | GCM@STAF |
| ISSN: | 2075-2180 |
| DOI: | 10.4204/eptcs.330.11 |
| Popis: | We consider Hoare-style verification for the graph programming language GP 2. In previous work, graph properties were specified by so-called E-conditions which extend nested graph conditions. However, this type of assertions is not easy to comprehend by programmers that are used to formal specifications in standard first-order logic. In this paper, we present an approach to verify GP 2 programs with a standard first-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain strongest liberal postconditions for arbitrary loop-free programs. Compared with previous work, this allows to reason about a vastly generalised class of graph programs. In particular, many programs with nested loops can be verified with the new calculus. Comment: In Proceedings GCM 2020, arXiv:2012.01181. arXiv admin note: substantial text overlap with arXiv:2010.14549 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|