Verifiable Semantic Difference Languages
| Autor: | Thibaut Girka, Yann Régis-Gianas, David Mentré |
|---|---|
| Přispěvatelé: | Mitsubishi Electric R&D Centre Europe [France] (MERCE-France), Mitsubishi Electric [France], Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Soundness
Theoretical computer science [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Syntax (programming languages) Semantics (computer science) Programming language Computer science Proof assistant 020207 software engineering Static program analysis 0102 computer and information sciences 02 engineering and technology Hoare logic computer.software_genre 01 natural sciences Oracle Imperative programming 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering computer |
| Zdroj: | International Symposium on Principles and Practice of Declarative Programming International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131870⟩ PPDP |
| Popis: | International audience; Program differences are usually represented as textual differences on source code with no regard to its syntax or its semantics. In this paper, we introduce semantic-aware difference languages. A difference denotes a relation between program reduction traces. A difference language for the toy imperative programming language Imp is given as an illustration. To certify software evolutions, we want to mechanically verify that a difference correctly relates two given programs. Product programs and correlating programs are effective proof techniques for relational reasoning. A product program simulates, in the same programming language as the compared programs, a well-chosen interleaving of their executions to highlight a specific relation between their reduction traces. While this approach enables the use of readily-available static analysis tools on the product program, it also has limitations: a product program will crash whenever one of the two programs under consideration crashes, thus making it unsuitable to characterize a patch fixing a safety issue. We replace product programs by correlating oracles which need not be expressed in the same programming language as the compared programs. This allows designing correlating oracle languages specific to certain classes of program changes and capable of relating crashing programs with non-crashing ones. Thanks to oracles, the primitive differences of our difference language on Imp can be assigned a verifiable semantics. Besides, each class of oracles comes with a specific proof scheme which simplifies relational reasoning for a well-specified class of relations. We also prove that our framework is at least as expressive as several Relational Hoare Logic variants by encoding them as correlating oracles, (re)proving sound-ness of those variants in the process. The entirety of the framework as well as its instantiations have been defined and proved correct using the Coq proof assistant. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|