Testable.dcl 6.09 KB
Newer Older
1
definition module Gast.Testable
Bas Lijnse's avatar
Bas Lijnse committed
2 3 4 5

/*
	GAST: A Generic Automatic Software Test-system
	
6
	testable: the test algorithm for logical properties
Bas Lijnse's avatar
Bas Lijnse committed
7

8
	Pieter Koopman, 2002-2012
Bas Lijnse's avatar
Bas Lijnse committed
9 10 11 12 13
	Radboud Universty, Nijmegen
	The Netherlands
	pieter@cs.ru.nl
*/

Camil Staps's avatar
Camil Staps committed
14
from StdMaybe import :: Maybe(Nothing)
15
import Gast.GenLibTest 
16 17
from Gast.StdProperty import ::Property // for instance of testable
import Gast.Gen
Camil Staps's avatar
Camil Staps committed
18
from Testing.TestEvents import :: TestLocation, :: CounterExample, :: FailedAssertion
19
from Text.GenPrint import class PrintOutput, :: PrintState, generic gPrint
Bas Lijnse's avatar
Bas Lijnse committed
20 21 22

//--- basics --//

23 24 25
:: Admin =
	{ labels                :: ![String]
	, args                  :: ![String]
26
	, argsRepresentation    :: ![String]
27
	, namePath              :: ![String]
28
	, res                   :: !Result
29 30
	, failedAssertions      :: ![(FailedAssertion, String, String)] //* Failed assertion & string representation of args
	, recFieldValueNrLimits :: !Map (TypeName, RecFieldName) Int    //* Restricts the number of values generated for record fields
31
	}
Bas Lijnse's avatar
Bas Lijnse committed
32
:: Result = Undef | Rej | Pass | OK | CE
33
newAdmin :: Admin
Bas Lijnse's avatar
Bas Lijnse committed
34 35 36 37

derive gLess Result
instance == Result

Camil Staps's avatar
Camil Staps committed
38
:: Property = Prop String (Maybe TestLocation) (GenState Admin -> [Admin])
Bas Lijnse's avatar
Bas Lijnse committed
39 40 41

prop :: a -> Property | Testable a

42
class TestArg a | genShow{|*|}, ggen{|*|}, gPrint{|*|} a
Camil Staps's avatar
Camil Staps committed
43

Camil Staps's avatar
Camil Staps committed
44 45 46
class Testable a
where
	evaluate :: !a GenState !Admin -> [Admin]
Camil Staps's avatar
Camil Staps committed
47
	testname :: a -> String
Bas Lijnse's avatar
Bas Lijnse committed
48

Camil Staps's avatar
Camil Staps committed
49 50
	testlocation :: a -> Maybe TestLocation
	testlocation _ = Nothing
Camil Staps's avatar
Camil Staps committed
51

Bas Lijnse's avatar
Bas Lijnse committed
52 53 54
instance Testable Bool
instance Testable Result
instance Testable Property
55 56
///instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a //TestArg a  
instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a & TestArg a  
Bas Lijnse's avatar
Bas Lijnse committed
57 58 59 60
instance Testable [a] | Testable a  

//derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)

61
MaxExists	:== 1000
Bas Lijnse's avatar
Bas Lijnse committed
62 63 64

//--- for generating lists of elements ---//

65 66
//aStream :: RandomStream
//split :: !RandomStream -> (RandomStream,RandomStream)
Bas Lijnse's avatar
Bas Lijnse committed
67 68 69

//--- for implementation of properties ---//

70
diagonal :: ![[a]] -> [a]
71 72 73 74
forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a
//split :: !RandomStream -> (RandomStream,RandomStream)
//generateAll :: !RandomStream -> [a] | ggen{|*|} a
generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
Bas Lijnse's avatar
Bas Lijnse committed
75 76 77

//--- testing --//

78
:: Testoption
79 80 81 82 83 84
	= Tests      Int
	| Fails      Int
	| Args       Int
	| RandomSeed Int
	| RandomList [Int]
	| Skew       Int
85
	| Bent
86 87
	| MaxDepth   Int
	| ArgTypes   [GenType]
88

89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
/**
 * The combined results of all tests for a single property.
 * This is in contrast to {{Result}} which represents the result of a single test.
 */
:: TestsResult = { maxTests   :: !Int        //* Maximum number of tests
                 , nRej       :: !Int        //* Rejected test arguments
                 , resultType :: !ResultType //* Type of the result
                 }
/**
 * The type of the combined result, together with information
 * specific to that type of result.
 */
:: ResultType = Proof        !Int                 //* Proof by exhaustive testing: nTests
              | PassedTest   !Int !Int !Int !Bool //* Passed test: maxArgs, nTests, nUnd, all possible args generated?
              | CounterExpls !Int !Int !Int       //* Counterexamples found: nTests nUnd nCounterExamples
              | Undefined    !Int                 //* Undefined result: nUnd
              | NoTests      !Int !Int !Int       //* No tests performed: maxArgs nTests nUnd

/**
 * A counter example.
 */
:: CounterExampleRes =
111 112 113 114 115 116
	{ maxTests           :: !Int      //* Maximal number of tests for run in which counter example is found
	, nTests             :: !Int      //* maxTests MINUS number of test at which counter example is found
	, nE                 :: !Int      //* Number of counter example
	, args               :: ![String] //* Arguments used for test (string representation)
	, argsRepresentation :: ![String] //* Arguments used for test ({{`gPrint`}} encoding)
	, name               :: !String   //* Name of property
117
	, failedAssertions   :: ![(FailedAssertion, String, String)] //* Failed assertions leading to counter example & string representation of arguments
118 119 120
	}

:: GastEvent
Camil Staps's avatar
Camil Staps committed
121 122
	= GE_TestStarted !(Maybe TestLocation) !String
	| GE_TestFinished !(Maybe TestLocation) !String !TestsResult ![CounterExampleRes] ![(String,Int)]
Camil Staps's avatar
Camil Staps committed
123 124
	| GE_CounterExample !CounterExampleRes
	| GE_Tick !Int !Admin
125

126 127 128 129 130 131 132 133 134 135
:: PrintOption
	= Verbose
	| Trace
	| Concise Int //* The Int tells how often a test count should be displayed
	| Quiet
	| OutputTestEvents //* output test results as event specified in clean-platform {{Testing.TestEvents}}

:: PrintConfig =
	{ everyOutput          :: Int Admin -> String
	, counterExampleOutput :: CounterExampleRes -> String
Camil Staps's avatar
Camil Staps committed
136 137
	, beforeStartOutput    :: (Maybe TestLocation) String -> String
	, resultOutput         :: (Maybe TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
138 139 140 141 142 143 144
	}

printEvents :: PrintConfig [GastEvent] -> [String]
toPrintConfig :: ([PrintOption] -> PrintConfig)

Test     :: ![Testoption] !p   -> [GastEvent] | Testable p
TestList :: ![Testoption] ![p] -> [GastEvent] | Testable p
145

146 147 148 149 150 151 152 153 154
verbose     ::      !RandomStream !p -> [String] | Testable p
verbosen    :: !Int !RandomStream !p -> [String] | Testable p
concise     ::      !RandomStream !p -> [String] | Testable p
concisen    :: !Int !RandomStream !p -> [String] | Testable p
quiet       ::      !RandomStream !p -> [String] | Testable p
quietn      :: !Int !RandomStream !p -> [String] | Testable p
quietnm     :: !Int !Int !RandomStream !p -> [String] | Testable p
testEvents  ::      !RandomStream !p -> [String] | Testable p
testEventsn :: !Int !RandomStream !p -> [String] | Testable p
Bas Lijnse's avatar
Bas Lijnse committed
155

156
test :: !p -> [String] | Testable p              // test p 1000 times
Bas Lijnse's avatar
Bas Lijnse committed
157 158 159 160
testn :: !Int !p -> [String] | Testable p        // maxnumber of tests
ttestn :: !Int !p -> [String] | Testable p       // maxnumber of tests, trace all arguments
testnm :: !Int !Int !p -> [String] | Testable p  // maxnumber of tests, max number of errors
ttestnm :: !Int !Int !p -> [String] | Testable p // maxnumber of tests, max number of errors