search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
48 stars 26 forks source link

Between variable renaming and update deletion something goes wrong #1418

Open wadoon opened 1 year ago

wadoon commented 1 year ago

This issue was created at git.key-project.org where the discussions are preserved.

Description

In the attached program there is a local variable me, which is assigned and later used in the loop invariant.

Sometimes, a proof run is produced where the update of me is deleted as effectless (rule simplifyUpdate2), so that the initial validity of the invariant cannot be shown. See attached proof script as proof (ha!). In other proof runs, the update is not deleted and the problem does not appear.

Apparently, it does not matter whether proofs are constructed fully automatically or with interaction. In both cases the problem appears intermittently. Sometimes the problematic rule can be applied and sometimes not.

Files

NameBug.java:

class NameBug {

    int f;

    /*@ requires f > 0;
        ensures f == 0;
        assignable f;
    */
    void m() {
        NameBug me = this;
        /*@ loop_invariant me.f >=0; 
            assignable this.f;
            decreases this.f;
        */
        while (f>0) f--;

    }

}

Notes

(at)most at 2013-10-23

Might it be the case that it appears when the proof is for a reloaded problem within the same KeY instance? I did enounter a problem with loop invariants and local variable naming in a situation like this, there is a bug somewhere...

(at)klebanov at 2013-10-24

It might, though I can neither confirm nor disprove this at the moment.

It seems one can increase the chances of the problem occurring by pruning and rebuilding the proof tree. After doing this, I can see the following:

Declaring the local variable me, renames it to me_2. The invariant (when applied) is now formulated in terms of me_1 (an undeclared symbol). Trying to reason about this me_1 (e.g., doing a cut) brings up an error message to this regard.

Thus, currently I tend to blame the mechanism that does renaming on the invariant when a local variable is declared.

(at)mulbrich at 2014-12-01

This is in fact a double-bug.

1) The update mechanism does not check for variable occurrences in loop specifications and block contracts; hence, the unexpected simplifyUpdate2.

2) If a declared variable is renamed (prune and reapply variable declaration rule), the old name remains in the loop (block) contract.

We encountered me_1 in the contract even if me_2 was the name of the currently used variable.

However, since loop (and block) contracts are mere guiding annotations, this bug does not the compromise correctness of KeY.

(Found with Richard)

History

Attributes

View in Mantis

Information:

FliegendeWurst commented 1 year ago

Same as #834