Statistical
checks: check
hypothesized distribution
•Probability
of no zeroes (to show x ¹ 0) for v values of x in range of size r
•Range
limits (e.g., x £22)
–same
number of samples as neighbors (uniform)
–more
samples than neighbors (clipped)
Statistical test
over hypothesized distribution (are the hypothesized distributions
meaningful?)
Much of the tool can
be viewed as tests of hypothesized distributions.
x 0: say range is
from -r/2 to r/2 (approximately); assumes uniform distribution.
[The hypothesized
distribution is always:the uniform
distribution.Don’t say that early in
the slide, only mention uniform distribution when discussing range limit
test.]
Recall that this is
over multiple tests in a test suite, not a single test.
There is a test
like this for every invariant.
This indicates the
value of reporting the invariant, it is not a statistical test of the
probability that it is really true over all possible executions.
This solves much of
the problem, but some such undesirable invariants remain.