Additional contract generated from the FM tutorial example

[WolframPfeifer]

Description

For the FM tutorial example's ArrayList::get method, a third proof obligation is shown:

This PO was not there in older KeY versions, and also is not provable (since the index precondition is missing).

Reproducible

always

Steps to reproduce

1. Load the example: File -> Load Example... -> FM 2024 Tutorial -> ArrayList and LinkedList

The proof management dialog shows the contract from the screenshot above, which is not provable.

[WolframPfeifer]

I don't understand where this contract comes from. At first I thought it is generated since the accessible clause is in between pre- and postcondition. However, why would the normal_behavior contract correctly have pre and post then? It seems that this is some kind of default contract that is not correctly filtered out (note that it does not have the normal_behavior).

[Drodt]

The error is in the JMLParser or TextualTranslator: It adds an empty spec case (apparently only with the public keyword) between

//@ public instance invariant \subset(\singleton(this.footprint), footprint);

and

//@ public accessible \inv: footprint;

in List.java. No idea yet why.

[Drodt]

It seems that the class-level accessible clause is parsed as part of a method contract and this empty contract is added.

[Drodt]

Removing public on accessible fixes things...

[Drodt]

We should fix this bug but for the release, I suppressed the new contract in 420c634

[WolframPfeifer]

Weird. Thanks for investigating and the workaround. I would keep this bug open, but change the milestone.