Coverage of Formal Specifications

This page supplies additional material for the extended abstract “Assessing the Coverage of Formal Specifications“, submitted to the PhD symposium “Algorithms, Tools and Applications” at iFM 2017.

In the extended abstract, we discussed a simple “find” method trying to discover an element in an integer array and returning its index, or -1 if the element was not present. In the section below, you find the source code of the method, along with the strongest JML specification that we discovered using our tool. Afterward, we present several specifications and the results produced for them by the tool. Finally, we provide an executable of the prototype with some usage instructions.

Update (2017/10/09): There is a new version of the tool which deviates in its output from the one discussed in the extended abstract. You find it here. The category of “use case facts” has been removed, the output is more verbose, and it features the possibility of interaction with the generated proof (e.g., to manually recover from prover incapacities). Also, the GUI has been improved.

Source code and Strongest Specification for “find”

Different Specifications for “find”

The following table shows the different specification versions for “find” which we studied, ordered by increasing strenght / coverage.

   \result == -1
|| arr[\result] == n

true

   \result == -1
|| arr[\result] == n

   result == -1
|| arr[result] == n

   \result == -1
|| arr[\result] == n

   i >= 0 && i <= arr.length
&& (   result != -1
    || (\forall int k; k >= 0 && k < i; arr[k] != n))
&& (   result == -1
    || arr[result] == n)

   \result == -1
|| arr[\result] == n

   i >= 0 && i <= arr.length
&& (   result != -1
    || (\forall int k; k >= 0 && k < i; arr[k] != n))
&& (   result == -1
    || arr[result] == n && result == i-1)

   ((\exists int i; i >= 0
                 && i < arr.length;
                    arr[i] == n)
       ==> arr[\result] == n)
&& ((\forall int i; i >= 0
                 && i < arr.length;
                    arr[i] != n)
       ==> \result == -1)

   i >= 0 && i <= arr.length
&& (   result != -1
    || (\forall int k; k >= 0 && k < i; arr[k] != n))
&& (   result == -1
    || arr[result] == n && result == i-1)

   ((\exists int i; i >= 0
                 && i < arr.length;
                    arr[i] == n)
       ==> arr[\result] == n)
&& ((\forall int i; i >= 0
                 && i < arr.length;
                    arr[i] != n)
       ==> \result == -1)

   i >= 0 && i <= arr.length
&& i = iLastRun + 1
&& (   result != -1
    || (\forall int k; k >= 0 && k < i; arr[k] != n))
&& (   result == -1
    || arr[result] == n && result == i-1)

ghost int iLastRun = i - 1;

   ((\exists int i; i >= 0
                 && i < arr.length;
                    arr[i] == n)
       ==>    arr[\result] == n
           && \result == f_iLastRun)
&& ((\forall int i; i >= 0
                 && i < arr.length;
                    arr[i] != n)
       ==> \result == -1)

   i >= 0 && i <= arr.length
&& i = f_iLastRun + 1
&& (   result != -1
    || (\forall int k; k >= 0 && k < i; arr[k] != n))
&& (   result == -1
    || arr[result] == n && result == i-1)

ghost int f_iLastRun = i - 1;

Coverage Results for “find” Specifications

The following table depicts the results produced by our implementation for the specification versions outlined above. “Strength 1” is a percentage coverage of covered and abstractly covered post condition, loop body and use case facts. “Strength 2” only considers covered post condition and loop body facts (so, no use case facts). “Strength 3” is an extension of “Strength 2” which also considers abstractly covered post condition and loop body facts. The values for “Strength 1” and “Strength 3” are only monotonic from the third line on, since in “SimplePost” and “StrongerInv”, there are exception / use case facts uncovered which makes it easier to abstractly cover facts (for instance, “true” abstractly covers all possible facts, but does not exclude any exception and usually does not imply any non-trivial method post condition).

The chart below illustrates the progession of the strength measures.

Tool Download and Usage Instructions

Download the executable of the prototype

After downloading the above ZIP file, just unzip it anywhere on your drive. A Java Runtime Environment of version 8 or higher is required to start the KeY version linked on this page.

To execute the strength analysis CLI, run java -cp KeY.jar de.tud.cs.se.ds.specstr.cli.Main, which will display the following help:

===========================================
            This is  SpecStr v0.1          
a tool for assessing the strength of formal
  specifications using symbolic execution  
===========================================


usage: java -cp KeY.jar de.tud.cs.se.ds.specstr.cli.Main
            [input Java file]
            [fully qualified method name]
 -h,--help                   Display help (this text) and terminate
 -o,--out-file <arg>         Save output to this file
 -p,--proof-out-file <arg>   Save proof to this file

For instance, starting it on the “find” method with the specification SimplePost (by executing java -cp KeY.jar de.tud.cs.se.ds.specstr.cli.Main /path/to/Find.java "Find::find([II)I"), we obtain as output

=====================
Unhandled Exceptions:
=====================

Unclosed exception node "Index Out of Bounds (_arr_0 != null, but i Out of Bounds!)", path condition: "result_1_0 = -1 & ( arr_0.length > i_0 & (arr_0.length <= i_0 | i_0 < 0))"

================
Uncovered Facts:
================

Post condition implies final state fact, Path condition "!result_1_0 = -1"
result = result_1_0

Loop use case fact, Path condition "!result_1_0 = -1"
arr_0[result_1_0]@heap[anon({}, anon_heap_LOOP)] = n

=========================
Abstractly Covered Facts:
=========================

Post condition implies final state fact, Path condition "result_1_0 = -1 & arr_0.length <= i_0"
result = -1

Loop body fact, Path condition "result_1_0 = -1 & (arr_0.length > i_0 & !arr_0[i_0] = n)"
i = 1 + i_0

Loop body fact, Path condition "result_1_0 = -1 & (arr_0.length > i_0 & arr_0[i_0] = n)"
i = 1 + i_0

Covered 3 (0 concretely, 3 abstractly) out of 5 facts
Overall Strength:          30,00%
Concrete Effects Strength: 0,00%
Abstract Effects Strength: 37,50%

The output can be written to a text file using the “-o” flag. With the “-p” flag, you can export the KeY proof tree (which is basically an extension of the symbolic execution tree) on which our analysis works. Then, you can start KeY by just running java -jar KeY.jar and loading the “.proof” file, and inspect the details of the analysis. Basically, everything is handled by dedicated proof rules which are prefixed by “Analyze…”, so you can search in the tree by pressing ctrl + shift + f, entering “Analyze” and jumping from match to match.