An evolutionary approach to translating operational specifications into declarative specifications

FACUNDO MOLINA; CÉSAR CORNEJO; GERMÁN REGIS; PABLO F. CASTRO; NAZARENO AGUIRRE; MARCELO FRIAS

SCIENCE OF COMPUTER PROGRAMMING

ELSEVIER SCIENCE BV

Lugar: Amsterdam; Año: 2019 vol. 181 p. 47 - 63

0167-6423

Various tools for program analysis, including run-time assertion checkers and static analyzers such as verification and test generationtools, require formal specifications of the programs being analyzed. Moreover, many of these tools and techniques require such specifications to bewritten in a particular style, or follow certain patterns, in order to obtain an acceptable performance from the corresponding analyses. Thus,having a formal specification sometimes is not enough for using a particular technique, since such specification may not be provided in the rightformalism. In this paper, we deal with this problem in the increasinglycommon case of having an operational specification, while for analysisreasons requiring a declarative specification. We propose an evolutionaryapproach to translate an operational specification written in a sequential programming language, into a declarative specification, in relationallogic. We perform experiments on a benchmark of data structure implementations, that show that translating representation invariants usingour approach and verifying invariant preservation using the resultingspecifications outperforms verification with specifications obtained using an existing semantics-preserving translation. Also, our evolutionarycomputation translation achieves very good precision in this context