Explicitly declared state modification

Question

In my code I have to write numerous ensures like this to satisfy contract checking on caller's site:

public void Method()
{
  Contract.Ensures(this.PropertyA == Contract.OldValue(this.PropertyA));
  Contract.Ensures(this.PropertyB == Contract.OldValue(this.PropertyB));
  Contract.Ensures(this.PropertyC == Contract.OldValue(this.PropertyC));
  Contract.Ensures(this.PropertyD == Contract.OldValue(this.PropertyD));
  Contract.Ensures(this.PropertyE == Contract.OldValue(this.PropertyE) + 1);

  this.propertyE = this.propertyE + 1;
}

Often there are many methods that modify only a couple of fields. The other state remains unchanged but the caller thinks that everything may change unless we write a number of ensures about other properties.

It would be convenient if all properties and fields were considered as not modified by the method unless the modification is explicitly declared by Contract.Ensures. And the static checker should generate a warning if the method attempts to make a non-declared state modifcation:

public void Method()
{
  Contract.Ensures(this.PropertyE == Contract.OldValue(this.PropertyE) + 1);

  this.propertyD = this.propertyD + 1; // --> generate a warning here
  this.propertyE = this.propertyE + 1;
}

Answer 1

Hi Alexey,

this is an excellent observation. As you can tell, we have been keeping pretty quiet about how the checker reasons about state modifications. We use heuristics to avoid having the programer state explicit Modifies clauses in order not to overwhelm him/her with a concept that may be difficult to deal with and that isn't easily checked at runtime.

Finding a good heuristic about what properties/pure observations are modified by a call and which ones are not is tricky. Mentioning a property in a post condition could be one way, but is not always unambiguous.

E.g.,

  void Update() {
      Contract.Ensures(this.P == this.Q );
      ...
  }

In the above case, do we assume both P and Q are modifed, or only one of them, and which one?

We probably will have to go to a more explicit form that overrides the default assumptions, such as:

public void Update()
{
  Contract.MayModify(this.P);
  ...
}

with the intent that when a method has one or more MayModify clauses, only these explicitly declared ones are possibly modified and anything not mentioned is not modified.

---

Cheers, -MaF (Manuel Fahndrich)

Answer 2

Hi Manuel.

In your example:

void Update() {
      Contract.Ensures(this.P == this.Q );
      ...
  }

Neither P nor Q may change unless we explicitly declare that P and Q may be modified. So if we don't have Requires(this.P == this.Q) then the Ensures cannot be proven. If we declare MayModify(this.P) then the Ensures cannot be proven unless we add MayModify(this.Q).

Checking for at least one Contract.MayModify clause would be ok, and for zero case we can just use Pure attribute.

In some post you have mentioned that you have a method purity checker internally. Maybe it can be used for proving that the object state is not modified except declared modifications. If a method declares Contract.MayModify(this.P) the purity checker can work as in absolutely pure case except that it should not prove the this.P is not modified.

Would be nice to have such feature. At least optionally. We are not required to use Pure attribute but is helps so much.