Validation of Statements, based on a stochastic approach.

Example Deterministic statements

>>> validate (SValid && (SInvalid || SValid))
Valid

The validation shows the following output:

>> Omega (StdGen {unStdGen = SMGen 1872899651221430933 9051984386581193015})
>> --------------------------------------------------------------------------------
>> Summary
>> 1 sample tested where 0 tests are false, having 0 denied premises
>> 5 tests with a false ratio of 0% and a denied premises ratio of 0%

From the third line on the number of samples is shown and how many tests over all have been performed to determine the result. As the above statement is obviously deterministic, only one sample has been tested, as the result is independent of the used stochastic.

Example Non deterministic statements

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

The validation shows the following output:

>> Omega (StdGen {unStdGen = SMGen 8429292192981378265 11527977991108410805})
>> --------------------------------------------------------------------------------
>> Summary
>> 10 samples tested where 0 tests are false, having 0 denied premises
>> 94 tests with a false ratio of 0% and a denied premises ratio of 

As this statement is non deterministic, the validation of it pics randomly 10 samples of Omegas and Wides (see the number of samples in the summery above) - starting from the shown Omega - and uses validateStoch to determine for each sample the result. All this results are combined with the &&-operator to yield the final result.

Example Lazy validation

>>> validate (SValid || throw DivideByZero)
Valid

Example Denied premises

>>> let s = Forall xInt (\i -> (i == i+1):?>Params["i":=show i]) in validate (s :=> s)
Valid

The validation shows the following output:

>> Omega (StdGen {unStdGen = SMGen 1872899651221430933 9051984386581193015})
>> --------------------------------------------------------------------------------
>> Summary
>> 1 sample tested where 0 tests are false, having 4 denied premises
>> 7 tests with a false ratio of 0% and a denied premises ratio of 57%

The statement s is obviously invalid but the tautology s :=> s is valid because of denied premises, which is shown in the summery.

Example Invalid statements

>>> validate (Forall (xIntB 0 10) (\i -> (10 < i):?>Params["i":=show i]))
Invalid

The validation shows the following output:

>> Omega (StdGen {unStdGen = SMGen 8429292192981378265 11527977991108410805})
>> --------------------------------------------------------------------------------
for all Invalid
  and Invalid
    check Invalid
      Invalid
      parameters
        i := 9

>> --------------------------------------------------------------------------------
>> Summary
>> 1 sample tested where 3 tests are false, having 0 denied premises
>> 3 tests with a false ratio of 100% and a denied premises ratio of 0%

where from the third line on the invalid test is shown and the summery shows that in the first sample for Omega and Wide an invalid test has been found.

Example Tracking of exceptions

>>> validate (SValid && (Label "bad" :<=>: throw DivideByZero))
*** Exception: FailedStatement divide by zero

The validation shows the following output:

>> Omega (StdGen {unStdGen = SMGen 3069986384088197145 15225250911862971905})
>> --------------------------------------------------------------------------------
>> failed sample
and divide by zero
  (bad) divide by zero
    failure divide by zero

>> --------------------------------------------------------------------------------
>> Summary
>> 1 sample tested where 0 tests are false, having 0 denied premises
>> 3 tests

The failed sample part of the output shows that in an and construct the component - labeled by bad - has been throwing an exception during the validation process.

Example Extended stochastic

If we validate the obviously false statement

> validate Forall (xIntB 0 1000) (\i -> (i < 1000) :?> Params["i":=show i])

the validation may nevertheless yield ProbablyValid - because all randomly picked Omegas and Wides may produce only values which are strict smaller then 1000. To overcome this problem and to get more confidence of the result it is possible to adapt the stochastic and use validateStochastic Massive instead (validate is equivalent to validateStochastic Sparse).

Note The here defined validation is highly inspired by the QuickCheck package. But we have chosen to adopt the idea to fit more our needs. For example, if a statement throws an exception, then the occurrence can be tracked. Also we devoted special attention to the logic of statements (as Statement is an instance Boolean, they fulfill all the logical tautologies). For example, the simple tautology s :=> s breaks, if you don't take special care during the validating process or if you allow user interactions.