I've been encountering this error with my "swap" method during verification: "Target array of assignment is not allowed to be committed." However, even after reading about this error in the tutorial pdf I'm still not quite sure I
understand how to avoid it. Here is the small amount of code I have so far (the swap method is pretty much identical to the one shown inside the tutorial with the exception that "int a" is not one of the parameters. Instead I wanted to modify my
class's main array (this is at the root of the problem I think).
Anyways, my class currently looks like the following:
int! Data = new int;
invariant Size <= Data.Length;
private void Swap(int i, int j)
requires 0 <= i && i < Data.Length;
requires 0 <= j && j < Data.Length;
modifies Data[i], Data[j];
ensures Data[i] == old(Data[j]) && Data[j] == old(Data[i]);
int temp = Data[i];
Data[i] = Data[j]; <-- this gets underlined in green. I must be doing something fundamentally wrong here...
Data[j] = temp;
Thanks, I appreciate all the help I've received so far.