Hoare-Style Verification of Graph Programs

• Autorzy: Poskitt C. M. , Plump D.
• Języki publikacji: EN

Abstrakty

EN

GP (for Graph Programs) is an experimental nondeterministic programming language for solving problems on graphs and graph-like structures. The language is based on graph transformation rules, allowing visual programming at a high level of abstraction. In particular, GP frees programmers from dealing with low-level data structures. In this paper, we present a Hoare-style proof system for verifying the partial correctness of (a subset of) graph programs. The pre- and postconditions of the calculus are nested graph conditions with expressions, a formalism for specifying both structural graph properties and properties of labels. We show that our proof system is sound with respect to GP’s operational semantics and give examples of its use.

Słowa kluczowe

EN

Graph Programs; graph transformation; abstract syntax

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 118, nr 1-2
• Strony: 135--175
• Opis fizyczny: Bibliogr. 37 poz., rys.

Twórcy

autor

Poskitt C. M.

autor

Plump D.

• Department of Computer Science, The University of York, Deramore Lane, York, YO10 5GH, United Kingdom,

Bibliografia

• [1] Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, third edition, 2009.
• [2] Adam Bakewell, Detlef Plump, and Colin Runciman. Checking the shape safety of pointer manipulations. In Int. Seminar on Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers, volume 3051, pages 48-61. Springer-Verlag, 2004.
• [3] Adam Bakewell, Detlef Plump, and Colin Runciman. Specifying pointer structures by graph reduction. In Applications of Graph Transformations With Industrial Relevance (AGTIVE 2003), Revised Selected and Invited Papers, volume 3062, pages 30-44. Springer-Verlag, 2004.
• [4] Paolo Baldan, Andrea Corradini, and Barbara König. A framework for the verification of infinite-state graph transformation systems. Information and Computation, 206(7):869-907, 2008.
• [5] Enrico Biermann, Claudia Ermel, and Gabriele Taentzer. Precise semantics of EMF model transformations by graph transformation. In Proc. Model Driven Engineering Languages and Systems (MoDELS 2008), volume 5301, pages 53-67. Springer-Verlag, 2008.
• [6] Dénes Bisztray, Reiko Heckel, and Hartmut Ehrig. Compositional verification of architectural refactorings. In Proc. Architecting Dependable Systems VI (WADS 2008), volume 5835, pages 308-333. Springer-Verlag, 2009.
• [7] Stephen A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, 7(1):70-90, 1978.
• [8] Rubino Geiß, Gernot Veit Batz, Daniel Grund, Sebastian Hack, and Adam M. Szalkowski. GrGen: A fast SPO-based graph rewriting tool. In Proc. International Conference on Graph Transformation (ICGT 2006), volume 4178, pages 383-397. Springer-Verlag, 2006.
• [9] Lars Grunske, Leif Geiger, Albert Zündorf, Niels Van Eetvelde, Pieter Van Gorp, and Dániel Varró. Using graph transformation for practical model-driven software engineering. In Sami Beydeda,Matthias Book, and Volker Gruhn, editors, Model-Driven Software Development, pages 91-117. Springer-Verlag, 2005.
• [10] Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 19(2):245-296, 2009.
• [11] Annegret Habel, Karl-Heinz Pennemann, and Arend Rensink. Weakest preconditions for high-level programs. In Proc. Graph Transformations (ICGT 2006), volume 4178, pages 445-460. Springer-Verlag, 2006.
• [12] Annegret Habel and Detlef Plump. Computational completeness of programming languages based on graph transformation. In Proc. Foundations of Software Science and Computation Structures (FOSSACS 2001), volume 2030, pages 230-245. Springer-Verlag, 2001.
• [13] Annegret Habel and Detlef Plump. Relabelling in graph transformation. In Proc. International Conference on Graph Transformation (ICGT 2002), volume 2505, pages 135-147. Springer-Verlag, 2002.
• [14] Annegret Habel and Hendrik Radke. Expressiveness of graph conditions with variables. In Proc. Colloquium on Graph and Model Transformation on the Occasion of the 65th Birthday of Hartmut Ehrig, volume 30 of Electronic Communications of the EASST, 2010.
• [15] Frank Hermann, Hartmut Ehrig, Fernando Orejas, and Ulrike Golas. Formal analysis of functional behavior for model transformations based on triple graph grammars. In Proc. Graph Transformations (ICGT 2010), volume 6372, pages 155-170. Springer-Verlag, 2010.
• [16] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969.
• [17] Karsten Hölscher, Paul Ziemann, andMartin Gogolla. On translating UML models into graph transformation systems. Journal of Visual Languages Computing, 17(1):78-105, 2006.
• [18] Marieke Huisman and Bart Jacobs. Java program verification via a Hoare Logic with abrupt termination. In Proc. Fundamental Approaches to Software Engineering (FASE 2000), volume 1783, pages 284-303. Springer-Verlag, 2000.
• [19] Barbara König and Javier Esparza. Verification of graph transformation systems with context-free specifications. In Proc. Graph Transformations (ICGT 2010), volume 6372, pages 107-122. Springer-Verlag, 2010.
• [20] Barbara König and Vitali Kozioura. Towards the verification of attributed graph transformation systems. In Proc. Graph Transformations (ICGT 2008), volume 5214, pages 305-320. Springer-Verlag, 2008.
• [21] Sabine Kuske, Martin Gogolla, Hans-Jörg Kreowski, and Paul Ziemann. Towards an integrated graph-based semantics for UML. Software and Systems Modeling, 8:403-422, 2009.
• [22] Greg Manning and Detlef Plump. The GP programming system. In Proc. Graph Transformation and Visual Modelling Techniques (GT-VMT 2008), volume 10 of Electronic Communications of the EASST, 2008.
• [23] Ulrich Nickel, Jörg Niere, and Albert Zündorf. The FUJABA environment. In Proc. International Conference on Software Engineering (ICSE 2000), pages 742-745. ACM Press, 2000.
• [24] Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Springer-Verlag, 2007.
• [25] Tobias Nipkow. Hoare logics in Isabelle/HOL. In Helmut Schwichtenberg and Ralf Steinbrüggen, editors, Proof and System-Reliability, pages 341-367. Kluwer Academic Publishers, 2002.
• [26] Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987.
• [27] Rinus Plasmeijer andMarko van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, 1993.
• [28] Detlef Plump. The graph programming language GP. In Proc. Algebraic Informatics (CAI 2009), volume 5725, pages 99-122. Springer-Verlag, 2009.
• [29] Detlef Plump and Sandra Steinert. The semantics of graph programs. In Proc. Rule-Based Programming (RULE 2009), volume 21 of Electronic Proceedings in Theoretical Computer Science, pages 27-38, 2010.
• [30] Arnd Poetzsch-Heffter and Peter Müller. A programming logic for sequential Java. In Proc. Programming Languages and Systems (ESOP 1999), pages 162-176, 1999.
• [31] Christopher M. Poskitt and Detlef Plump. A Hoare calculus for graph programs. In Proc. International Conference on Graph Transformation (ICGT 2010), volume 6372, pages 139-154. Springer-Verlag, 2010.
• [32] Arend Rensink, ákos Schmidt, and Dániel Varró. Model checking graph transformations: A comparison of two approaches. In Proc. Graph Transformations (ICGT 2004), volume 3256, pages 226-241. Springer-Verlag, 2004.
• [33] Stefan Rieger and Thomas Noll. Abstracting complex data structures by hyperedge replacement. In Proc. Graph Transformations (ICGT 2008), volume 5214, pages 69-83. Springer-Verlag, 2008.
• [34] Andy Schürr, Andreas Winter, and Albert Zündorf. The PROGRES approach: Language and environment. In H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozenberg, editors, Handbook of Graph Grammars and Computing by Graph Transformation, volume 2, chapter 13, pages 487-550.World Scientific, 1999.
• [35] Gabriele Taentzer. AGG: A graph transformation environment for modeling and validation of software. In Applications of Graph Transformations With Industrial Relevance (AGTIVE 2003), Revised Selected and Invited Papers, volume 3062, pages 446-453. Springer-Verlag, 2004.
• [36] Dániel Varró, Gergely Varró, and András Pataricza. Designing the automatic transformation of visual languages. Science of Computer Programming, 44(2):205-227, 2002.
• [37] David von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13):1173-1214, 2001.