Loop invariant definitions can not be applied after creation of 2-Dimensional arrays

[wadoon]

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

---

• Mantis: MT-1294
• Submitted on: 2013-04-30 by (at)greiner
• Updated: 2013-05-14

Description

After creating a 2-dimensional array, a specified and correct loop invariant definition can not be applied.

Steps to reproduce

Load the attached file.
Load contract for testMeth()
Run Makro finish Symbolic Execution
Try to apply loop invariant

Restart
remove the line "someInt = new int[5][5];"
Do as above
-> The loop contract is applied automatically 

Files

Test.java:

public class Test {

    private int[][] someInt;

    /*@ public normal_behaviour
      @ ensures true;
     */
    public void testMeth() {
        someInt = new int[5][5];

        /*@ loop_invariant
          @ (\forall int j; 0 <= j && j < i; someInt[0][j] == 5);
          @ assignable someInt[*];
          @ decreases someInt.length - i;
         */
        for (int i = 0; i < someInt.length; i++) {
            someInt[0][i] = 5;
        }
    }

}

Notes

(at)grahl at 2013-04-30

This looks the same issue as #1288 which Wojtek posted last week.

During symbolic execution, your program gets rewritten to "while (i<dim0) {...}" and your invariant does not know of dim0.

Associated Bugs

• Relates to MT-1288 with

History

• (at)greiner -- (NEW_BUG) 2013-04-30

• (at)greiner -- (FILE_ADDED) 2013-04-30

• (at)grahl -- (BUGNOTE_ADDED) 2013-04-30

• (at)grahl -- (BUG_ADD_RELATIONSHIP) 2013-05-14

Attributes

• Category: Calculus
• Status: NEW
• Severity: MINOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: KeY 2.0
• Build:
• Tags []
• Labels: ~Calculus ~Bug ~NORMAL
• Version: 2.2

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:43:43.315Z
• updated_at: 2017-05-29T02:43:43.315Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0

[mattulbrich]

Astonishingly, the very same problem is alive after a decade:

class A {
    //@ ensures true;
    void m() {
        int[][] a = new int[1][1];
    }
}

cannot be verified since the 2-dimensional array construction introduces a loop without invariant ... We should introduce a rule that applies a contract to new T[n][m]...[k] creations.