List Invariant

Wiki Link: [discussion:284112]
mbalves
Dec 25, 2011 at 3:03 AM

 

using System.Collections.Generic;
using Microsoft.Contracts;

namespace DrawingEngineGeneric {

public class DrawingEngine {// invariant does not hold here

  [Rep][ElementsRep] List<Step> steps = new List<Step>();

  invariant forall{int x in (0:steps.Count); steps[x].argX>0};

  public void AddStep(byte op, int argX, int argY) 
	ensures steps.Count == old(steps.Count)+1 ;
	requires argX>0;
  {
    expose (this) {
      Step s = new Step(op, argX, argY);
      Owner.AssignSame(s, steps);
      steps.Add(s);
    } // invariant does not hold here
  }

  public void Apply() {
    foreach (Step s in steps) {
      expose (this) { s.DoWork(); // invariant does not hold here
    }
	
    steps = new List<Step>();
  }
}

class Step {
  public byte op;
  public int argX, argY;

  invariant argX>0;

  public Step(byte op, int x, int y) 
	requires x>0;
  {
    this.op = op;  argX = x;  argY = y; 
  }
  public void DoWork() 
  {  argX=10; }
}

}






How can i write class invariant for objects of the type list accessing their element properties ? What am I doing wrong here ?





Best Regards and Merry Christmas
mbalves
Dec 25, 2011 at 4:16 PM

I ran the example with arrays and I added one new invariant.  The warnings are in the underlined lines.

using System;
using Microsoft.Contracts;

namespace DrawingEngineArray {

public class DrawingEngine {
  [Rep][ElementsRep] Step?[] steps = new Step?[100];
  invariant 1 <= steps.Length;
  int cnt;
  invariant 0 <= cnt && cnt <= steps.Length;
  invariant forall{int i in (0: cnt); steps[i] != null}; 
  invariant forall{int i in (0: cnt); steps[i].argX > 0};

// Possible null dereference
// Receiver might be null (of type 'DrawingEngineArray.Step')

  public void AddStep(byte op, int argX, int argY) 
	requires argX>0;
  {
    if (cnt == steps.Length) { EnlargeArray(); }
    
	expose (this) {
      Step s = new Step(op, argX, argY);
      steps[cnt] = s;
      cnt++;
    }
  }
  void EnlargeArray()
    ensures cnt < steps.Length;
  {
    expose (this) {
      Step?[] more = new Step?[2*steps.Length];
      Array.Copy(steps, 0, more, 0, steps.Length);
      steps = more;
    }
  }
  public void Apply() {
    for (int i = 0; i < cnt; i++) {
      Step? s = steps[i];
      assert s != null;
      expose (this) { s.DoWork(); } // Object invariant possibly does not hold: forall{int i in (0: cnt); steps[i].argX > 0}
    }
    cnt = 0;
  }
}

class Step {
  public byte op;
  public int argX, argY;
  
  invariant argX > 0;
  
  public Step(byte op, int x, int y) 
	requires x>0;
  {
    this.op = op;  argX = x;  argY = y;
	assert argX>0;
  }

  public void DoWork() { /* ... */ }
}

}


Anyone knows what I am doing wrong? 

Best Regards
Sign in to post message or set email notifications