How to prove properties of finite state machines with cccheck

  • Article

In the previous post we saw how to use cccheck to prove that we did not forgot any case in a switch statement. Some friend in Microsoft product groups asked if we can do more. For instance, if we can prove properties about a finite state machine using the CodeContracts static checker. The answer is yes, and I will illustrate it with our favorite example: cooking pasta!

First, we define a function that tell us if we can move from one state in the (extremely important) process of cooking pasta, to the next one (for theory lovers, we are defining the transition relation of a finite state machine).

enum CookPasta { BoilWater, AddSalt, AddPasta, Stir, Strain, Eat }

[Pure]
static public bool CanTransition(CookPasta from, CookPasta to)
{
 switch (from)
 {
  case CookPasta.BoilWater:
  return to == CookPasta.AddPasta || to == CookPasta.AddSalt;

  case CookPasta.AddPasta:
  return to == CookPasta.AddSalt || to == CookPasta.Stir;

  case CookPasta.AddSalt:
  return to == CookPasta.AddPasta;

  case CookPasta.Stir:
  return to == CookPasta.Strain;

  case CookPasta.Strain:
  return to == CookPasta.Eat;

  case CookPasta.Eat:
  return false;

  default:
   throw CodeContractsHelpers.ThrowIfReached("missing case");
 }
}

Now we'd love to prove some properties about our state machine. For instance that the first thing to do is to boil water or that once we eat all our pasta we are done. We can do it by defining two methods as below (again for the theory-loving people those acts as lemmas to be proven by the static analyzer).

Important. To repro the examples below, make sure that you have the "Infer ensures" on.

With the first method, BoilWaterIsIntitial, we ask the tool to prove that there is no state from which we can transition into BoilWater:

static public void BoilWaterIsInitial(CookPasta someState)
{
  var next = CanTransition(someState, CookPasta.BoilWater);
  Contract.Assert( !next, "there is no way to transition to boiling water");
}

Similarly, we can ask the tool to prove that there is successor for Eat.

static public void EatingIsFinal(CookPasta someOtherState)
{
  var next = CanTransition(CookPasta.Eat, someOtherState);
  Contract.Assert( !next, "Once you eat your pasta, nothing left to do");
}

Nevertheless, if we ask whether Strain is final, cccheck will tell that it is not:

static public void StrainIsFinal(CookPasta someOtherState)
{
  var next = CanTransition(CookPasta.Strain, someOtherState); 
  Contract.Assert( !next, "We cannot prove it, as it is false");
}

d:\tmp\Pasta\CookPasta.cs(58,9): warning : CodeContracts: assert unproven

What's the magic behind? There is no magic. The static analyzer will infer the inputs under which CanTransition returns true, and then it uses this information to prove (or disprove) the assertion. If you are curious to see what the inferred postcondition looks like, add "-infer methodensures" to the extra static checker options box in VS.