Cannot always prove that a method leaves a disjoint set of objects unmodified

[danmatichuk]

Given the following class:

  class MyClass{
    var i : int;
    method setInt(i : int)
      modifies {this}
      {this.i := i; }
}

I would expect the following to hold for any set of objs : set<object>:

myClass.setInt(i);
assert myClass !in objs ==> unchanged(objs);

However this is not able to be verified if objs is the result of an opaque function, either due to
having an undefined body or via the {:opaque} attribute.

function method someObjsUndefinedFunction() : set<object>
...
var objs := someObjsUndefinedFunction();
myClass.setInt(1);
assert myClass !in objs ==> unchanged(objs); // fails

Notably this works as expected if the field update occurs directly instead of through a method call.

function method someObjsUndefinedFunction() : set<object>
...
var objs := someObjsUndefinedFunction();
myClass.i := 1;
assert myClass !in objs ==> unchanged(objs); // succeeds

Adding the following (trivially-satisfied) postcondition to the method yields the expected result and successfully verifies in both cases:

    method setIntPlus(i : int)
      modifies {this}
      ensures forall objs : set<object> :: this !in objs ==> unchanged(objs) // always trivially true
      {this.i := i; }

[danmatichuk]

Full test file here:

class MyClass{
    var i : int;
    method setInt(i : int)
      modifies {this}
      {this.i := i; }

    method setIntPlus(i : int)
      modifies {this}
      ensures forall objs : set<object> :: this !in objs ==> unchanged(objs) // always trivially true
      {this.i := i; }

    protected static function method someObjsProtectedFunction() : set<object>
      { {} }
  }

method someObjsMethod() returns (ret : set<object>)

function method someObjsUndefinedFunction() : set<object>
function method someObjsDefinedFunction() : set<object>
  { {} }

function method {:opaque} someObjsOpaqueFunction() : set<object>
  { {} }

method test(obj : MyClass, objs : set<object>)
  modifies {obj}
{
  var objs2 := someObjsMethod();
  var objs3 := someObjsUndefinedFunction();
  var objs4 : set<object> := *;
  var objs5 := someObjsDefinedFunction();
  var objs6 := someObjsOpaqueFunction();
  var objs7 := MyClass.someObjsProtectedFunction();

  label L1:
  obj.i := 1;
  assert obj !in objs ==> unchanged@L1(objs);
  assert obj !in objs2 ==> unchanged@L1(objs2);
  assert obj !in objs3 ==> unchanged@L1(objs3);
  assert obj !in objs4 ==> unchanged@L1(objs4);
  assert obj !in objs5 ==> unchanged@L1(objs5);
  assert obj !in objs6 ==> unchanged@L1(objs6);
  assert obj !in objs7 ==> unchanged@L1(objs7);

  label L2:
  obj.setInt(1);
  assert obj !in objs ==> unchanged@L2(objs);
  assert obj !in objs2 ==> unchanged@L2(objs2);
  assert obj !in objs3 ==> unchanged@L2(objs3); // fails
  assert obj !in objs4 ==> unchanged@L2(objs4);
  assert obj !in objs5 ==> unchanged@L2(objs5);
  assert obj !in objs6 ==> unchanged@L2(objs6); // fails
  assert obj !in objs7 ==> unchanged@L2(objs7);

  label L3:
  obj.setIntPlus(1);
  assert obj !in objs ==> unchanged@L3(objs);
  assert obj !in objs2 ==> unchanged@L3(objs2);
  assert obj !in objs3 ==> unchanged@L3(objs3);
  assert obj !in objs4 ==> unchanged@L3(objs4);
  assert obj !in objs5 ==> unchanged@L3(objs5);
  assert obj !in objs6 ==> unchanged@L3(objs6);
  assert obj !in objs7 ==> unchanged@L3(objs7);
}