Line 47: | Line 47: | ||
negativeExamples.add(new Example().addf(new VariableExample("floor", "-2"))); | negativeExamples.add(new Example().addf(new VariableExample("floor", "-2"))); | ||
</pre> | </pre> | ||
The method <b>addf()</b> is just a wrapper for a Java set's <b>add()</b> method enabling a functional style. | |||
Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>: | Afterwards, we are able to run synthesis using <b>synthesizePredicate()</b>: | ||
<pre> | <pre> |
Program synthesis is the task of generating executable programs from a given specification usually considering a domain specific language. There are many ways to specify the behavior of a program to be synthesized like logical or mathematical formulae (e.g., in the form of pre- and post-conditions) or explicit input-output examples. The ProB Prolog core provides an implementation to synthesize B predicates or complete machine operations from explicit state input-output examples. The ProB2 Java API provides an interface to utilize the program synthesis backend. The implemented synthesis technique is based on the work by Susmit Jha, Sumit Gulwani et al. [1] A synthesis task is encoded as a constraint satisfaction problem in B using the ProB constraint solver and its available backends to find valid solutions.
In order to use the synthesis backend we expect the B machine to be loaded for which B code should be synthesized. The input-output examples describing the behavior of a program to be synthesized then refer to a subset of machine variables. In particular, synthesis expects a set of positive and negative examples. In case of synthesizing a B predicate, the synthesized predicate is true for the positive examples and false for the negative examples. Here, an example is a single machine state (input). In case of synthesizing a B machine operation, the positive examples are used to synthesize the B operation's substitution while both sets of examples are used to synthesize an appropriate precondition for the operation if necessary. Here, an example consists of inputs and outputs, i.e., before- and after-states.
The main class is BSynthesizer which expects the statespace of a currently loaded B machine on construction:
BSynthesizer synthesizer = new BSynthesizer(stateSpace);
Using input-output examples to specify the behavior of a program is most comfortable for the user but most difficult for program synthesis itself. As input-output examples possibly describe ambiguous behavior we provide two modes for synthesis:
The synthesis mode can be set using the method setSynthesisMode():
synthesizer.setSynthesisMode(SynthesisMode.INTERACTIVE);
We provide three classes to create examples:
As mentioned above one can either synthesize a B predicate or a complete machine operation. To do so, a BSynthesizer object provides two methods synthesizePredicate() and synthesizeOperation().
Synthesizing a B predicate expects a set of positive examples and a set of negative examples. For instance, assume we have loaded a machine that has an integer variable called "floor" and want to synthesize the predicate "floor > 0". First, we create the set of positive and negative examples:
HashSet<Example> positiveExamples = new HashSet<>(); positiveExamples.add(new Example().addf(new VariableExample("floor", "1"))); positiveExamples.add(new Example().addf(new VariableExample("floor", "2"))); positiveExamples.add(new Example().addf(new VariableExample("floor", "3"))); HashSet<Example> negativeExamples = new HashSet<>(); negativeExamples.add(new Example().addf(new VariableExample("floor", "0"))); negativeExamples.add(new Example().addf(new VariableExample("floor", "-1"))); negativeExamples.add(new Example().addf(new VariableExample("floor", "-2")));
The method addf() is just a wrapper for a Java set's add() method enabling a functional style. Afterwards, we are able to run synthesis using synthesizePredicate():
try { BSynthesisResult solution = synthesizer.synthesizePredicate(positiveExamples, negativeExamples); if (solution.isProgram()) { SynthesizedProgram synthesizedProgram = (SynthesizedProgram) solution; System.out.println("Predicate: " + synthesizedProgram); } } catch (BSynthesisException e) { // }
A BSynthesisResult is either a program or a distinguishing example depending on the selected synthesis mode. If synthesis fails, an exception is thrown providing an appropriate error message.
Now assume that we want to synthesize a B machine operation that increases the variable "floor" by one. Again, we first create the set of positive and negative examples which are now examples for input and output:
positiveIOExamples.add(new IOExample( new Example().addf(new VariableExample("floor", "0")), new Example().addf(new VariableExample("floor", "1")))); positiveIOExamples.add(new IOExample( new Example().addf(new VariableExample("floor", "1")), new Example().addf(new VariableExample("floor", "2")))); positiveIOExamples.add(new IOExample( new Example().addf(new VariableExample("floor", "2")), new Example().addf(new VariableExample("floor", "3"))));
Afterwards, we are able to run synthesis:
try { BSynthesisResult solution = bSynthesizer.synthesizeOperation(positiveIOExamples, new HashSet<>(), lib); if (solution.isProgram()) { SynthesizedProgram synthesizedProgram = (SynthesizedProgram) solution; System.out.println("Operation: " + synthesizedProgram); } } catch (BSynthesisException e) { // }
Note, we do not provide any negative examples but pass an empty set. If we would provide negative input-output examples, an appropriate precondition would be synthesized for the machine operation. That is, the synthesized operation is enabled for the inputs of the positive examples and disabled for the inputs of the negative examples.
The employed synthesis technique is based on the combination of program components and, thus, requires a predefined set of library components. For instance, an integer addition is such a library component. If using synthesis as described above, a default library configuration is used. This default configuration tries to use as little components as possible and successively intermingles components or increases the amount of specific components if no solution can be found using the current library configuration. As this default library configuration is mainly selected randomly, synthesis possibly lacks for performance compared to using the exact library of components that is necessary to synthesize a program. To that effect, the user is also able to specify the exact library configuration to be considered during synthesis. We provide the class BLibrary to create a specific library configuration.
The enum LibraryComponentName provides all B components that are supported by the synthesis backend. Constructing a BLibrary object provides an empty library considering the default configuration. We thus have to state that we want to use a specific library of components only and add the desired components using their names. For instance, we want to create a component library using an integer addition and subtraction:
BLibrary lib = new BLibrary(); lib.setUseDefaultLibrary(false); lib.addLibraryComponent(LibraryComponentName.ADD); lib.addLibraryComponent(LibraryComponentName.MINUS);
A BLibrary object can be passed as the third argument for synthesizePredicate() and synthesizeOperation() respectively.
The employed synthesis technique is based on constraint solving and, thus, each component has a unique output within a synthesized program. For instance, to synthesize the predicate "x + y + z > 2" we need two addition components. There are three ways to adapt the amount how often a specific component should be considered:
Moreover, one can define whether synthesis should consider constants that have to be enumerated by the solver by using the method setEnumerateConstants(). If is false, only constants that are in the scope of the currently loaded machine are considered. For instance, if the current machine does not define any integer constant and we want to synthesize a predicate "x + 1 > y" the constraint solver needs to enumerate an integer constant to the value of 1 to achieve the desired behavior. If synthesizing an operation, one can further define whether if-statements should be considered during synthesis represented by the enum ConsiderIfType. There are three possibilities: