Ghosts for Model Checking

ATS programming language allows programmers to write code constructing proofs along side with operational code which does the actual computation. The code for proof is seen only by the type checker of ATS and is erased completely before the compiler of ATS starts generating executable programs. We extends such concept by allowing programmers to write code related to model checking. Such code can be seen by the type checker of ATS, which facilitate the type checking process, and will be erased (just like proof code) before the compiler of ATS starts generating executable programs. We call such code ghost code. Ghost code comes in various forms: Ghost function, Ghost value, Ghost type, and etc. We will talk about them in details when meeting related exampels.

Both operational code and ghost code have semantics to model checker we build. On the other hand, proof code is neglected by the model checker. The simplest but maybe the most stimulating example of ghost code is mc_assert as shown below.

  fun foo (): void = let
    prval () = mc_assert (false)
  in
  end

  val () = foo ()

The executable generated by ATS compiler from the code above simply does nothing since the only content of the function foo is a ghost function mc_assert, which is only meaningful to our model checker. Intuitively, we can view mc_assert as assertions normally used by programmers for runtime checking, but this time it’s used at the stage of model checking.

Feel free to try the example using our online model checker. To use the model checker, we need to appending the following code to indicate that we want to verify that mc_assert succeeds.

  %{$
  #assert main |= G sys_assertion;
  %}

The complete code (with some routine code for header files) for the example can be found here demo_01_mc_assert.dats

With mc_assert, we can use model checking as a test facility as shown in the following example.

  typedef Int = [x:int] int x

  fun sum {x:nat} (x: int x): Int = x * (x + 1) / 2

  fun sum2 {x:nat}.<x>.(x: int x):<fun> Int =
    if x > 0 then x + sum2 (x - 1)
    else 0

  val n = 3
  val ret = sum (n)
  prval mc_ret = sum2 (n)
  prval () = mc_assert (ret = mc_ret)

In the example above, we have two versions of the summation function. We use model checking to verify that they generate the same output. mc_ret is a ghost value (declared via the keyword prval), and accordingly the executable generated by ATS compiler doesn’t contain the invocation of sum2. However sum2 itself is not a ghost function, and it can be used at runtime if programmers choose to. (Just for technical detail, currently only pure functions in ATS can be used to calculate ghost values. That’s why the type of sum2 is a little bit verbose, since we prove that sum2 always terminates.)

One thing worth mentioning is the type of mc_assert as shown below:

prfun mc_assert {b: bool} (x: bool b):<fun> [b == true] void

The type of the argument of mc_assert depends on a boolean value b in the statics of ATS. mc_assert assures the type system that b is true and as such the type checking of the whole program may be established successfully. Also the validity of such assertion is checking during the process of model checking.