This is a short comparison report about a verification task solved with KeY, Why3, Dafny and Frama-C.
The original challenge comes from a real-world situation. There is no particular “trick” needed for the specification and verification; it is rather straightforward. Yet, the required annotations to achieve the specification are not too few – making the example a good opportunity to compare different specification languages.
The original problem is a GUI bug in KeY where tooltips suffered from very long lines. A routine to wrap these tooltips had to be written. To make it correct, it has been formally proven in KeY (yielding the first KeY-proven code inside KeY!). Jean-Christophe and Andrei from the Why3 team then kindly contributed a provenly correct solution in Why3. A literal translation of the KeY solution to Dafny gives us a third comparison partner in Dafny. Lionel provided a version in Frama-C.
A simpler version of this example has been proposed as the microchallenge in a recent KeY tutorial.
Implement a method
wrapLines that wrap lines such that a maximum line length is not exceeded. It receives a string in form of a mutable character array and a positive desired length of lines. The array may already contain newline-characters when the method is called.
wrapLinesdoes not raise any runtime error and always terminates (normally).
wrapLineschanges at most entries in the array, and only replaces spaces by newline characters.
- If, after
wrapLinesterminates, there are more than
lineLengthcharacters in a row without newline characters among them, then there are also no spaces among them. (Impossible to break …)
wrapLinesintroduces a newline character at index
k, then there is no possibility that the line terminated at
kcould have been made longer without exceeding the desired length of lines.
|Tool||Languages||Simple challenge||Challenge||Code Language|
|KeY||Java + JML||Link||Link||Java|
|Frama-C||ACSL + C||Link||Link||C|
Simple Challenge refers to the microchallenge in the tutorial.
Code Language refers to the language for the executable version of the specified code.
(Update 2021-04-13: Added Frama-C)