Exploration of language specifications by compilation to first-order logic

Grewe, Sylvia; Erdweg, S.T.; Pacak, André; Raulf, Michael; Mezini, Mira

doi:10.1016/j.scico.2017.08.001

Exploration of language specifications by compilation to first-order logic

Title

Exploration of language specifications by compilation to first-order logic

Author

Grewe, Sylvia (Technische Universität Darmstadt)
Erdweg, S.T. (TU Delft Programming Languages)
Pacak, André (Technische Universität Darmstadt)
Raulf, Michael (Technische Universität Darmstadt)
Mezini, Mira (Technische Universität Darmstadt)

Date

2018

Abstract

Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we translate language specifications and exploration tasks to first-order logic, which many ATPs accept as input. However, there are several different strategies for compiling a language specification to first-order logic, and even small variations in the translation may have a large impact on the time it takes ATPs to find proofs. In this paper, we first present a systematic empirical study on how to best compile language specifications to first-order logic such that existing ATPs can solve typical exploration tasks efficiently. We have developed a compiler product line that implements 36 different compilation strategies and used it to feed language specifications to 4 existing first-order theorem provers. As benchmarks, we developed language specifications for typed SQL and for a Questionnaire Language (QL), with 50 exploration goals each. Our study empirically confirms that the choice of a compilation strategy greatly influences prover performance in general and shows which strategies are advantageous for prover performance. Second, we extend our empirical study with 4 domain-specific strategies for axiom selection and find that axiom selection does not influence prover performance in our benchmark specifications.

Subject

Declarative languages
Domain-specific languages
First-order theorem proving
Formal specification
Type systems

To reference this document use:

http://resolver.tudelft.nl/uuid:8238a0cc-6466-434a-9627-c1416795d9af

DOI

https://doi.org/10.1016/j.scico.2017.08.001

Embargo date

2020-03-06

ISSN

0167-6423

Source

Science of Computer Programming, 155, 146-172