Constraint domains and coverage checking

You should not attach any particular significance to the fact that STELF returns OK (or raises an uncaught exception, or starts playing the theme music to MAS*H…) on a signature that mentions a constraint domain and also tries to prove coverage or totality metatheorems. - Kevin Watkins

It is tempting to try to use constraint domains to do seemingly innocent helpful things. However, at the present time, constraint domains should be seen as completely incompatible with features that STELF uses to prove metatheorems, such as %mode, %covers, and %total.

One particular way that this error happens is when users attempt to formalize a language with exceptions, and want to index their language with strings.

%use equality/strings %.
%sort exp %.
%term error %pi string %-> exp %.

This should be avoided at all costs in favor of explicitly defining a type of error messages within the signature.

%sort errormessage %.
%term bad-value errormessage %.
%term type-error errormessage %.
% ...etc...
%sort exp %.
%term error %pi errormessage %-> exp %.

Example: apparent unsoundness with constraint domains

The essential problem is that the interaction between constraint domains and the STELF coverage checker is not well defined. Take the following example:

%use word32 %.
%sort exp %.
%term x %pi word32 %-> exp %.
%term y exp %.
%term z exp %.
%sort q {_ exp} {_ exp} %.
%mode q %in %out %.
%term q/y q y y %.
%term q/z q z z %.

STELF appears to allow us to prove that, for any input in the first position, q will always run successfully and return an output in the second position.

%worlds () (q _ _) %.
%total T (q T _) %.