AbsSpec

AbsSpec is a tool to automatically infer specifications from Curry programs. Program specifications (in particular, automatically derived specifications) have been used for program verification, understanding, documentation, service discovering or testing. Our tool, statically infers from the source code of a Curry program a specification which consists of a set of equations relating (nested) operation calls that have the same behavior. We propose a (white-box) semantic-based inference method which relies on the (fully-abstract condensed) semantics of (Bacci 2011) for achieving, to some extent, the correctness of the inferred specification.

A prototype of the AbsSpec tool is available here.