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:

class Priority_Queue{

int[]! Data = new int[10];

int Size;

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. 

Hi,

this error tells you that you try to modify a committed object. However, if you want to modify some object it generally needs to be consistent. There are multiple ways of achieving this in your example:

1) Require the object 'Data' to be consistent.

2) Mark the 'Data' field as [Peer]. Since the 'this' object (and method parameters; this is why the example in the tutorial works) is consistent implicitly, its peers are also consistent.

3) Mark the 'Data' field as [Rep] and expose the 'this' object before you modify the object 'Data'. This is probably what you would want in your case.

The following code should verify:

class Priority_Queue {
  // Option 2:
  // [Peer]

  // Option 3:
  [Rep]
  int[]! Data = new int[10];
  int Size;
  invariant Size <= Data.Length;

  private void Swap(int i, int j)
    requires 0 <= i && i < Data.Length;
    requires 0 <= j && j < Data.Length;
    // Option 1:
    // requires Data.IsConsistent;
    modifies Data[i], Data[j];
    ensures Data[i] == old(Data[j]) && Data[j] == old(Data[i]);
  {
      int temp = Data[i];

      // Option 3:
      expose (this) {
          Data[i] = Data[j];

          Data[j] = temp;
      }
  }

}

Best regards,

Valentin

Thanks for the help. This may seem like a sort of weird question to ask, but after getting this to check without error, is there any way I can print out a nice, clean, ordered list of verification conditions that SscBoogie generated for this Swap method? I've been looking through all the commands that "SscBoogie /help" brings and am unsure which, command, if any, would allow me to see the final string of implications and substitutions that were made when the code was backed over. 

Hi,

I know of three interesting options that allow you to see what goes on behind the scenes:

- sscboogie /print:<filename>.bpl <filename>.dll (to get the Boogie program that is used to produce the verification conditions; this is quite readable and useful)

- boogie /traceverify <filename>.bpl (to see how the Boogie program is desugared before the prover is invoked)

- boogie <filename>.bpl /proverLog:<output file> (to get the verification conditions that are sent to the prover; this is not very readable)

Best regards,

Valentin