Exploration of language specifications by compilation to first-order logic

Sylvia Grewe*, Sebastian Erdweg, André Pacak, Michael Raulf, Mira Mezini

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

3 Citations (Scopus)
39 Downloads (Pure)

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.

Original languageEnglish
Pages (from-to)146-172
Number of pages27
JournalScience of Computer Programming
Volume155
DOIs
Publication statusPublished - 2018

Bibliographical note

Accepted Author Manuscript

Keywords

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

Fingerprint

Dive into the research topics of 'Exploration of language specifications by compilation to first-order logic'. Together they form a unique fingerprint.

Cite this