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
|
-- | An example showing the usage of the What4 backend in copilot-theorem for
-- simple arithmetic.
module Main where
import qualified Prelude as P
import Control.Monad (void, forM_)
import Language.Copilot
import Copilot.Theorem.What4
spec :: Spec
spec = do
-- Define some external streams. Their values are not important, so external
-- streams suffice.
let eint8 :: Stream Int8
eint8 = extern "eint8" Nothing
eword8 :: Stream Word8
eword8 = extern "eword8" Nothing
efloat :: Stream Float
efloat = extern "efloat" Nothing
-- The simplest example involving numbers: equality on constant values.
void $ prop "Example 1" (forAll ((constant (1 :: Int8)) == (constant 1)))
-- Testing "a < a + 1". This should fail, because it isn't true.
void $ prop "Example 2" (forAll (eint8 < (eint8 + 1)))
-- Adding another condition to the above property to make it true.
void $ prop "Example 3" (forAll ((eint8 < (eint8 + 1)) || (eint8 == 127)))
-- Just like the previous example, but with words.
void $ prop "Example 4" (forAll ((eword8 < (eword8 + 1)) || (eword8 == 255)))
-- An example with floats.
void $ prop "Example 5" (forAll ((2 * efloat) == (efloat + efloat)))
-- Another example with floats. This fails, because it isn't true.
void $ prop "Example 6" (forAll ((efloat + 1) /= efloat))
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"
|
