1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
-- | An example showing the usage of the What4 backend in copilot-theorem for
-- propositional logic on boolean streams.
module Main where
import qualified Prelude as P
import Control.Monad (void, forM_)
import Language.Copilot
import Copilot.Theorem.What4
spec :: Spec
spec = do
-- The constant value true, which is translated as the corresponding SMT
-- boolean literal.
void $ prop "Example 1" (forall true)
-- The constant value false, which is translated as the corresponding SMT
-- boolean literal.
void $ prop "Example 2" (forall false)
-- An inductively defined flavor of true, which requires induction to prove,
-- and hence is found to be invalid by the SMT solver (since no inductive
-- hypothesis is made).
let a = [True] ++ a
void $ prop "Example 3" (forall a)
-- An inductively defined "a or not a" proposition, which is unprovable by
-- the SMT solver.
let a = [False] ++ b
b = [True] ++ a
void $ prop "Example 4" (forall (a || b))
-- A version of "a or not a" proposition which does not require any sort of
-- inductive argument, and hence is provable.
let a = [False] ++ b
b = not a
void $ prop "Example 5" (forall (a || b))
-- A bit more convoluted version of Example 5, which is provable.
let a = [True, False] ++ b
b = [False] ++ not (drop 1 a)
void $ prop "Example 6" (forall (a || b))
-- An example using external streams.
let a = extern "a" Nothing
void $ prop "Example 7" (forall (a || not a))
main :: IO ()
main = do
spec' <- reify spec
-- Use Z3 to prove the properties.
results <- prove Z3 spec'
-- Print the results.
forM_ results $ \(nm, res) -> do
putStr $ nm <> ": "
case res of
Valid -> putStrLn "valid"
Invalid -> putStrLn "invalid"
Unknown -> putStrLn "unknown"
|
