Project description

by Fraser

Apropos is a set of tools for generating property tests from a logical model of behaviour.

Apropos generates these tests by enrichment of of an underlying type. The enrichment is a logical model that partitions the space of inhabitants of the underlying type. A property test is generated for each partition.

e.g. In the Int example we enrich the Int type such that it can be described by formulae such as IsSmall :&&: IsPositive. This description corresponds to a partition and a corresponding property. We use a SAT solver to enumerate all solutions to a logical model and define the partitions.

The focus when developing an Apropos specification is not on individual test cases but on a holistic model consisting of properties that enrich an underlying type, their relation to the underlying type, and a random generator that can generate an inhabitant of underlying type that satisfies a given set of properties.

Generating property tests from a model has advantages over writing them by hand.

• From the specifications in the examples directory we generate 1329 tests and the suite passes in 31.19s
• The line count for all of the examples files is 1088 which is less than the number of tests generated.
• Additionally we can be sure that there are no missing property tests since the tests are created by exhaustive search.
• Writing 1329 property tests by hand and auditing them to be sure that none are missing would be a tedious effort - we can automate this with Apropos.
• We gain additional confidence in our tests from the fact that we can reflixively "self-check" our random generator against our properties. This allows Apropos to be used as a way of creating specifications for code before code is written.

Apropos provides tools for aiding construction of parameterised random generators

• PermutationGenerator can construct a ParameterisedGenerator from a set of random Morphisms between partitions

Apropos provides meta-programming abstractions for model composition

• Logical Models can be embedded
• PermutationGenerator Morphisms can be abstracted to construct graphs for embedded models