TY - JOUR
T1 - Exploration of language specifications by compilation to first-order logic
AU - Grewe, Sylvia
AU - Erdweg, Sebastian
AU - Pacak, André
AU - Raulf, Michael
AU - Mezini, Mira
N1 - Accepted Author Manuscript
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
KW - Declarative languages
KW - Domain-specific languages
KW - First-order theorem proving
KW - Formal specification
KW - Type systems
UR - http://www.scopus.com/inward/record.url?scp=85028400628&partnerID=8YFLogxK
UR - http://resolver.tudelft.nl/uuid:8238a0cc-6466-434a-9627-c1416795d9af
U2 - 10.1016/j.scico.2017.08.001
DO - 10.1016/j.scico.2017.08.001
M3 - Article
AN - SCOPUS:85028400628
SN - 0167-6423
VL - 155
SP - 146
EP - 172
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -