Loop scope rule uses variables outside the name space

[mattulbrich]

Description

The loop scope invariant rule introduces variables (usually called h and a that are not within the namespace of the current goal).

In some cases this may even lead to two variables of the same name, but with different types on the sequent.

Reproducible

always

Steps to reproduce

1. Load the sum and max example from the example browser..
2. In the proof search strategy set "Loop treatment" to "none".
3. Set "Arithmetic treatment" to "basic".
4. Push the green arrow button
5. On the one open goal apply the rule "loopScopeInvDia".
6. Navigate to the 2nd open goal

Two things are bad now:

• There is an update h := heap, but you cannot perform a cut h = h because h is an unknown name.
• There is an update a := _a.length - k assigning an int value to a. However, a is the parameter of the method and an int[] variable.

The rule fails to register the assigned variables in the goal context (in other rules that usually happens by declaring the new names within modalities).

Additional information

Discovered, since this is a deal breaker for research on a scripting engine.

---

• Commit: 470b0d6

[mattulbrich]

Another related problem with the loop scope rule is that it introduces conflicting location variables with the same name.

1. Load Binary Search and press autoplay.
2. Have a look at node 125 (invariant preserved and used)

It contains two variables called a. One of type any (introduced to store the variant) and one of type int[] which is the array to be searched.

Here a screenshot indicating the problem:

on 0ac6d7f