OAlg.Data.Statement.Definition

Statements on properties which can be validated via validateStoch. They serve to implement automatic testing (see OAlg.Control.Validate).

Examples Deterministic

Validation of the valid and invalid statement

>>> getOmega >>= validateStoch SValid 10
Valid

>>> getOmega >>= validateStoch SInvalid 5
Invalid

As no stochastic was used to evaluate the two examples, the result is Valid and Invalid respectively!

Examples Stochastic

Validation of a Forall and Exist statement

>>> getOmega >>= validateStoch (Forall (xIntB 0 10) (\i -> (0 <= i && i <= 10):?>Params["i":=show i]-- )) 100
ProbablyValid

>>> getOmega >>= validateStoch (Exist (xIntB 0 10) (\i -> (11 <= i):?>Params["i":=show i])) 100
ProbablyInvalid

The valuation of these two examples uses the given Omega and Wide of 100 to pick randomly 100 samples of the given random variable xIntB 0 10 and applies these samples to the given test function. The result is ProbablyValid and ProbablyInvalid respectively!

Statement

data Statement where

statement on properties..

Constructors

SInvalid :: Statement

the invalid statement.

SValid :: Statement

the valid statement.

(:?>) :: Bool -> Message -> Statement infix 4

checking a boolean.

Catch :: Exception e => Statement -> (e -> Statement) -> Statement

catching an exception.

Not :: Statement -> Statement

not

(:&&) :: Statement -> Statement -> Statement infixr 3

and

And :: [Statement] -> Statement

and

(:||) :: Statement -> Statement -> Statement infixr 2

or

Or :: [Statement] -> Statement

or

(:=>) :: Statement -> Statement -> Statement infixr 1

implication

Impl :: [Statement] -> Statement -> Statement

implication

(:<=>:) :: Label -> Statement -> Statement infixr 0

efinitional equivalence

(:<=>) :: Statement -> Statement -> Statement infixr 1

equivalence

Eqvl :: [Statement] -> Statement

equivalence

Forall :: X x -> (x -> Statement) -> Statement

the for all constructor

Exist :: X x -> (x -> Statement) -> Statement

the exist constructor.

Instances

HNFData Statement

Defined in OAlg.Data.Statement.Definition

Methods

rhnf :: Statement -> ()

Boolean Statement

Defined in OAlg.Data.Statement.Definition

Methods

false :: Statement

true :: Statement

not :: Statement -> Statement

(||) :: Statement -> Statement -> Statement

or :: [Statement] -> Statement

(&&) :: Statement -> Statement -> Statement

and :: [Statement] -> Statement

(~>) :: Statement -> Statement -> Statement

(<~>) :: Statement -> Statement -> Statement

eqvl :: [Statement] -> Statement

(.==.) :: Eq a => a -> a -> Statement infix 4

checking for equality.

(./=.) :: Eq a => a -> a -> Statement infix 4

checking for inequality.

(|~>) :: Statement -> Statement -> Statement infixr 1

implication without resulting in denied premises for a false premises. This is useful for switch cases.

someException :: Statement -> SomeException -> Statement

convenient catcher for SomeException.

data Label

a labels.

Constructors

Label String

Prp String

Instances

Show Label

Defined in OAlg.Data.Statement.Definition

Methods

showsPrec :: Int -> Label -> ShowS

show :: Label -> String

showList :: [Label] -> ShowS

Verbose Label

Defined in OAlg.Data.Statement.Definition

Methods

vshow :: Verbosity -> Label -> String

data Message

a message.

Constructors

MInvalid

used for relations where no further information is desired or possible to give (see relRelation as an example).

Message String

a message

Params [Parameter]

a list of parameters

Instances

Show Message

Defined in OAlg.Data.Statement.Definition

Methods

showsPrec :: Int -> Message -> ShowS

show :: Message -> String

showList :: [Message] -> ShowS

Verbose Message

Defined in OAlg.Data.Statement.Definition

Methods

vshow :: Verbosity -> Message -> String

type Variable = String

type of variables.

data Parameter where

showing the involved parameters of a statement.

Constructors

(:=) :: Variable -> String -> Parameter

Instances

Show Parameter

Defined in OAlg.Data.Statement.Definition

Methods

showsPrec :: Int -> Parameter -> ShowS

show :: Parameter -> String

showList :: [Parameter] -> ShowS

Verbose Parameter

Defined in OAlg.Data.Statement.Definition

Methods

vshow :: Verbosity -> Parameter -> String

Validating

Stochastic

validateStoch :: Statement -> Wide -> Omega -> IO Valid

validates the statement according to a given Wide and Omega. For deterministic statements better use validateDet and for non deterministic or to get more information validate.

type Wide = Int

the wide for a Forall and Exist resolution.

value :: Statement -> Wide -> Omega -> IO V

evaluates the value of a statement according a given Wide and Omega.

Note

1. The only reason to valuate a statement in the IO monad is to be able to catch exceptions. Other interactions with the real world during the valuation are not performed.
2. During the evaluation process the given wide and omega will not be changed and as such all same random variables will produce exactly the same samples. This restricts the stochastic, but it is necessary for the sound behavior of the validation of statements.

data V

the value of a statement resulting from its validation. Forall and Exist are resolved by finite samples.

Instances

Show V

Defined in OAlg.Data.Statement.Definition

Methods

showsPrec :: Int -> V -> ShowS

show :: V -> String

showList :: [V] -> ShowS

Verbose V

Defined in OAlg.Data.Statement.Definition

Methods

vshow :: Verbosity -> V -> String

valDeterministic :: V -> Bool

determines whether the value is deterministic, i.e. dose not contain a VForall or VExist constructor.

valT :: V -> T

validating a value v.

type T = HNFValue Valid

the truth type of a value v.

data Valid

weak form of classical boolean values arising from stochastically performed valuation of Statements.

Definition Let a, b be in Valid, then we define:

1. not a = toEnum (fromEnum Valid - fromEnum a).
2. a || b = max a b.
3. a && b = min a b.
4. a ~> b = not a || b.

Note min and max are implemented lazy as Valid is bounded. This is important that ~> behaves as desired, i.e. for a ~> b and a = Invalid then b has not to be evaluated, because the maximum is already reached..

Constructors

Invalid

ProbablyInvalid

ProbablyValid

Valid

Instances

Bounded Valid

Defined in OAlg.Data.Statement.Definition

Methods

minBound :: Valid

maxBound :: Valid

Enum Valid

Defined in OAlg.Data.Statement.Definition

Methods

succ :: Valid -> Valid

pred :: Valid -> Valid

toEnum :: Int -> Valid

fromEnum :: Valid -> Int

enumFrom :: Valid -> [Valid]

enumFromThen :: Valid -> Valid -> [Valid]

enumFromTo :: Valid -> Valid -> [Valid]

enumFromThenTo :: Valid -> Valid -> Valid -> [Valid]

Show Valid

Defined in OAlg.Data.Statement.Definition

Methods

showsPrec :: Int -> Valid -> ShowS

show :: Valid -> String

showList :: [Valid] -> ShowS

NFData Valid

Defined in OAlg.Data.Statement.Definition

Methods

rnf :: Valid -> ()

Eq Valid

Defined in OAlg.Data.Statement.Definition

Methods

(==) :: Valid -> Valid -> Bool

(/=) :: Valid -> Valid -> Bool

Ord Valid

Defined in OAlg.Data.Statement.Definition

Methods

compare :: Valid -> Valid -> Ordering

(<) :: Valid -> Valid -> Bool

(<=) :: Valid -> Valid -> Bool

(>) :: Valid -> Valid -> Bool

(>=) :: Valid -> Valid -> Bool

max :: Valid -> Valid -> Valid

min :: Valid -> Valid -> Valid

Boolean Valid

Defined in OAlg.Data.Statement.Definition

Methods

false :: Valid

true :: Valid

not :: Valid -> Valid

(||) :: Valid -> Valid -> Valid

or :: [Valid] -> Valid

(&&) :: Valid -> Valid -> Valid

and :: [Valid] -> Valid

(~>) :: Valid -> Valid -> Valid

(<~>) :: Valid -> Valid -> Valid

eqvl :: [Valid] -> Valid

Validable Valid

Defined in OAlg.Data.Validable

Methods

valid :: Valid -> Statement

Projectible Bool Valid

Defined in OAlg.Data.Statement.Definition

Methods

prj :: Valid -> Bool

showV :: Indent -> V -> String

pretty showing a value with the given indentation.

indent0 :: String -> Indent

the initial indentation given by a indentation string.

showVStatement :: Wide -> Statement -> IO ()

pretty showing the value of a statement according to the given Wide and randomly given Omega.

Deterministic

validateDet :: Statement -> Bool

validation for deterministic statements.

Definition A statement s is called deterministic if and only if it dose not depend on the stochastic nor on the state of the machine.

Examples

>>> validateDet SValid
True

>>> validateDet (Forall xBool (\_ -> SValid))
*** Exception: NonDeterministic

>>> validateDet (SValid || Exist xInt (\i -> (i==0):?>MInvalid))
True

Reducing Values

tests :: V -> [(Int, SPath)]

the list of all relevant tests - i.e 'VDedEqvl l _ where l = Label _ - together with the number of tests.

type SPath = [String]

path of strings.

cntTests :: V -> Int

number of tests.

rdcTrue :: V -> Maybe V

reduces true valus to its relevant part.

cntTestsRdcTrue :: V -> Int

number of tests for true values. Note Before counting the tests they will be first reduced to there relevant part (see rdcTrue).

rdcFalse :: V -> Maybe V

reduces false valus to its relevant part.

cntTestsRdcFalse :: V -> Int

number of tests for false values. Note Before counting the tests they will be first reduced to there relevant part (see rdcFalse).

rdcDndPrms :: V -> Maybe V

reduces ture values - having implications with no conclusions, i.e. denied premises - to its relevant part.

cntTestsRdcDndPrms :: V -> Int

number of tests for values containing denied premises. Note Before counting the tests they will be first reduced to there relevant part (see rdcDndPrms).

rdcFailed :: V -> Maybe V

reduces failed values to its relevant part.

cntTestsRdcFailed :: V -> Int

number of tests for failed values. Note Before counting the tests they will be first reduced to there relevant part (see rdcFailed).

X

xValue :: Statement -> X (Wide, Omega) -> X (IO V)

random variable of valuation values according to the randomly given Wide and Omega.

xWO :: Wide -> Wide -> X (Wide, Omega)

xWO l h is the random variable over wide and omgea, where the wide is bounded between l and h.

xValid :: X Valid

uniformly distributed random variable of Valid.

Exception

data ValidateingException

validating exceptions which are sub exceptions from SomeOAlgException.

Constructors

NonDeterministic

Instances

Exception ValidateingException

Defined in OAlg.Data.Statement.Definition

Methods

toException :: ValidateingException -> SomeException

fromException :: SomeException -> Maybe ValidateingException

displayException :: ValidateingException -> String

Show ValidateingException

Defined in OAlg.Data.Statement.Definition

Methods

showsPrec :: Int -> ValidateingException -> ShowS

show :: ValidateingException -> String

showList :: [ValidateingException] -> ShowS

Eq ValidateingException

Defined in OAlg.Data.Statement.Definition

Methods

(==) :: ValidateingException -> ValidateingException -> Bool

(/=) :: ValidateingException -> ValidateingException -> Bool