Coverage checking

Coverage checking is used to describe two analyses that STELF 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:

%sort nat %.
%term z nat %.
%term s %pi 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.

%sort half {_ nat} {_ nat} %.
%mode half %in %out %.
%term half/z half z z %.
%term half/s %pi (half (s (s N)) (s M)) %<- (half N M) %.
%worlds () (half _ _) %.

%total N (half N _).

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 STELF 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:

%sort half {_ nat} {_ nat} %.
%mode half %in %out %.
%term half/z half z z %.
%term half/1 %pi (half (s z) z) %<- (half z z) %.
%term half/s %pi (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 STELF is not capable of verifying this and complains accordingly.

%total N (half N _).

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

%term half/1 half (s z) z %.

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

%term half/1 %pi (half (s z) N) %<- (half z N) %.

The full working example with the first approach looks like this:

%sort half {_ nat} {_ nat} %.
%mode half %in %out %.
%term half/z half z z %.
%term half/1 half (s z) z %.
%term half/s %pi (half (s (s N)) (s M)) %<- (half N M) %.
%worlds () (half _ _) %.

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

• Coverage (guide §9.52)
• Output freeness
• Debugging coverage errors
• Output factoring