copilot-theorem 3.17 → 3.18

raw patch · 4 files changed

+162/−3 lines, 4 filesdep +QuickCheckdep +copilot-theoremdep +test-frameworkdep ~basedep ~copilot-coredep ~copilot-prettyprinter

Dependencies added: QuickCheck, copilot-theorem, test-framework, test-framework-quickcheck2

Dependency ranges changed: base, copilot-core, copilot-prettyprinter

Files

• CHANGELOG +5/−0
• copilot-theorem.cabal +31/−3
• tests/Main.hs +18/−0
• tests/Test/Copilot/Theorem/What4.hs +108/−0

@@ -1,3 +1,8 @@+2024-01-07+        * Version bump (3.18). (#487)+        * Introduce testing infrastructure for Copilot.Theorem.What4. (#474)+        * Replace uses of forall with forAll. (#470)+ 2023-11-07         * Version bump (3.17). (#466)         * Relax version constraint on what4. (#461)

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 3.17+version                   : 3.18 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -63,8 +63,8 @@                           , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.6 -                          , copilot-core          >= 3.17 && < 3.18-                          , copilot-prettyprinter >= 3.17 && < 3.18+                          , copilot-core          >= 3.18 && < 3.19+                          , copilot-prettyprinter >= 3.18 && < 3.19    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove@@ -108,3 +108,31 @@                           , Copilot.Theorem.TransSys.Type                            , Copilot.Theorem.What4.Translate++test-suite unit-tests+  type:+    exitcode-stdio-1.0++  main-is:+    Main.hs++  other-modules:+    Test.Copilot.Theorem.What4++  build-depends:+      base+    , QuickCheck+    , test-framework+    , test-framework-quickcheck2++    , copilot-core+    , copilot-theorem++  hs-source-dirs:+    tests++  default-language:+    Haskell2010++  ghc-options:+    -Wall

@@ -0,0 +1,18 @@+-- | Test copilot-theorem.+module Main where++-- External imports+import Test.Framework (Test, defaultMain)++-- Internal imports+import qualified Test.Copilot.Theorem.What4++-- | Run all unit tests on copilot-theorem.+main :: IO ()+main = defaultMain tests++-- | All unit tests in copilot-theorem.+tests :: [Test.Framework.Test]+tests =+  [ Test.Copilot.Theorem.What4.tests+  ]

@@ -0,0 +1,108 @@+-- The following warning is disabled due to a necessary instance of SatResult+-- defined in this module.+{-# OPTIONS_GHC -fno-warn-orphans #-}+-- | Test copilot-theorem:Copilot.Theorem.What4.+module Test.Copilot.Theorem.What4 where++-- External imports+import Data.Int                             (Int8)+import Test.Framework                       (Test, testGroup)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.QuickCheck                      (Property, arbitrary, forAll)+import Test.QuickCheck.Monadic              (monadicIO, run)++-- External imports: Copilot+import           Copilot.Core.Expr      (Expr (Const, Op2))+import           Copilot.Core.Operators (Op2 (..))+import           Copilot.Core.Spec      (Spec (..))+import qualified Copilot.Core.Spec      as Copilot+import           Copilot.Core.Type      (Typed (typeOf))++-- Internal imports: Modules being tested+import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove)++-- * Constants++-- | Unit tests for copilot-theorem:Copilot.Theorem.What4.+tests :: Test.Framework.Test+tests =+  testGroup "Copilot.Theorem.What4"+    [ testProperty "Prove via Z3 that true is valid"    testProveZ3True+    , testProperty "Prove via Z3 that false is invalid" testProveZ3False+    , testProperty "Prove via Z3 that x == x is valid"  testProveZ3EqConst+    ]++-- * Individual tests++-- | Test that Z3 is able to prove the following expression valid:+-- @+--   constant True+-- @+testProveZ3True :: Property+testProveZ3True =+    monadicIO $ run $ checkResult Z3 propName spec Valid+  where+    propName :: String+    propName = "prop"++    spec :: Spec+    spec = propSpec propName $ Const typeOf True++-- | Test that Z3 is able to prove the following expression invalid:+-- @+--   constant False+-- @+testProveZ3False :: Property+testProveZ3False =+    monadicIO $ run $ checkResult Z3 propName spec Invalid+  where+    propName :: String+    propName = "prop"++    spec :: Spec+    spec = propSpec propName $ Const typeOf False++-- | Test that Z3 is able to prove the following expresion valid:+-- @+--   for all (x :: Int8), constant x == constant x+-- @+testProveZ3EqConst :: Property+testProveZ3EqConst = forAll arbitrary $ \x ->+    monadicIO $ run $ checkResult Z3 propName (spec x) Valid+  where+    propName :: String+    propName = "prop"++    spec :: Int8 -> Spec+    spec x = propSpec propName $+      Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)++-- | Check that the solver's satisfiability result for the given property in+-- the given spec matches the expectation.+checkResult :: Solver -> String -> Spec -> SatResult -> IO Bool+checkResult solver propName spec expectation = do+  results <- prove solver spec++  -- Find the satisfiability result for propName.+  let propResult = lookup propName results++  -- The following check also works for the case in which the property name+  -- does not exist in the results, in which case the lookup returns 'Nothing'.+  return $ propResult == Just expectation++-- * Auxiliary++-- | Build a 'Spec' that contains one property with the given name and defined+-- by the given boolean expression.+propSpec :: String -> Expr Bool -> Spec+propSpec propName propExpr = Spec [] [] [] [Copilot.Property propName propExpr]++-- | Equality for 'SatResult'.+--+-- This is an orphan instance, so we suppress the warning that GHC would+-- normally produce with a GHC option at the top.+instance Eq SatResult where+  Valid   == Valid   = True+  Invalid == Invalid = True+  Unknown == Unknown = True+  _       == _       = False