| Copyright | (C) 2017 ATS Advanced Telematic Systems GmbH |
|---|---|
| License | BSD-style (see the file LICENSE) |
| Maintainer | Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk> |
| Stability | provisional |
| Portability | non-portable (GHC extensions) |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Test.StateMachine.Logic
Description
This module defines a predicate logic-like language and its counterexample semantics.
Synopsis
- data Logic
- data LogicPredicate
- = forall a.(Eq a, Show a) => a :== a
- | forall a.(Eq a, Show a) => a :/= a
- | forall a.(Ord a, Show a) => a :< a
- | forall a.(Ord a, Show a) => a :<= a
- | forall a.(Ord a, Show a) => a :> a
- | forall a.(Ord a, Show a) => a :>= a
- | forall t a.(Foldable t, Eq a, Show a, Show (t a)) => Member a (t a)
- | forall t a.(Foldable t, Eq a, Show a, Show (t a)) => NotMember a (t a)
- dual :: LogicPredicate -> LogicPredicate
- strongNeg :: Logic -> Logic
- data Counterexample
- = BotC
- | Fst Counterexample
- | Snd Counterexample
- | EitherC Counterexample Counterexample
- | ImpliesC Counterexample
- | NotC Counterexample
- | PredicateC LogicPredicate
- | forall a.Show a => ForallC a Counterexample
- | forall a.Show a => ExistsC [a] [Counterexample]
- | BooleanC
- | AnnotateC String Counterexample
- data Value
- boolean :: Logic -> Bool
- logic :: Logic -> Value
- evalLogicPredicate :: LogicPredicate -> Value
- gatherAnnotations :: Logic -> [String]
- (.==) :: (Eq a, Show a) => a -> a -> Logic
- (./=) :: (Eq a, Show a) => a -> a -> Logic
- (.<) :: (Ord a, Show a) => a -> a -> Logic
- (.<=) :: (Ord a, Show a) => a -> a -> Logic
- (.>) :: (Ord a, Show a) => a -> a -> Logic
- (.>=) :: (Ord a, Show a) => a -> a -> Logic
- member :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
- notMember :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
- (.//) :: Logic -> String -> Logic
- (.&&) :: Logic -> Logic -> Logic
- (.||) :: Logic -> Logic -> Logic
- (.=>) :: Logic -> Logic -> Logic
- forAll :: Show a => [a] -> (a -> Logic) -> Logic
- exists :: Show a => [a] -> (a -> Logic) -> Logic
Documentation
data LogicPredicate Source #
Constructors
| forall a.(Eq a, Show a) => a :== a | |
| forall a.(Eq a, Show a) => a :/= a | |
| forall a.(Ord a, Show a) => a :< a | |
| forall a.(Ord a, Show a) => a :<= a | |
| forall a.(Ord a, Show a) => a :> a | |
| forall a.(Ord a, Show a) => a :>= a | |
| forall t a.(Foldable t, Eq a, Show a, Show (t a)) => Member a (t a) | |
| forall t a.(Foldable t, Eq a, Show a, Show (t a)) => NotMember a (t a) |
Instances
| Show LogicPredicate Source # | |
Defined in Test.StateMachine.Logic Methods showsPrec :: Int -> LogicPredicate -> ShowS # show :: LogicPredicate -> String # showList :: [LogicPredicate] -> ShowS # | |
dual :: LogicPredicate -> LogicPredicate Source #
data Counterexample Source #
Constructors
| BotC | |
| Fst Counterexample | |
| Snd Counterexample | |
| EitherC Counterexample Counterexample | |
| ImpliesC Counterexample | |
| NotC Counterexample | |
| PredicateC LogicPredicate | |
| forall a.Show a => ForallC a Counterexample | |
| forall a.Show a => ExistsC [a] [Counterexample] | |
| BooleanC | |
| AnnotateC String Counterexample |
Instances
| Show Counterexample Source # | |
Defined in Test.StateMachine.Logic Methods showsPrec :: Int -> Counterexample -> ShowS # show :: Counterexample -> String # showList :: [Counterexample] -> ShowS # | |
Constructors
| VFalse Counterexample | |
| VTrue |
gatherAnnotations :: Logic -> [String] Source #
Gather user annotations of a true logic expression.
>>>gatherAnnotations (Top .// "top")["top"]
>>>gatherAnnotations ((Bot .// "bot") .|| (Top .// "top"))["top"]
>>>gatherAnnotations (Top .// "top1" .&& Top .// "top2")["top1","top2"]
>>>gatherAnnotations (Bot .// "bot" .&& Top .// "top")[]
>>>gatherAnnotations (forAll [1,2,3] (\i -> 0 .< i .// "positive"))["positive","positive","positive"]
>>>gatherAnnotations (forAll [0,1,2,3] (\i -> 0 .< i .// "positive"))[]
>>>gatherAnnotations (exists [1,2,3] (\i -> 0 .< i .// "positive"))["positive"]