Regression tests for proved rules¶
Changes¶
 Jan 2014, Mattias Ulbrich
 June 2015, Kai Wallisch
The taclet base for KeY grows constantly and it is difficult to oversee that all these rules are sound. It is possible to prove taclets sound within KeY. Such proofs may become invalidated by changes in the taclet database.
We have implemented a test suite which reruns taclet proofs along with the regression tests regularly and thereby ensures that these taclets are sound in every (master) version of KeY.
ProveRules is a JUnit test suite that verifies correctness of taclets by replaying their saved correctness proofs.
In order to add a taclet proof to ProveRules, the following steps are necessary:

Annotate the taclet to be a lemma by adding "\lemma" in front of the taclet's name. For example, the declaration of taclet bsum_empty looks as follows:
\lemma bsum_empty { ... };

Conduct a proof of the taclet by selecting the same taclet from
File > Prove > KeY's Taclets
. (Better to select one at a time). 
Save a proof of the taclet in the folder
key/key.core/tacletProofs
or an arbitrary subfolder. It is recommended to use the name of the keyfile in which the taclet has been defined as name of the subdirectory. The name of the proof file has to match the pattern:Taclet_$TACLETNAME.proof
.
For example, the proof of the taclet bsum_empty can be found in
key/key.core/tacletProofs/bsum/Taclet_bsum_empty.proof
.
The JUnit test case will fail
 if there is a proof for a taclet that is not marked
\lemma
. (Just add the \lemma anntoation to the taclet) or  if there is no proof for a taclet which is annotated lemma.
 if there is a proof, but that cannot be replayed in KeY.
See class de.uka.ilkd.key.proof.proverules.ProveRulesTest
for implementation
details.
In order to run taclet proofs manually, execute the gradle task testProveRules
in component key.core
.