A First Step in the Translation of Alloy to Coq
| Autor: | Salwa Souaf, Frédéric Loulergue |
|---|---|
| Přispěvatelé: | Northern Arizona University [Flagstaff], Laboratoire d'Informatique Fondamentale d'Orléans (LIFO), Institut National des Sciences Appliquées - Centre Val de Loire (INSA CVL), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université d'Orléans (UO) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
first order relational logic
Modeling language Computer science Programming language Alloy Assertion translation [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] engineering.material Translation (geometry) computer.software_genre calculus of inductive construction 020204 information systems TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Formal language 0202 electrical engineering electronic engineering information engineering engineering Code (cryptography) computer Scope (computer science) Counterexample |
| Zdroj: | 21st International Conference on Formal Engineering Methods (ICFEM) 21st International Conference on Formal Engineering Methods (ICFEM), 2019, Shenzen, China. ⟨10.1007/978-3-030-32409-4_28⟩ Formal Methods and Software Engineering ISBN: 9783030324087 ICFEM |
| DOI: | 10.1007/978-3-030-32409-4_28⟩ |
| Popis: | International audience; Alloy is both a formal language and a tool for software mod-eling. The language is basically first order relational logic. The analyzer is based on instance finding: it tries to refute assertions and if it succeeds it reports a counterexample. It works by translating Alloy models and instance finding into SAT problems. If no instance is found it does not mean the assertion is satisfied. Alloy relies on the small scope hypothesis: examining all small cases is likely to produce interesting counterexamples. This is very valuable when developing a system. However, Alloy cannot show their absence. In this paper, we propose an approach where Alloy can be used as a first step, and then using a tool we develop, Alloy models can be translated to Coq code to be proved correct interactively. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|