improve 0.0.3 → 0.0.4

raw patch · 2 files changed

+134/−8 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/ImProve/Examples.hs +128/−5
• improve.cabal +6/−3

@@ -1,10 +1,16 @@ -- | ImProve examples. module Language.ImProve.Examples-  ( gcd'-  , gcdMain-  , buildGCD+  ( buildGCD   , counter   , verifyCounter+  , arbiterSpec+  , arbiter+  , arbiter1+  , arbiter2+  , arbiter3+  , verifyArbiters+  , buildArbiters+  , runAll   ) where  import Language.ImProve@@ -70,9 +76,126 @@   assert "LessThan10"            $ ref counter <.  10    -- Implementation.-  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (incr counter)+  ifelse "ResetCounter" (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1) --- Verify the 'counter' example.+  -- Alternatives to try.+  --ifelse "ResetCounter" (ref counter >=. 9) (counter <== 0) (counter <== ref counter + 1)+  --ifelse "ResetCounter" (ref counter >=. 9 ||. ref counter <. 0)  (counter <== 0) (counter <== ref counter + 1)++-- | Verify the 'counter' example. verifyCounter :: IO () verifyCounter = verify "yices" 20 counter++++-- | Arbiter specification.+arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()+arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do++  -- Mutual exclusion.  At most, only one requester granted at a time.+  assert "OneHot" $      grantA &&. not_ grantB &&. not_ grantC+                ||. not_ grantA &&.      grantB &&. not_ grantC+                ||. not_ grantA &&. not_ grantB &&.      grantC+                ||. not_ grantA &&. not_ grantB &&. not_ grantC+  +  -- No grants without requests.+  assert "NotRequestedA" $ imply (not_ requestA) (not_ grantA)+  assert "NotRequestedB" $ imply (not_ requestB) (not_ grantB)+  assert "NotRequestedC" $ imply (not_ requestC) (not_ grantC)++  -- Grants to single requests.+  assert "OnlyRequestA" $ imply (     requestA &&. not_ requestB &&. not_ requestC) grantA+  assert "OnlyRequestB" $ imply (not_ requestA &&.      requestB &&. not_ requestC) grantB+  assert "OnlyRequestC" $ imply (not_ requestA &&. not_ requestB &&.      requestC) grantC++  -- Priority.+  assert "Highest" $ imply requestA grantA+  assert "Medium"  $ imply (not_ requestA &&. requestB) grantB+  assert "Lowest"  $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC++-- | An arbiter implementation.+arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)+arbiter1 (requestA, requestB, requestC) = do+  let grantA = requestA+      grantB = requestB+      grantC = requestC+  return (grantA, grantB, grantC)++-- | An another arbiter implementation.+arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)+arbiter2 (requestA, requestB, requestC) = do+  grantA <- bool "grantA" False+  grantB <- bool "grantB" False+  grantC <- bool "grantC" False++  if_ "GrantA" (requestA)                                     (grantA <== true)+  if_ "GrantB" (not_ requestA &&. requestB)                   (grantB <== true)+  if_ "GrantC" (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)++  return (ref grantA, ref grantB, ref grantC)++-- | Yet another arbiter implementation.+arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)+arbiter3 (requestA, requestB, requestC) = do+  let grantA = requestA+      grantB = not_ requestA &&. requestB+      grantC = not_ requestA &&. not_ requestB &&. requestC+  return (grantA, grantB, grantC)++-- | Binding an arbiter implemenation to the arbiter specification.+arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()+arbiter name implementation = scope name $ do+  -- Create input variables.+  requestA <- input bool "requestA"+  requestB <- input bool "requestB"+  requestC <- input bool "requestC"+  let requests = (requestA, requestB, requestC)++  -- Instantiate implementation.+  grants@(grantA, grantB, grantC) <- scope "impl" $ implementation requests++  -- Bind specification.+  arbiterSpec requests grants++  -- Create output variables.+  bool' "grantA" grantA+  bool' "grantB" grantB+  bool' "grantC" grantC+  return ()++-- | Verify the different arbiter implementations.+verifyArbiters :: IO ()+verifyArbiters = do+  putStrLn "\nVerifying arbiter1 ..."+  verify "yices" 20 $ arbiter "arbiter1" arbiter1++  putStrLn "\nVerifying arbiter2 ..."+  verify "yices" 20 $ arbiter "arbiter2" arbiter2++  putStrLn "\nVerifying arbiter2 ..."+  verify "yices" 20 $ arbiter "arbiter3" arbiter3++-- | Build the different arbiter implementations.+buildArbiters :: IO ()+buildArbiters = do+  putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."+  code "arbiter1" $ arbiter "arbiter1" arbiter1++  putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."+  code "arbiter2" $ arbiter "arbiter2" arbiter2++  putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."+  code "arbiter3" $ arbiter "arbiter3" arbiter3++-- | Run all examples.+runAll :: IO ()+runAll = do+  putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."+  buildGCD+  putStrLn "\nVerifying counter ..."+  verifyCounter+  putStrLn "\nVerifying arbiters ..."+  verifyArbiters+  putStrLn "\nBuilding arbiters ..."+  buildArbiters 

@@ -1,12 +1,15 @@ name:    improve-version: 0.0.3+version: 0.0.4  category: Language -synopsis: An imperative, verifiable programming language for embedded applications.+synopsis: An imperative, verifiable programming language for high assurance applications.  description:-    TODO+  ImProve is an imperative DSL intended for high assurance, embedded applications.+  ImProve uses infinite state, unbounded model checking to verify programs adhere+  to specifications, which are written in the form of assertion statements.+  Yices (required) is the backend SMT solver.  author:     Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>