improve 0.1.6 → 0.2.0
raw patch · 7 files changed
+120/−414 lines, 7 files
Files
- Language/ImProve.hs +39/−23
- Language/ImProve/Code.hs +1/−1
- Language/ImProve/Core.hs +19/−4
- Language/ImProve/Examples.hs +0/−200
- Language/ImProve/Narrow.hs +0/−78
- Language/ImProve/Verify.hs +60/−105
- improve.cabal +1/−3
Language/ImProve.hs view
@@ -148,6 +148,7 @@ , AllE , NumE , Name+ , Theorem -- * Expressions -- ** Constants , true@@ -209,9 +210,9 @@ -- ** Incrementing and decrementing. , incr , decr- -- ** Assertions and Assumptions- , assert+ -- ** Assumptions and theorems. , assume+ , theorem -- * Verification , verify -- * Code Generation@@ -363,23 +364,23 @@ -- 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], Null)+ (id, path0, stmt0) <- get+ put (id, path0 ++ [name], Null) a <- stmt- (_, stmt1) <- get- put (path0, stmt0)+ (id, _, stmt1) <- get+ put (id, path0, stmt0) statement $ Label name stmt1 return a -get :: Stmt ([Name], Statement)+get :: Stmt (Int, [Name], Statement) get = Stmt $ \ a -> (a, a) -put :: ([Name], Statement) -> Stmt ()+put :: (Int, [Name], Statement) -> Stmt () put s = Stmt $ \ _ -> ((), s) getPath :: Stmt [Name] getPath = do- (path, _) <- get+ (_, path, _) <- get return path var :: AllE a => Name -> a -> Stmt (V a)@@ -437,7 +438,7 @@ decr a = a <== ref a - 1 -- | The Stmt monad holds variable declarations and statements.-data Stmt a = Stmt (([Name], Statement) -> (a, ([Name], Statement)))+data Stmt a = Stmt ((Int, [Name], Statement) -> (a, (Int, [Name], Statement))) instance Monad Stmt where return a = Stmt $ \ s -> (a, s)@@ -449,10 +450,10 @@ Stmt f4 = f2 a statement :: Statement -> Stmt ()-statement a = Stmt $ \ (path, statement) -> ((), (path, Sequence statement a))+statement a = Stmt $ \ (id, path, statement) -> ((), (id, path, Sequence statement a)) -evalStmt :: [Name] -> Stmt () -> ([Name], Statement)-evalStmt path (Stmt f) = snd $ f (path, Null)+evalStmt :: Int -> [Name] -> Stmt () -> (Int, [Name], Statement)+evalStmt id path (Stmt f) = snd $ f (id, path, Null) class Assign a where (<==) :: V a -> E a -> Stmt ()@@ -460,22 +461,33 @@ instance Assign Int where a <== b = statement $ Assign a b instance Assign Float where a <== b = statement $ Assign a b --- | Assert that a condition is true.-assert :: E Bool -> Stmt ()-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 a = statement $ Assume a +-- | Theorem to be proven or used as lemmas to assist proofs of other theorems.+data Theorem = Theorem' Int++-- | Defines a new theorem.+--+-- > theorem name k lemmas proposition+theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem+theorem name k lemmas proposition+ | k < 1 = error $ "k-induction search depth must be > 0: " ++ name ++ " k = " ++ show k+ | otherwise = do+ (id, path, stmt) <- get+ put (id + 1, path, Sequence stmt $ Label name $ Theorem id k [ i | Theorem' i <- lemmas ] proposition)+ return $ Theorem' id+ -- | Conditional if-else. ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt () ifelse cond onTrue onFalse = do- path <- getPath- let (_, stmt1) = evalStmt path onTrue- (_, stmt2) = evalStmt path onFalse+ (id0, path, stmt) <- get+ let (id1, _, stmt1) = evalStmt id0 path onTrue+ (id2, _, stmt2) = evalStmt id1 path onFalse+ put (id2, path, stmt) statement $ Branch cond stmt1 stmt2 -- | Conditional if without the else.@@ -498,10 +510,14 @@ -- | Verify a program. -- -- > verify pathToYices maxK program-verify :: FilePath -> Int -> Stmt () -> IO ()-verify yices maxK program = V.verify yices maxK $ snd $ evalStmt [] program+verify :: FilePath -> Stmt () -> IO ()+verify yices program = V.verify yices stmt+ where+ (_, _, stmt) = evalStmt 0 [] program -- | Generate C code. code :: Name -> Stmt () -> IO ()-code name program = C.code name $ snd $ evalStmt [] program+code name program = C.code name stmt+ where+ (_, _, stmt) = evalStmt 0 [] program
Language/ImProve/Code.hs view
@@ -34,7 +34,7 @@ Branch a b Null -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\n" Branch a b c -> "if (" ++ codeExpr a ++ ") {\n" ++ indent (codeStmt name path b) ++ "}\nelse {\n" ++ indent (codeStmt name path c) ++ "}\n" Sequence a b -> codeStmt name path a ++ codeStmt name path b- Assert a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n"+ Theorem _ _ _ a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n" Assume a -> "assert((" ++ show (intercalate "." path) ++ ", " ++ codeExpr a ++ "));\n" Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a) Null -> ""
Language/ImProve/Core.hs view
@@ -4,6 +4,7 @@ , UV (..) , Name , Path+ , UID , PathName (..) , AllE (..) , NumE@@ -13,6 +14,7 @@ , varInfo , stmtVars , exprVars+ , theorems ) where import Data.List@@ -22,6 +24,8 @@ type Path = [Name] +type UID = Int+ -- | A mutable variable. data V a = V Bool [Name] a deriving (Eq, Ord) @@ -101,7 +105,7 @@ Assign :: AllE a => V a -> E a -> Statement Branch :: E Bool -> Statement -> Statement -> Statement Sequence :: Statement -> Statement -> Statement- Assert :: E Bool -> Statement+ Theorem :: Int -> Int -> [Int] -> E Bool -> Statement -- ^ Theorem id depth lemmas expr Assume :: E Bool -> Statement Label :: Name -> Statement -> Statement Null :: Statement@@ -122,18 +126,18 @@ UVInt a -> varInfo a UVFloat a -> varInfo a --- Variables in a program.+-- | Variables in a program. stmtVars :: Statement -> [UV] stmtVars a = case a of Assign a b -> nub $ untype a : exprVars b Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c Sequence a b -> nub $ stmtVars a ++ stmtVars b- Assert a -> exprVars a+ Theorem _ _ _ a -> exprVars a Assume a -> exprVars a Label _ a -> stmtVars a Null -> [] --- Variables in an expression.+-- | Variables in an expression. exprVars :: E a -> [UV] exprVars a = case a of Ref a -> [untype a]@@ -152,4 +156,15 @@ Le a b -> exprVars a ++ exprVars b Ge a b -> exprVars a ++ exprVars b Mux a b c -> exprVars a ++ exprVars b ++ exprVars c++-- | Theorems in a program.+theorems :: Statement -> [(Int, Int, [Int], E Bool)]+theorems a = case a of+ Theorem id k lemmas expr -> [(id, k, lemmas, expr)]+ Assign _ _ -> []+ Branch _ a b -> theorems a ++ theorems b+ Sequence a b -> theorems a ++ theorems b+ Assume _ -> []+ Label _ a -> theorems a+ Null -> []
− Language/ImProve/Examples.hs
@@ -1,200 +0,0 @@--- | ImProve examples.-module Language.ImProve.Examples- ( buildGCD- , counter- , verifyCounter- , arbiterSpec- , arbiter- , arbiter1- , arbiter2- , arbiter3- , verifyArbiters- , buildArbiters- , runAll- ) where--import Language.ImProve---- | Computes the greatest common divison of two integers.--- Returns true if the computation is done, and the result.-gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)-gcd' a b = do- a0 <- int "a0" 0 -- Copy of input 'a'.- b0 <- int "b0" 0 -- Copy of input 'b'.- a1 <- int "a1" 0 -- Working copy of 'a'.- b1 <- int "b1" 0 -- Working copy of 'b'.-- -- A new input to process.- "startNew" -| if_ (a /=. ref a0 ||. b /=. ref b0) $ do- a0 <== a- b0 <== b- a1 <== a- b1 <== b-- -- Reduce a1.- "reduceA" -| if_ (ref a1 >. ref b1) $ do- a1 <== ref a1 - ref b1-- -- Reduce b1.- "reduceB" -| if_ (ref b1 >. ref a1) $ do- b1 <== ref b1 - ref a1-- -- Done if a1 == b1.- return (ref a1 ==. ref b1, ref a1)----- | A top level wrapper for gcd'.-gcdMain :: Stmt ()-gcdMain = do- let a = input int ["a"] -- Input variable 'a'.- b = input int ["b"] -- Input variable 'b'.- done <- bool "done" False -- Variable signalling completion.- result <- int "result" 0 -- Result of GCD.-- -- Call gcd' in its own scope. (Scopes prevent variable name collisions.)- (done', result') <- "gcd" -| gcd' a b-- -- Bind the results to the output variables.- done <== done'- result <== result'---- | Build the gcdMain code (i.e. gcd.c, gcd.h).-buildGCD :: IO ()-buildGCD = code "gcd" gcdMain------ | A rolling counter verification example.-counter :: Stmt ()-counter = do- -- The counter variable.- counter <- int "counter" 0-- -- Specification.- "GreaterThanOrEqualTo0" -| assert $ ref counter >=. 0- "LessThan10" -| assert $ ref counter <. 10-- -- Implementation.- ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)-- -- 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.- "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.- "NotRequestedA" -| assert $ not_ requestA --> not_ grantA- "NotRequestedB" -| assert $ not_ requestB --> not_ grantB- "NotRequestedC" -| assert $ not_ requestC --> not_ grantC-- -- Grants to single requests.- "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.- "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)-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-- "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)---- | 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 = name -| do- -- Create input variables.- let requestA = input bool ["requestA"]- requestB = input bool ["requestB"]- requestC = input bool ["requestC"]- let requests = (requestA, requestB, requestC)-- -- Instantiate implementation.- grants@(grantA, grantB, grantC) <- "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-
− Language/ImProve/Narrow.hs
@@ -1,78 +0,0 @@-module Language.ImProve.Narrow (narrow) where--import Data.List-import Data.Maybe--import Language.ImProve.Core--narrow :: Statement -> Statement-narrow stmt = assumes- where- assumes = foldl Sequence Null [ Label lab $ Assume assume | (lab, opt) <- optimizations, assume <- opt stmt ]- optimizations =- [ ("constantAssigns", constantAssigns)- , ("timerRanges", timerRanges)- ]--constantAssigns :: Statement -> [E Bool]-constantAssigns stmt = mapMaybe f1 $ stmtVars stmt- where- f1 :: UV -> Maybe (E Bool)- f1 uv- | input = Nothing- | otherwise = do- assigns <- lastConstAssign uv stmt- case (init, nub $ init : assigns) of- (Bool _, [_, _]) -> Nothing- (_, a) -> return $ foldl1 Or $ map f2 a- where- f2 :: Const -> E Bool- f2 assign = case (init, assign) of- (Bool a, Bool b) -> Eq (Ref (V input path a)) (Const b)- (Int a, Int b) -> Eq (Ref (V input path a)) (Const b)- (Float a, Float b) -> Eq (Ref (V input path a)) (Const b)- _ -> undefined- (input, path, init) = varInfo uv--lastConstAssign :: UV -> Statement -> Maybe [Const]-lastConstAssign uv a = do- (_, a) <- lastConstAssign a- return $ nub a- where- lastConstAssign :: Statement -> Maybe (Bool, [Const])- lastConstAssign a = case a of- Assign v (Const a) | untype v == uv -> Just (True, [const' a])- Assign v _ | untype v == uv -> Nothing- Branch _ a b -> do- (aDone, a) <- lastConstAssign a- (bDone, b) <- lastConstAssign b- return (aDone && bDone, a ++ b)- Sequence a b -> do- (bDone, b) <- lastConstAssign b- if bDone- then return (True, b)- else do- (aDone, a) <- lastConstAssign a- return (aDone, a ++ b)- Label _ a -> lastConstAssign a- _ -> Just (False, [])--timerRanges :: Statement -> [E Bool]-timerRanges stmt = [] --XXX- where- intCode :: [(VarInfo, Statement)]- intCode = [ (varInfo a, assignedVar a stmt) | a@(UVInt _) <- stmtVars stmt ]---- | Reduces a program only to assignments of a certain variable.-assignedVar :: UV -> Statement -> Statement-assignedVar v a = case a of- Assign v' _ | v == untype v' -> a- Branch cond a b -> case (assignedVar v a, assignedVar v b) of- (Null, Null) -> Null- (a, b) -> Branch cond a b- Sequence a b -> case (assignedVar v a, assignedVar v b) of- (Null, Null) -> Null- (a, b) -> Sequence a b- Label a b -> Label a $ assignedVar v b- _ -> Null-
Language/ImProve/Verify.hs view
@@ -1,7 +1,6 @@ module Language.ImProve.Verify (verify) where import Control.Monad.State-import Data.List import Math.SMT.Yices.Pipe import Math.SMT.Yices.Syntax import System.IO@@ -9,87 +8,38 @@ import Language.ImProve.Code () import Language.ImProve.Core-import Language.ImProve.Narrow -- | Verify a program with k-induction.-verify :: FilePath -> Int -> Statement -> IO ()-verify _ maxK _ | maxK < 1 = error "max k can not be less than 1"-verify yices maxK program = do- putStrLn "state variable narrowing ..."- print $ narrow program- mapM_ (verifyProgram yices format maxK $ narrow program) $ trimAssertions $ labelAssertions program- where- format = "verifying %-" ++ show (maximum [ length $ pathName path | path <- assertions program ]) ++ "s "---- | Set of statements containing only one assertion.-trimAssertions :: Statement -> [Statement]-trimAssertions program = [ a | a <- trimAssertions program, length (assertions a) == 1 ]+verify :: FilePath -> Statement -> IO ()+verify yices program = mapM_ (proveTheorem yices format program) $ theorems program where- trimAssertions :: Statement -> [Statement]- trimAssertions a = case a of- Sequence a b -> [ Sequence a (removeAssertions b) | a <- trimAssertions a ]- ++ [ Sequence (removeAssertions a) b | b <- trimAssertions b ]- Branch cond a b -> [ Branch cond a (removeAssertions b) | a <- trimAssertions a ]- ++ [ Branch cond (removeAssertions a) b | b <- trimAssertions b ]- Label name a -> [ Label name a | a <- trimAssertions a ]- a -> [a]---- | Remove all assertions.-removeAssertions :: Statement -> Statement-removeAssertions a = case a of- Assert _ -> Null- Sequence a b -> Sequence (removeAssertions a) (removeAssertions b)- Branch cond a b -> Branch cond (removeAssertions a) (removeAssertions b)- Label name a -> Label name $ removeAssertions a- a -> a+ format = "%-" ++ show (maximum [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s " --- | Ensure all assertions are uniquely labed.-labelAssertions :: Statement -> Statement-labelAssertions program = evalState (f program) ([], [], 1)+-- | Path of a theorem.+theoremPath :: Int -> Statement -> Path+theoremPath t stmt = case f stmt of+ Nothing -> error $ "theorem not found: " ++ show t+ Just p -> p where- f :: Statement -> State (Path, [Path], Int) Statement+ pair :: Statement -> Statement -> Maybe Path+ pair a b = case (f a, f b) of+ (Just a, _) -> Just a+ (_, Just a) -> Just a+ _ -> Nothing+ f :: Statement -> Maybe Path f a = case a of- Branch a b c -> do- b <- f b- c <- f c- return $ Branch a b c- Sequence a b -> do- a <- f a- b <- f b- return $ Sequence a b- Assert a -> do- (path, paths, n) <- get- if elem path paths- then do- put (path, paths, n + 1)- f $ Label (show n) $ Assert a- else do- put (path, path : paths, n)- return $ Assert a+ Theorem t' _ _ _ | t == t' -> Just [show t']+ Sequence a b -> pair a b+ Branch _ a b -> pair a b Label name a -> do- (path, paths, n) <- get- put (path ++ [name], paths, n)- a <- f a- (_, paths, n) <- get- put (path, paths, n)- return $ Label name a- a -> return a---- | Paths of all assertions.-assertions :: Statement -> [Path]-assertions = assertions []- where- assertions :: Path -> Statement -> [Path]- assertions path a = case a of- Assert _ -> [path]- Sequence a b -> assertions path a ++ assertions path b- Branch _ a b -> assertions path a ++ assertions path b- Label name a -> assertions (path ++ [name]) a- _ -> []+ path <- f a+ return $ name : path+ _ -> Nothing +{- -- | Trim all unneeded stuff from a program.-trimProgram :: Statement -> Statement -> Statement-trimProgram base program = trim program+trimProgram :: Int -> Statement -> Statement+trimProgram t program = trim program where vars = fixPoint [] fixPoint :: [UV] -> [UV]@@ -134,47 +84,47 @@ Assume _ -> [] Label _ a -> modifiedVars a Null -> []+-} --- | Verify a trimmed program.-verifyProgram :: FilePath -> String -> Int -> Statement -> Statement -> IO ()-verifyProgram yices format maxK narrowing program' = do+-- | Prove a single theorem.+proveTheorem :: FilePath -> String -> Statement -> (Int, Int, [Int], E Bool) -> IO ()+proveTheorem yices format program (id, k, lemmas, _) = do printf format name hFlush stdout- env0 <- initEnv program --XXX Need to add narrowing assumptions.- execStateT (check yices name maxK program env0 1) env0+ env0 <- initEnv program+ execStateT (check yices name id lemmas program env0 k) env0 return () where- program = Sequence (trimProgram program' narrowing) (trimProgram program' program')- name = pathName $ head' "a1" $ assertions program--head' msg a = if null a then error msg else head a+ name = pathName $ theoremPath id program data Result = Pass | Fail [ExpY] | Problem -- | k-induction.-check :: FilePath -> Name -> Int -> Statement -> Env -> Int -> Y ()-check yices name maxK program env0 k = do- addTrace $ Cycle' $ k - 1- inputs program- evalStmt (LitB True) program+check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y ()+check yices name theorem lemmas program env0 k = do+ sequence_ [ addTrace (Cycle' i) >> inputs program >> evalStmt theorem lemmas (LitB True) program | i <- [0 .. k - 1] ] resultBasis <- checkBasis yices program env0 case resultBasis of- Fail a -> liftIO (printf "FAILED: disproved basis in k = %d (see %s.trace)\n" k name) >> writeTrace name a+ Fail a -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace name a Problem -> error "Verify.check1" Pass -> do resultStep <- checkStep yices case resultStep of- Fail a | k < maxK -> check yices name maxK program env0 (k + 1)- | otherwise -> liftIO (printf "inconclusive: unable to proved step up to max k = %d (see %s.trace)\n" k name) >> writeTrace name a+ Fail a -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace name a Problem -> error "Verify.check2"- Pass -> liftIO $ printf "passed: proved step in k = %d\n" k+ Pass -> liftIO $ printf "proved\n" -- | Check induction step. checkStep :: FilePath -> Y Result checkStep yices = do env <- get- r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env) ++ [ASSERT $ NOT $ head' "a2" $ asserts env] ++ [CHECK]+ r <- liftIO $ quickCheckY' yices [] $ reverse (cmds env) ++ [assert env] ++ [CHECK] return $ result r+ where+ assert env = case asserts env of+ [] -> error "unexpected: no assertion"+ [a] -> ASSERT $ NOT $ a+ a : b -> ASSERT $ NOT $ AND b :=> a -- | Check induction basis. checkBasis :: FilePath -> Statement -> Env -> Y Result@@ -198,18 +148,23 @@ _ -> error $ "unexpected yices results: " ++ show a -evalStmt :: ExpY -> Statement -> Y ()-evalStmt enabled a = case a of+evalStmt :: Int -> [Int] -> ExpY -> Statement -> Y ()+evalStmt theorem lemmas enabled a = case a of Null -> return ()- Sequence a b -> evalStmt enabled a >> evalStmt enabled b+ Sequence a b -> evalStmt theorem lemmas enabled a >> evalStmt theorem lemmas enabled b Assign a b -> assign a b- Assert a -> do- a <- evalExpr a- b <- newBoolVar- addCmd $ ASSERT (VarE b := (enabled :=> a))- env <- get- put env { asserts = VarE b : asserts env }- addTrace $ Assert' b+ Theorem id _ _ a+ | elem id lemmas -> do+ a <- evalExpr a+ addCmd $ ASSERT (enabled :=> a)+ | id == theorem -> do+ a <- evalExpr a+ b <- newBoolVar+ addCmd $ ASSERT (VarE b := (enabled :=> a))+ env <- get+ put env { asserts = VarE b : asserts env }+ addTrace $ Assert' b+ | otherwise -> return () Assume a -> do a <- evalExpr a addCmd $ ASSERT (enabled :=> a)@@ -219,16 +174,16 @@ addCmd $ ASSERT (VarE b := a) env0 <- get put env0 { trace = [] }- evalStmt (AND [enabled, a]) onTrue+ evalStmt theorem lemmas (AND [enabled, a]) onTrue env1 <- get put env1 { trace = [] }- evalStmt (AND [enabled, NOT a]) onFalse+ evalStmt theorem lemmas (AND [enabled, NOT a]) onFalse env2 <- get put env2 { trace = Branch' b (reverse $ trace env1) (reverse $ trace env2) : trace env0 } Label name a -> do env0 <- get put env0 { trace = [] }- evalStmt enabled a+ evalStmt theorem lemmas enabled a env1 <- get put env1 { trace = Label' name (reverse $ trace env1) : trace env0 } where
improve.cabal view
@@ -1,5 +1,5 @@ name: improve-version: 0.1.6+version: 0.2.0 category: Language, Formal Methods, Embedded @@ -32,8 +32,6 @@ Language.ImProve Language.ImProve.Code Language.ImProve.Core- Language.ImProve.Examples- Language.ImProve.Narrow Language.ImProve.Tree Language.ImProve.Verify