Coverage checking

From The Twelf Project
Jump to: navigation, search

Coverage checking is used to describe two analyses that Twelf needs to perform in order to verify totality assertions.

The first analysis, for input coverage, is performed by both %total and %covers declarations and resembles exhaustiveness checking in a language like ML.

The second analysis, output coverage, is performed only by %total to ensure that the outputs of subgoals are sufficiently general. Output coverage consists of a check for incorrect constant pattern-matching and a check for output freeness violations.

We will use the common example of natural numbers for this example:

nat: type.

z: nat.
s: nat -> nat.

Input coverage

Input coverage is similar to exhaustiveness checking in ML, in that it ensures that your relation is prepared to accept any input that is thrown at it. We would run afoul of the input coverage checker if we tried to run a %covers or %total declaration on the relation half that halves a natural number but is undefined on odd numbers. Another example of input coverage checking can be seen at the page on %covers.

half : nat -> nat -> type.
%mode half +N1 -N2. 

half/z : half z z.
half/s : half (s (s N)) (s M)
          <- half N M.

%worlds () (half _ _).
%total N (half N _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Coverage error --- missing cases: {X1:nat} |- half (s z) X1.

%% ABORT %%

Output coverage

Output coverage ensures that your relation is prepared to deal with any possible term that it might be output by a subgoal. Output coverage does not have quite so obvious a counterpart in functional languages like ML; the reason is that Twelf differentiates between case-analyzing outputs and case-analyzing inputs, whereas in ML there is just one case construct.

Output constant pattern-matching

Say we attempted to fix half by defining half of 1 to be 0 by adding the case half/1 shown below:

half : nat -> nat -> type.
%mode half +N1 -N2.

half/z : half z z.
half/1 : half (s z) z
          <- half z z.
half/s : half (s (s N)) (s M)
          <- half N M.

%worlds () (half _ _).

For pedagogical purposes, we have given the constant half/1 an unnecessary extra premise that half z z . Thus, the case half/1 expects the "output" of the subgoal <- half z z to be z; inspecting the program, this is a true fact, but Twelf is not capable of verifying this and complains accordingly.

%total N (half N _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Totality: Output of subgoal not covered Output coverage error --- missing cases: {X1:nat} |- half z (s X1).

%% ABORT %%

In this case, we can fix the problem in one of two ways. First, we can remove the subgoal entirely:

half/1 : half (s z) z.

Alternatively, we can rewrite the subgoal, leaving the output a free variable:

half/1 : half (s z) N
          <- half z N.

In many circumstances when the output coverage checker rejects a totality assertion that should, in fact, be true, a standard technique output factoring can deal with the problem.

Output freeness

The other part of output coverage checking is output freeness checking; see its page for a definition and examples.

See also