This project is read-only.

List Invariant

Dec 25, 2011 at 4: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

Dec 25, 2011 at 5: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