Creating Formal Specifications with Analogical Reasoning

We describe the Arís (Analogical Reasoning for Implementations and Specifications) system that uses analogical reasoning to create formal specifications for a given implementation. Arís is built on the hypothesis that structurally similar implementations often represent similar functionality. It leverages this similarity to create new specifications, by analogy to a retrieved similar example. Of course some similarly structured implementations provide different functionality, so a major focus of Arís is to discriminate between analogous and dis-analogous pairs of code. Examples are used to highlight Arís’ ability to create specifications, across a range of similar implementations and even similar algorithms. Results are presented on Arís ability to create verified specifications for a sample of ten textbook problems. We argue that Arís both emulates and supports the workaday little-c creativity of formal software developers