Proving Line Wrapping in KeY, Why3, Dafny and Frama-C

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.

Motivation

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.

Informal specification

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.

  1. wrapLines does not raise any runtime error and always terminates (normally).
  2. wrapLines changes at most entries in the array, and only replaces spaces by newline characters.
  3. If, after wrapLines terminates, there are more than lineLength characters in a row without newline characters among them, then there are also no spaces among them. (Impossible to break …)
  4. If wrapLines introduces a newline character at index k, then there is no possibility that the line terminated at k could have been made longer without exceeding the desired length of lines.

Solutions

Tool Languages Simple challenge Challenge Code Language
KeY Java + JML Link Link Java
Why3 WhyML Link Link OCaml
Dafny Dafny Link C#
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)

Posted on by Mattias Ulbrich