Data.SBV.Plugin.Examples.MicroController

A transcription of Anthony Cowley's MicroController example, using the SBV plugin. For the original, see: http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf

Parameters

safetyDistance :: Int

The range detector must output if the range is larger than this amount.

maxTimeSince :: Int

The range detector must have sent an output before this many cycles have past.

The specification

checkSpec :: (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool

Given a last-signal-time calculator, named calculate, check that it satisfies the following three requirements: We must've just sent a signal if:

• minRate: The last-time we sent is strictly less than the maxTimeSince amount
• minRange: We must've just sent a signal if the range is beyond safetyDistance
• manualOverride: We must've just sent a signal if the manual-override is specified

A bad implementation

computeLastBad :: Int -> Bool -> Int -> Int

A "bad" implementation, see if you can spot the problem with it, before looking at the failed theorem below!

checkBad :: Int -> Bool -> Int -> Bool

Using SBV, prove that the computeLastBad is indeed a bad implementation. Here's the output we get from the plugin:

  [SBV] MicroController.hs:85:1-8 Proving "checkBad", using Z3.
  [Z3] Falsifiable. Counter-example:
    range     =   200 :: Int64
    manual    = False :: Bool
    timeSince =     9 :: Int64

We're being told that if the range is 200, and manual override is off, and time-since last is 9, then our "calculator" returns 10. But that violates the minRate requirement, since we never want to go maxTimeSince cycles without sending a signal!

A correct implementation

computeLastGood :: Int -> Bool -> Int -> Int

A "good" implementation, properly handling the off-by-one error of the original.

checkGood :: Proved (Int -> Bool -> Int -> Bool)

We now verify that the good variant is indeed good. We have:

  [SBV] MicroController.hs:108:1-9 Proving "checkGood", using Z3.
  [Z3] Q.E.D.

Exercise for the reader

It is easy to see that an implementation that always returns 0 (i.e., one that always sends a signal) will also pass our specification!

• First, use the plugin to prove that such an implementation is indeed accepted.
• Then, modify the spec so that we require the timeSince parameter to actually get incremented under the correct conditions.
• Show that your new spec outlaws the always 0 producing implementation.