improve 0.3.4 → 0.4.0

raw patch · 8 files changed

+62/−60 lines, 8 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/ImProve.hs +10/−16
• Language/ImProve/Code/Ada.hs +4/−4
• Language/ImProve/Code/C.hs +2/−2
• Language/ImProve/Code/Simulink.hs +2/−2
• Language/ImProve/Core.hs +17/−17
• Language/ImProve/Path.hs +1/−1
• Language/ImProve/Verify.hs +25/−17
• improve.cabal +1/−1

@@ -57,7 +57,7 @@ /Assertion Statements/  @-assert(condition);        'theorem' name k lemmas condition+assert(condition);        'assert' name k condition @  /Statement Labels/@@ -148,7 +148,6 @@   , AllE   , NumE   , Name-  , Theorem   -- * Expressions   -- ** Constants   , true@@ -213,9 +212,9 @@   -- ** Incrementing and decrementing.   , incr   , decr-  -- ** Assumptions and theorems.+  -- ** Assumptions and assertions.   , assume-  , theorem+  , assert   -- * Verification   , verify   -- * Code Generation@@ -472,27 +471,22 @@ class Assign a where (<==) :: V a -> E a -> Stmt () instance AllE a => Assign a where a <== b = statement $ Assign a b --- | Theorem to be proven or used as lemmas to assist proofs of other theorems.-data Theorem = Theorem' Int- -- | Assume a condition is true.---   Assumptions are used as lemmas to other theorems.-assume :: Name -> E Bool -> Stmt Theorem+--   Assumptions are used as lemmas to other assertions.+assume :: Name -> E Bool -> Stmt () assume name a = do   (id, path, stmt) <- get   put (id + 1, path, Sequence stmt $ Label name $ Assume id a)-  return $ Theorem' id --- | Defines a new theorem.+-- | Defines a new assertion. ----- > theorem name k lemmas proposition-theorem :: Name -> Int -> [Theorem] -> E Bool -> Stmt Theorem-theorem name k lemmas proposition+-- > assert name k proposition+assert :: Name -> Int -> E Bool -> Stmt ()+assert name k 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+    put (id + 1, path, Sequence stmt $ Label name $ Assert id k proposition)  -- | Conditional if-else. ifelse :: E Bool -> Stmt () -> Stmt () -> Stmt ()

@@ -55,11 +55,11 @@   Assign a b -> name ++ "_Variables." ++ pathName a ++ " := " ++ codeExpr b ++ ";\n"   Branch a b Null -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "end if;\n"   Branch a b c    -> "if " ++ codeExpr a ++ " then\n" ++ indent (codeStmt name path b) ++ "\nelse\n" ++ indent (codeStmt name path c) ++ "end if;\n"-  Sequence a b -> codeStmt name path a ++ codeStmt name path b-  Theorem _ _ _ a -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"+  Sequence a b    -> codeStmt name path a ++ codeStmt name path b+  Assert _ _ a    -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"   Assume _ a      -> "Assert(" ++ codeExpr a ++ ", " ++ show (pathName path) ++ ");\n"-  Label name' a -> "-- " ++ name' ++ "\n" ++ indent (codeStmt name (path ++ [name']) a)-  Null -> ""+  Label name' a   -> "-- " ++ name' ++ "\n" ++ indent (codeStmt name (path ++ [name']) a)+  Null            -> ""   where    codeExpr :: E a -> String

@@ -41,8 +41,8 @@   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-  Theorem _ _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"-  Assume _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"+  Assert _ _ a -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"+  Assume _ a   -> "assert((" ++ show (pathName path) ++ ", " ++ codeExpr a ++ "));\n"   Label name' a -> "/*" ++ name' ++ "*/\n" ++ indent (codeStmt name (path ++ [name']) a)   Null -> ""   where

@@ -102,7 +102,7 @@   Assign   a b     -> Assign a b   Branch   a b c   -> Branch a (lowerConditionals (And cond a) b) (lowerConditionals (And cond $ Not a) c)   Sequence a b     -> Sequence (lowerConditionals cond a) (lowerConditionals cond b)-  Theorem  a b c d -> Theorem a b c $ Or (Not cond) d+  Assert   a b c   -> Assert a b $ Or (Not cond) c   Assume   i a     -> Assume i $ Or (Not cond) a   Label    a b     -> Label a $ lowerConditionals cond b   Null             -> Null@@ -188,7 +188,7 @@    Sequence a b    -> evalStmt a >> evalStmt b -  Theorem _ _ _ a -> do+  Assert _ _ a -> do     a <- evalExpr a     name <- getPathName     assert <- block' name Assertion

@@ -14,7 +14,7 @@   , varInfo   , stmtVars   , arrayLength-  , theorems+  , assertions   ) where  import Data.List@@ -107,8 +107,8 @@   Assign   :: AllE a => V a -> E a -> Statement   Branch   :: E Bool -> Statement -> Statement -> Statement   Sequence :: Statement -> Statement -> Statement-  Theorem  :: Int -> Int -> [Int] -> E Bool -> Statement -- Theorem id k lemmas expr-  Assume   :: Int -> E Bool -> Statement                 -- Assume id expr+  Assert   :: Int -> Int -> E Bool -> Statement -- Assert id k expr+  Assume   :: Int -> E Bool -> Statement        -- Assume id expr   Label    :: Name -> Statement -> Statement   Null     :: Statement @@ -127,13 +127,13 @@ -- | Variables in a program. stmtVars :: Statement -> [VarInfo] stmtVars a = case a of-  Assign a b   -> nub $ varInfo a : exprVars b-  Branch a b c -> nub $ exprVars a ++ stmtVars b ++ stmtVars c-  Sequence a b -> nub $ stmtVars a ++ stmtVars b-  Theorem _ _ _ a -> exprVars a-  Assume  _ a     -> exprVars a-  Label  _ a   -> stmtVars a-  Null         -> []+  Assign a b    -> nub $ varInfo 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+  Assume  _ a   -> exprVars a+  Label  _ a    -> stmtVars a+  Null          -> []  -- | Variables in an expression. exprVars :: E a -> [VarInfo]@@ -155,14 +155,14 @@   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)]+-- | Assertions in a program.+assertions :: Statement -> [(Int, Int, E Bool)]+assertions a = case a of+  Assert id k expr -> [(id, k, expr)]   Assign _ _   -> []-  Branch _ a b -> theorems a ++ theorems b-  Sequence a b -> theorems a ++ theorems b+  Branch _ a b -> assertions a ++ assertions b+  Sequence a b -> assertions a ++ assertions b   Assume _ _   -> []-  Label  _ a   -> theorems a+  Label  _ a   -> assertions a   Null         -> [] 

@@ -14,7 +14,7 @@   Assign _ _      -> 1   Branch _ a b    -> paths a + paths b   Sequence a b    -> paths a * paths b-  Theorem _ _ _ _ -> 1+  Assert _ _ _ -> 1   Assume  _ _     -> 1   Label  _ a      -> paths a   Null            -> 1

@@ -12,13 +12,13 @@  -- | Verify a program with k-induction. verify :: FilePath -> Statement -> IO ()-verify yices program = mapM_ (proveTheorem yices format program) $ theorems program+verify yices program = proveAssertions yices format program [] $ assertions program   where-  format = "%-" ++ show (maximum' [ length $ pathName $ theoremPath t program | (t, _, _, _) <- theorems program ]) ++ "s    "+  format = "%-" ++ show (maximum' [ length $ pathName $ assertionPath t program | (t, _, _) <- assertions program ]) ++ "s    " --- | Path of a theorem.-theoremPath :: Int -> Statement -> Path-theoremPath t stmt = case f stmt of+-- | Path of an assertion.+assertionPath :: Int -> Statement -> Path+assertionPath t stmt = case f stmt of   Nothing -> error $ "theorem not found: " ++ show t   Just p  -> p   where@@ -29,7 +29,7 @@     _ -> Nothing   f :: Statement -> Maybe Path   f a = case a of-    Theorem t' _ _ _ | t == t' -> Just []+    Assert t' _ _ | t == t' -> Just []     Sequence a b -> pair a b     Branch _ a b -> pair a b     Label name a -> do@@ -37,34 +37,42 @@       return $ name : path     _ -> Nothing --- | Prove a single theorem.-proveTheorem :: FilePath -> String -> Statement -> (Int, Int, [Int], E Bool) -> IO ()-proveTheorem yices format program (id, k, lemmas, _) = do+proveAssertions :: FilePath -> String -> Statement -> [Int] -> [(Int, Int, E Bool)] -> IO ()+proveAssertions _ _ _ _ [] = return ()+proveAssertions yices format program lemmas ((id, k, _) : rest) = do   printf format name   hFlush stdout   env0 <- initEnv program-  execStateT (check yices name id lemmas program env0 k) env0-  return ()+  pass <- evalStateT (check yices name id lemmas program env0 k) env0+  proveAssertions yices format program (if pass then id : lemmas else lemmas) rest   where-  name = pathName $ theoremPath id program+  name = pathName $ assertionPath id program  data Result = Pass | Fail [ExpY] | Problem  -- | k-induction.-check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y ()+check :: FilePath -> Name -> Int -> [Int] -> Statement -> Env -> Int -> Y Bool check yices name theorem lemmas program env0 k = do   mapM_ step [0 .. k - 1]   resultBasis <- checkBasis yices program env0   case resultBasis of-    Fail a  -> liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name) >> writeTrace name a+    Fail a  -> do+      liftIO (printf "FAILED: disproved basis (see %s.trace)\n" name)+      writeTrace name a+      return False     Problem -> error "Verify.check1"     Pass -> do       step k       resultStep <- checkStep yices       case resultStep of-        Fail a  -> liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name) >> writeTrace name a+        Fail a  -> do+	  liftIO (printf "inconclusive: unable to proved step (see %s.trace)\n" name)+	  writeTrace name a+	  return False         Problem -> error "Verify.check2"-        Pass    -> liftIO $ printf "proved\n"+        Pass    -> do+	  liftIO $ printf "proved\n"+	  return True   where   step :: Int -> Y ()   step i = do@@ -110,7 +118,7 @@   Null -> return ()   Sequence a b -> evalStmt theorem lemmas enabled a >> evalStmt theorem lemmas enabled b   Assign a b -> assign a b-  Theorem id _ _ a+  Assert id _ a     | elem id lemmas -> do       a <- evalExpr a       addCmd $ ASSERT (enabled :=> a)

@@ -1,5 +1,5 @@ name:    improve-version: 0.3.4+version: 0.4.0  category: Language, Formal Methods, Embedded