  
  [1X3 [33X[0;0YFunctionality[133X[101X
  
  
  [1X3.1 [33X[0;0YMethods[133X[101X
  
  [33X[0;0YThis section will describe the methods of QuickCheck[133X
  
  [1X3.1-1 QC_MakeRandomArgument[101X
  
  [33X[1;0Y[29X[2XQC_MakeRandomArgument[102X( [3XObjectDescription[103X, [3XRandomSource[103X, [3Xlimit[103X ) [32X function[133X
  
  [33X[0;0YCreate  a  random  object  as described by [3XObjectDescription[103X of size at most
  [3Xlimit[103X  using  [3XRandomSource[103X.  How [3Xlimit[103X is interpreted will vary depending on
  the type of object.[133X
  
  [1X3.1-2 QC_Check[101X
  
  [33X[1;0Y[29X[2XQC_Check[102X( [3Xarguments[103X, [3Xfunction[103X[, [3Xconfig[103X] ) [32X function[133X
  
  [33X[0;0YRun tests on [3Xfunction[103X with arguments as described in [3Xarguments[103X.[133X
  
  [1X3.1-3 QC_CheckEqual[101X
  
  [33X[1;0Y[29X[2XQC_CheckEqual[102X( [3Xarguments[103X, [3XfunctionL[103X, [3XfunctionR[103X[, [3Xconfig[103X] ) [32X function[133X
  
  [33X[0;0YCheck  that,  given  the  same  list of arguments as described in [3Xarguments[103X,
  functionL and function return the same value.[133X
  
  [1X3.1-4 QC_LastFailure[101X
  
  [33X[1;0Y[29X[2XQC_LastFailure[102X(  ) [32X function[133X
  
  [33X[0;0YReturn  the function called, and arguments given, if the most recent call to
  [10XQC_Check[110X or [10XQC_CheckEqual[110X failed on a particular input.[133X
  
  [33X[0;0YReturns  a  record  containing  [3Xargs[103X (the arguments) and a function [10Xfunc[110X (if
  [10XQC_Check[110X  failed)  or  a  list of functions [10Xfuncs[110X (if [10XQC_CheckEqual[110X failed).
  Returns [9Xfalse[109X otherwise.[133X
  
  [1X3.1-5 QC_RerunLastFailure[101X
  
  [33X[1;0Y[29X[2XQC_RerunLastFailure[102X(  ) [32X function[133X
  
  [33X[0;0YRerun  the  last test which failed, as given by [2XQC_LastFailure[102X ([14X3.1-4[114X). This
  is  most  useful  if  a test in a '.tst' file failed, as this will allow the
  test to enter the break loop. Returns [9Xfail[109X if [2XQC_LastFailure[102X ([14X3.1-4[114X) returns
  [9Xfalse[109X.[133X
  
  [1X3.1-6 QC_SetConfig[101X
  
  [33X[1;0Y[29X[2XQC_SetConfig[102X( [3Xconfig[103X ) [32X function[133X
  
  [33X[0;0YSet  config  options for QuickCheck globally, by passing a record. It is not
  required to set all options.[133X
  
  [33X[0;0YCurrent options are:[133X
  
  [30X    [33X[0;6Y[10Xtests[110X: Number of tests to run (default 500)[133X
  
  [30X    [33X[0;6Y[10Xlimit[110X: The size of the largest object to create (default 9)[133X
  
  [30X    [33X[0;6Y[10Xramp[110X:  Number  of  tests,  including skipped ones, to run at each size
        before increasing it (default 30)[133X
  
  [30X    [33X[0;6Y[10Xseed[110X: Initial random seed (default 1)[133X
  
  [30X    [33X[0;6Y[10XcatchErrors[110X:  If  [9Xtrue[109X,  an  error  in the tested function counts as a
        failure; if [9Xfalse[109X, it enters the break loop (default [9Xtrue[109X)[133X
  
  [1X3.1-7 QC_GetConfig[101X
  
  [33X[1;0Y[29X[2XQC_GetConfig[102X(  ) [32X function[133X
  
  [33X[0;0YGet the current global configuration for QuickCheck, as a record[133X
  
  [1X3.1-8 QC_Skip[101X
  
  [33X[1;0Y[29X[2XQC_Skip[102X [32X global variable[133X
  
  [33X[0;0YA  function  tested  by [2XQC_Check[102X ([14X3.1-2[114X) or [2XQC_CheckEqual[102X ([14X3.1-3[114X) can return
  [10XQC_Skip[110X if its arguments do not satisfy its requirements (for example, if it
  needs  an  intransitive  group,  or  an integer which is not prime). Skipped
  tests  do  not  count  as  failures or towards the number of tests. To avoid
  infinite  loops, if 100 times the requested number of tests are skipped, the
  check stops and returns [9Xfalse[109X.[133X
  
  [1X3.1-9 QC_RegisterFilterGen[101X
  
  [33X[1;0Y[29X[2XQC_RegisterFilterGen[102X( [3Xfilter[103X, [3Xgen[103X ) [32X function[133X
  
  [33X[0;0YRegister  [3Xgen[103X  as  a generator for arguments described by the filter [3Xfilter[103X.
  [3Xgen[103X  is  called  as  [10Xgen(rs, limit)[110X, where [3Xrs[103X is a random source and [3Xlimit[103X a
  positive  integer  bounding the size of the value. It is up to [3Xgen[103X to decide
  how  to  interpret  [3Xlimit[103X. Smaller values of [3Xlimit[103X are used first, so simple
  inputs  are  tested  before complex ones. Values not in [3Xfilter[103X are discarded
  and  regenerated,  with  an  error after 100 attempts. This lets a generator
  serve  a more specific filter, for example an abelian permutation group when
  only a [3Xgen[103X for permutation groups has been installed.[133X
  
  
  [1X3.2 [33X[0;0YArgument descriptions[133X[101X
  
  [33X[0;0YAn  argument description is either a filter with a registered generator (see
  [2XQC_RegisterFilterGen[102X  ([14X3.1-9[114X)),  or a function [10Xgen(rs, limit)[110X. The functions
  below build descriptions from other descriptions.[133X
  
  [1X3.2-1 QC_ListOf[101X
  
  [33X[1;0Y[29X[2XQC_ListOf[102X( [3Xdesc[103X ) [32X function[133X
  
  [33X[0;0YDescribes a list of between 0 and [10Xlimit[110X values described by [3Xdesc[103X.[133X
  
  [4X[32X  Example  [32X[104X
    [4X[25Xgap>[125X [27XQC_Check([QC_ListOf(QC_PairOf(IsPosInt))],[127X[104X
    [4X[25X>[125X [27X            l -> ForAll(l, p -> Length(p) = 2 and ForAll(p, IsPosInt)));[127X[104X
    [4X[28Xtrue[128X[104X
  [4X[32X[104X
  
  [1X3.2-2 QC_FixedLengthListOf[101X
  
  [33X[1;0Y[29X[2XQC_FixedLengthListOf[102X( [3Xdesc[103X, [3Xlen[103X ) [32X function[133X
  
  [33X[0;0YDescribes a list of [3Xlen[103X values described by [3Xdesc[103X.[133X
  
  [1X3.2-3 QC_PairOf[101X
  
  [33X[1;0Y[29X[2XQC_PairOf[102X( [3Xdesc[103X ) [32X function[133X
  
  [33X[0;0YDescribes a list of length two, whose entries are described by [3Xdesc[103X.[133X
  
  [1X3.2-4 QC_SetOf[101X
  
  [33X[1;0Y[29X[2XQC_SetOf[102X( [3Xdesc[103X ) [32X function[133X
  
  [33X[0;0YDescribes a set of between 0 and [10Xlimit[110X values described by [3Xdesc[103X.[133X
  
  [1X3.2-5 QC_ElementOf[101X
  
  [33X[1;0Y[29X[2XQC_ElementOf[102X( [3Xcoll[103X ) [32X function[133X
  
  [33X[0;0YDescribes a random element of the collection [3Xcoll[103X. This ignores [10Xlimit[110X.[133X
  
