----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Plugin.Examples.MicroController -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- -- A transcription of Anthony Cowley's MicroController example, using -- the SBV plugin. For the original, see: <http://acowley.github.io/NYHUG/FunctionalRoboticist.pdf> -- ----------------------------------------------------------------------------- {-# LANGUAGE CPP #-} #ifndef HADDOCK {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} #endif {-# OPTIONS_GHC -Wall -Werror #-} module Data.SBV.Plugin.Examples.MicroController where import Data.SBV.Plugin ----------------------------------------------------------------------------- -- * Parameters ----------------------------------------------------------------------------- -- | The range detector must output if the range is larger than this amount. safetyDistance :: Int safetyDistance :: Int safetyDistance = Int 200 -- | The range detector must have sent an output before this many cycles have past. maxTimeSince :: Int maxTimeSince :: Int maxTimeSince = Int 10 ----------------------------------------------------------------------------- -- * The specification ----------------------------------------------------------------------------- -- | 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 checkSpec :: (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool checkSpec :: (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool checkSpec Int -> Bool -> Int -> Int calculate Int r Bool m Int t = Bool minRate Bool -> Bool -> Bool && Bool minRange Bool -> Bool -> Bool && Bool manualOverride where sinceLast :: Int sinceLast = Int -> Bool -> Int -> Int calculate Int r Bool m Int t -- Never exceed the max-time allowed minRate :: Bool minRate = Int sinceLast Int -> Int -> Bool forall a. Ord a => a -> a -> Bool < Int maxTimeSince -- If the range is exceeded, always send a signal minRange :: Bool minRange = Int r Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int safetyDistance Bool -> Bool -> Bool || Int sinceLast Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int 0 -- Manual override, always signals manualOverride :: Bool manualOverride = Bool -> Bool not Bool m Bool -> Bool -> Bool || Int sinceLast Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int 0 ----------------------------------------------------------------------------- -- * A bad implementation ----------------------------------------------------------------------------- -- | A "bad" implementation, see if you can spot the problem with it, before looking -- at the failed theorem below! computeLastBad :: Int -> Bool -> Int -> Int computeLastBad :: Int -> Bool -> Int -> Int computeLastBad Int range Bool manual Int timeSince | Int range Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int safetyDistance = Int 0 | Bool manual = Int 0 | Int timeSince Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int maxTimeSince Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1 = Int 0 | Bool True = Int timeSince Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1 -- | 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! #ifndef HADDOCK {-# ANN checkBad theorem {options = [IgnoreFailure]} #-} #endif checkBad :: Int -> Bool -> Int -> Bool checkBad :: Int -> Bool -> Int -> Bool checkBad Int range Bool manual Int timeSince = (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool checkSpec Int -> Bool -> Int -> Int computeLastBad Int range Bool manual Int timeSince ----------------------------------------------------------------------------- -- * A correct implementation ----------------------------------------------------------------------------- -- | A "good" implementation, properly handling the off-by-one error of the original. computeLastGood :: Int -> Bool -> Int -> Int computeLastGood :: Int -> Bool -> Int -> Int computeLastGood Int range Bool manual Int timeSince | Int range Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int safetyDistance = Int 0 | Bool manual = Int 0 | Int timeSince Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int maxTimeSince Int -> Int -> Int forall a. Num a => a -> a -> a - Int 2 = Int 0 | Bool True = Int timeSince Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1 -- | 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. -- @ checkGood :: Proved (Int -> Bool -> Int -> Bool) checkGood :: Int -> Bool -> Int -> Bool checkGood Int range Bool manual Int timeSince = (Int -> Bool -> Int -> Int) -> Int -> Bool -> Int -> Bool checkSpec Int -> Bool -> Int -> Int computeLastGood Int range Bool manual Int timeSince ----------------------------------------------------------------------------- -- * Exercise for the reader -- $exercise ----------------------------------------------------------------------------- {- $exercise 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. -} {-# ANN module ("HLint: ignore Eta reduce" :: String) #-}