statement on properties..

checking for equality.

checking for inequality.

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

convenient catcher for SomeException.

a labels.

a message.

type of variables.

showing the involved parameters of a statement.

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.

the wide for a Forall and Exist resolution.

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.

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

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

validating a value v.

the truth type of a value v.

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..

pretty showing a value with the given indentation.

the initial indentation given by a indentation string.

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

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

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

path of strings.

number of tests.

reduces true valus to its relevant part.

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

reduces false valus to its relevant part.

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

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

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

reduces failed values to its relevant part.

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

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

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

uniformly distributed random variable of Valid.

validating exceptions which are sub exceptions from SomeOAlgException.