Paul Attie, Fadi Zaraket, Mohamad Noureddine, and Farah Al-Hariri
abstract
The problem of writing a functional specification which re- flects the intentions of the developer has long been recognized as fun- damental. We propose a method to construct (synthesize) a functional specification for a terminating program which takes a single input and produces a single output. The specification consists of a precondition and a postcondition, expressed as first-order logic wff’s, including quan- tifiers. The user provides an underlying type theory for the variables used to write the specification, and also answers a series of queries, which make precise her intentions. Each query presents an example of the relevant data: input for precondition, input-output pair for postcondition. The developer states whether the precondition (postcondition, respectively) being written should hold or not (according to the users intentions). By grouping examples into equivalence classes, we reduce the number of queries to finite. After one query for each equivalence class has been answered, the method outputs a formula for the precondition (postcondi- tion, respectively) that the user intends. By using various pruning strate- gies, and by constructing a formula using simpler formulae that have been previously constructed, we further reduce the number of queries to the point that our method is practical. Our method constructed, in reason- able time, accurate specifications for array search, binary heap, binary search, linked list, and trie.
The following tarball contains the code of the specification construction algorithm. You can build it using the make command on a linux machine (cygwin for windows). It also contains a copy of the Z3 solver for convenience.
Use the sc binary with the runTh script for the specification construction algorithm.
Use the ma binary with the runMA script for the make vocabulary adequate algorithm.
Following is a user experiment and its corresponding session files.
user experiment 1 instructions user experiment 2 instructions
Sample user session files:
The following is a sample report fully specifying the trie data structure trie specs.
Paul Attie, Fadi Zaraket, Mohamad Noureddine, and Mohamad Fawaz
The problem of writing a specification which accurately reflects the intent of the developer has long been recognized as fundamental. We propose a method and a supporting tool to write and check a specification and an implementation using a set of use cases, \ie input-output pairs that the developer supplies. These are instances of both good (correct) and bad (incorrect) behavior. We assume that the use cases are accurate, as it is easier to generate use cases than to write an accurate specification. We incrementally construct a specification (precondition and postcondition) based on semantic feedback generated from these use cases. We check the accuracy of the constructed specification using two proposed algorithms. The first algorithm checks the accuracy of the specification against an automatically generated specification from a supplied finite domain of use cases. The second checks the accuracy of the specification via reducing its domain to a finite yet equally satisfiable domain if possible. When the specification is mature, we start to also construct a program that satisfies the specification. However, our method makes provision for the continued modification of the specification, if needed. We illustrate our method with two examples; linear search and text justify.
The code can be found at http://research-fadi.aub.edu.lb/speccheck/cg.tgz
You can build the code on linux or on windows platforms with the gnu make command (we used cygwin on windows). In addition to the above you need the Qt 4.6.X libraries, the Z3 SMT solver libraries, and the antlr tool and libraries for C (libantlr3.2c). Place links to each of them appropriately under the cg/third directory. We will place a tarball for the needed libraries for convenience shortly on this page, please use it only if really needed.
The linear search example can be found at http://research-fadi.aub.edu.lb/speccheck/linearSearch.c
The linear search example can be found at http://research-fadi.aub.edu.lb/speccheck/justify.c
Paul Attie, Fadi Zaraket, Mohamad Noureddine, Farah Al-Hariri, and Mohamad fawaz