[FIXED] How to check that only 1 element in a set has changed in a dafny ensures?

Issue

How can I check that only 1 element in a set has changed in a dafny ensures?

Example:

method myMethod(myParameter: int)
  requires myParameter >= 0
  modifies mySet
  ensures ONLY_ONE_ELEMENT_IN_THE_SET_HAS_CHANGED
{
  ...
}

Solution

If you mean that one element was removed and another was added, you need to provide them explicitly as (ghost) return variables and use the old keyword to reference the previous value of mySet

method myMethod(myParameter: int) returns (ghost removed: int, ghost added: int)
  requires myParameter >= 0
  modifies mySet
  ensures old(mySet) - {removed} + {added} == mySet
{
  ...
}

Answered By - Mikaël Mayer

Answer Checked By - Robin (PHPFixing Admin)