Data.SBV.Plugin.Examples.MicroController

Parameters

safetyDistance

maxTimeSince

The specification

checkSpec

A bad implementation

computeLastBad

checkBad

A correct implementation

computeLastGood

checkGood

Exercise for the reader