"Target array ... not allowed to be committed"

Aug 5, 2011 at 12:26 AM

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. 

Developer
Aug 5, 2011 at 9:54 AM

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

Aug 6, 2011 at 6:34 AM

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. 

Developer
Aug 8, 2011 at 10:26 AM

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