diff --git a/Language/ImProve.hs b/Language/ImProve.hs --- a/Language/ImProve.hs +++ b/Language/ImProve.hs @@ -52,7 +52,7 @@ /Statement Labels/ @ -hello: { 'label' \"hello\" $ do +hello: { \"hello\" '-:' do a(); a b(); b } @@ -146,7 +146,7 @@ , or_ , any_ , all_ - , imply + , (-->) -- ** Equality and Comparison , (==.) , (/=.) @@ -171,9 +171,9 @@ , linear -- * Statements , Stmt - -- ** Hierarchical Scope and Annotations - , scope - , label + -- ** Statement Labeling and Hierarchical Scope + , (-:) + , (!) -- ** Variable Declarations , bool , bool' @@ -209,7 +209,8 @@ infix 4 ==., /=., <., <=., >., >=. infixl 3 &&. infixl 2 ||. -infixr 1 <== +infixr 1 --> +infixr 0 <==, -:, ! -- | True term. true :: E Bool @@ -252,8 +253,8 @@ any_ f a = or_ $ map f a -- Logical implication (if a then b). -imply :: E Bool -> E Bool -> E Bool -imply a b = not_ a ||. b +(-->) :: E Bool -> E Bool -> E Bool +a --> b = not_ a ||. b -- | Equal. (==.) :: AllE a => E a -> E a -> E Bool @@ -338,28 +339,30 @@ mux :: AllE a => E Bool -> E a -> E a -> E a mux = Mux --- | Creates a hierarchical scope for variable names. -scope :: Name -> Stmt a -> Stmt a -scope name stmt = do +-- | Labels a statement. +-- Labels are used in counter examples to trace the program execution. +-- And assertion names, and hence counter example trace file names, are produce from labels. +(-:) :: Name -> Stmt a -> Stmt a +name -: stmt = do (path0, stmt0) <- get - put (path0 ++ [name], stmt0) + put (path0, Null) a <- stmt (_, stmt1) <- get - put (path0, stmt1) + put (path0, stmt0) + statement $ Label name stmt1 return a --- | Labels a statement. Labels are used in counter examples to trace the program execution. --- And assertion names, and hence counter example file names, are produce from labels. -label :: Name -> Stmt a -> Stmt a -label name stmt = do +-- | Creates a new hierarcical scope for variable names. +(!) :: Name -> Stmt a -> Stmt a +name ! stmt = do (path0, stmt0) <- get - put (path0, Null) + put (path0 ++ [name], stmt0) a <- stmt (_, stmt1) <- get - put (path0, stmt0) - statement $ Label name stmt1 + put (path0, stmt1) return a - + + get :: Stmt ([Name], Statement) get = Stmt $ \ a -> (a, a) @@ -452,8 +455,10 @@ assert = statement . Assert -- | Declare an assumption condition is true. +-- Assumptions expressions must contain variables directly or indirectly related +-- to the assertion under verification, otherwise they will be ignored. assume :: E Bool -> Stmt () -assume = statement . Assume +assume a = statement $ Assume a -- | Conditional if-else. ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt () diff --git a/Language/ImProve/Examples.hs b/Language/ImProve/Examples.hs --- a/Language/ImProve/Examples.hs +++ b/Language/ImProve/Examples.hs @@ -25,18 +25,18 @@ b1 <- int "b1" 0 -- Working copy of 'b'. -- A new input to process. - label "startNew" $ if_ (a /=. ref a0 ||. b /=. ref b0) $ do + "startNew" -: if_ (a /=. ref a0 ||. b /=. ref b0) $ do a0 <== a b0 <== b a1 <== a b1 <== b -- Reduce a1. - label "reduceA" $ if_ (ref a1 >. ref b1) $ do + "reduceA" -: if_ (ref a1 >. ref b1) $ do a1 <== ref a1 - ref b1 -- Reduce b1. - label "reduceB" $ if_ (ref b1 >. ref a1) $ do + "reduceB" -: if_ (ref b1 >. ref a1) $ do b1 <== ref b1 - ref a1 -- Done if a1 == b1. @@ -52,7 +52,7 @@ result <- int "result" 0 -- Result of GCD. -- Call gcd' in its own scope. (Scopes prevent variable name collisions.) - (done', result') <- scope "gcd" $ gcd' a b + (done', result') <- "gcd" ! gcd' a b -- Bind the results to the output variables. done <== done' @@ -72,8 +72,8 @@ counter <- int "counter" 0 -- Specification. - label "GreaterThanOrEqualTo0" $ assert $ ref counter >=. 0 - label "LessThan10" $ assert $ ref counter <. 10 + "GreaterThanOrEqualTo0" -: assert $ ref counter >=. 0 + "LessThan10" -: assert $ ref counter <. 10 -- Implementation. ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1) @@ -93,25 +93,25 @@ arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do -- Mutual exclusion. At most, only one requester granted at a time. - label "OneHot" $ assert $ grantA &&. not_ grantB &&. not_ grantC - ||. not_ grantA &&. grantB &&. not_ grantC - ||. not_ grantA &&. not_ grantB &&. grantC - ||. not_ grantA &&. not_ grantB &&. not_ grantC + "OneHot" -: assert $ 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. - label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA) - label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB) - label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC) + "NotRequestedA" -: assert $ not_ requestA --> not_ grantA + "NotRequestedB" -: assert $ not_ requestB --> not_ grantB + "NotRequestedC" -: assert $ not_ requestC --> not_ grantC -- Grants to single requests. - label "OnlyRequestA" $ assert $ imply ( requestA &&. not_ requestB &&. not_ requestC) grantA - label "OnlyRequestB" $ assert $ imply (not_ requestA &&. requestB &&. not_ requestC) grantB - label "OnlyRequestC" $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC + "OnlyRequestA" -: assert $ ( requestA &&. not_ requestB &&. not_ requestC) --> grantA + "OnlyRequestB" -: assert $ (not_ requestA &&. requestB &&. not_ requestC) --> grantB + "OnlyRequestC" -: assert $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC -- Priority. - label "Highest" $ assert $ imply requestA grantA - label "Medium" $ assert $ imply (not_ requestA &&. requestB) grantB - label "Lowest" $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC + "Highest" -: assert $ requestA --> grantA + "Medium" -: assert $ (not_ requestA &&. requestB) --> grantB + "Lowest" -: assert $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC -- | An arbiter implementation. arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool) @@ -128,9 +128,9 @@ grantB <- bool "grantB" False grantC <- bool "grantC" False - label "GrantA" $ if_ (requestA) (grantA <== true) - label "GrantB" $ if_ (not_ requestA &&. requestB) (grantB <== true) - label "GrantC" $ if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true) + "GrantA" -: if_ (requestA) (grantA <== true) + "GrantB" -: if_ (not_ requestA &&. requestB) (grantB <== true) + "GrantC" -: if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true) return (ref grantA, ref grantB, ref grantC) @@ -144,7 +144,7 @@ -- | 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 +arbiter name implementation = name -: do -- Create input variables. requestA <- input bool "requestA" requestB <- input bool "requestB" @@ -152,7 +152,7 @@ let requests = (requestA, requestB, requestC) -- Instantiate implementation. - grants@(grantA, grantB, grantC) <- scope "impl" $ implementation requests + grants@(grantA, grantB, grantC) <- "impl" -: implementation requests -- Bind specification. arbiterSpec requests grants diff --git a/Language/ImProve/Verify.hs b/Language/ImProve/Verify.hs --- a/Language/ImProve/Verify.hs +++ b/Language/ImProve/Verify.hs @@ -107,7 +107,7 @@ (Null, a) -> a (a, Null) -> a (a, b) -> Sequence a b - Assert a -> if any (flip elem vars) (exprVars a) then Assert a else Null + Assert a -> Assert a Assume a -> if any (flip elem vars) (exprVars a) then Assume a else Null Label name a -> case trim a of Null -> Null @@ -404,7 +404,7 @@ Just "true" -> "ifelse true:\n" ++ indent (concatMap f onTrue) Just "false" -> "ifelse false:\n" ++ indent (concatMap f onFalse) _ -> "" - Label' name traces -> name ++ ":\n" ++ indent (concatMap f traces) + Label' name traces -> name ++ " -:\n" ++ indent (concatMap f traces) indent :: String -> String indent = unlines . map (" " ++) . lines diff --git a/improve.cabal b/improve.cabal --- a/improve.cabal +++ b/improve.cabal @@ -1,5 +1,5 @@ name: improve -version: 0.0.8 +version: 0.0.9 category: Language