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)
0 Comments:
Post a Comment
Note: Only a member of this blog may post a comment.