Testing of KeY

Usage of RunAllProofs JUnit implementation

May 2015 Kai Wallisch

RunAllProofs is a test routine in KeY verifying that a set of .key files can be opened and proven by the KeY prover without user interaction. Proofs created during a test are reloaded after saving them to the file system to test the save/load mechanism. Also, RunAllProofs verifies that another set of .key files (containing invalid statements) can not be proven automatically.

The previous version of RunAllProofs was realized as a Perl script. This has now been replaced by a Java JUnit implementation. Main benefits of the new implementation are:

RunAllProofs Invocations

The following possibilities are currently available to start a RunAllProofs test run:

ant -buildfile key/key.core.test/build.xml runAllProofs

The recommended tool for a user to execute RunAllProofs locally is by executing the shell script key/scripts/runAllProofs. Invocation of this script without any arguments starts a RunAllProofs test run with standard settings. Check output of key/scripts/runAllProofs --help to see available command line parameters.

Executing ant task runAllProofs should do the same as the command line script. It is recommended over ant task test-deploy for local test runs.

Syntax of the Proof Collection/Index File

There is an proof collection (or index) file containing the declaration the sets of .key files that will be tested during RunAllProofs test run. This file is currently located in KeY git-repository at: key/key.ui/examples/index/automaticJAVADL.txt.

A small antlr parser was written for this file. Corresponding antlr grammar is located at: key/key.core.test/src/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.g.

The proof collection file is composed of the following components:

The different components are explained below. It is recommended to look up automaticJAVADL.txt as an example.

Comments


The following comment styles are supported:

# Single-line shell-style comment

// Single-line C-style comment

/*
 * Multi-line C-style comment
 */

Settings Declarations

Proof collections settings entries are key-value pairs, which must occur before the first test group declaration. The following syntax is used for settings declarations:

  key = value

A key is an arbitrary identifier composed of letters and digits starting with a letter. Value can be either of the following:

Examples:

baseDirectory = ../
statisticsFile = ../../key.core.test/testresults/runallproofs/runStatistics.csv
forkMode = perGroup
reloadEnabled = true
userName = "Foo Bar"
tempDir = ../../key.core.test/runallproofs_tmp
multiLine = "String literals
             may contain line breaks!"

The following settings are currently supported:

Note

The available options are also listed in automaticJAVADL.txt. You should look there, too.

Proof collection settings can be specified in the following ways:

If a settings key is assigned mutltiple times at different places, the declaration with the highest priority takes precedence for that key. Priorities are determined according to the following order:

Proof collection parser is forgiving in the sense that unknown settings are parsed without an error (unless they are syntactically incorrect) but will not influence a test run. Caution: Typos in settings may thus escape the developer's notice!

Declarations of test groups

Test groups can be declared in two different ways in a proof collection file. Either explicitly grouped or ungrouped. Test Files that are grouped together will be executed in the same subprocess when fork mode "perGroup" is activated. Each individual file gets its own subprocess in fork mode "perFile" (regardless of groups). The files are declared by a path name (which is treated relative to base directory) preceded by a test property to be verified.

All settings declarations must precede test group declarations. However, groups can have custom settings declarations, overriding the gloval settings. These settings must precede .key files (see example below) within the group declarations.

The following test properties are currently supported:

Example for a group declaration with custom/local settings:

  group newBook {
    forkMode = perFile
    reloadEnabled = false
    provable ./newBook/09.list_modelfield/ArrayList.add.key
    provable ./newBook/09.list_modelfield/ArrayList.remFirst.key
    provable ./newBook/09.list_modelfield/ArrayList.empty.key
    provable ./newBook/09.list_modelfield/ArrayList.size.key
    provable ./newBook/09.list_modelfield/ArrayList.get.key
  }

.key file declarations are also allowed outside of groups, for example:

  provable ./standard_key/java_dl/methodCall.key
  notprovable ./standard_key/java_dl/jml-min/min-unprovable1.key

which is similar to the following explicit group declarations:

  group methodCall.key {
    provable ./standard_key/java_dl/methodCall.key
  }
  group min-unprovable1.key {
    notprovable ./standard_key/java_dl/jml-min/min-unprovable1.key 
  }

Fork Modes

There are different fork mode settings available which influence how often fresh Java virtual machines (JVM) are launched during RunAllProofs test run. Default is the value "noFork" which prevents RunAllProofs from launching Java processes entirely (everything is executed within the VM running the test). However, in case memory leaks occur and have a significant impact on test performance, it is recommended to use one of the other available fork mode settings.

The following fork modes are available:

Example: Setting fork mode to "perFile" can be done with the following line in automaticJAVADL.txt:

forkMode = perFile

Test Statistics

In case a path is specified via settings key "statisticsFile", RunAllProofs will save proof statistics to that file. It contains information about runtime, memory consumption, rule applications and others.

Example for declaration of a statistics file in automaticJAVADL.txt:

statisticsFile = ../../key.core.test/testresults/runallproofs/runStatistics.csv

Proof Reloading

RunAllProofs will attempt to reload proofs that were retrieved during a successful proof attempt for files that are marked provable. Proof reloading can be disabled via settings key reloadEnabled as follows:

reloadEnabled = true