Declaring regular types

Defining properties

Given the classes of assertions in the Ciao assertion language, there are two fundamental classes of properties. Properties used in assertions which refer to execution states (i.e., calls/1, success/1, and the like) are called properties of execution states. Properties used in assertions related to computations (i.e., comp/1) are called properties of computations. Different considerations apply when writing a property of the former or of the latter kind.

Consider a definition of the predicate string_concat/3 which concatenates two character strings (represented as lists of ASCII codes):

string_concat([],L,L).
string_concat([X|Xs],L,[X|NL]):- string_concat(Xs,L,NL).

Assume that we would like to state in an assertion that each argument “is a list of integers.” However, we must decide which one of the following two possibilities we mean exactly: “the argument is instantiated to a list of integers” (let us call this property instantiated_to_intlist/1), or “if any part of the argument is instantiated, this instantiation must be compatible with the argument being a list of integers” (we will call this property compatible_with_intlist/1). For example, instantiated_to_intlist/1 should be true for the terms [] and [1,2], but should not for X, [a,2], and [X,2]. In turn, compatible_with_intlist/1 should be true for [], X, [1,2], and [X,2], but should not be for [X|1], [a,2], and 1. We refer to properties such as instantiated_to_intlist/1 above as instantiation properties and to those such as compatible_with_intlist/1 as compatibility properties (corresponding to the traditional notions of “instantiation types” and “compatibility types”).

It turns out that both of these notions are quite useful in practice. In the example above, we probably would like to use compatible_with_intlist/1 to state that on success of string_concat/3 all three argument must be compatible with lists of integers in an assertion like:

:- success string_concat(A,B,C) => ( compatible_with_intlist(A),
                                     compatible_with_intlist(B),
                                     compatible_with_intlist(C) ).

With this assertion, no error will be flagged for a call to string_concat/3 such as string_concat([20],L,R), which on success produces the resulting atom string_concat([20],L,[20|L]), but a call string_concat([],a,R) would indeed flag an error.

On the other hand, and assuming that we are running on a Prolog system, we would probably like to use instantiated_to_intlist/1 for sumlist/2 as follows:

:- calls sumlist(L,N) : instantiated_to_intlist(L).

sumlist([],0).
sumlist([X|R],S) :- sumlist(R,PS), S is PS+X.

to describe the type of calls for which the program has been designed, i.e., those in which the first argument of sumlist/2 is indeed a list of integers.

The property instantiated_to_intlist/1 might be written as in the following (Prolog) definition:

:- prop instantiated_to_intlist/1.

instantiated_to_intlist(X) :- 
       nonvar(X), instantiated_to_intlist_aux(X).

instantiated_to_intlist_aux([]).
instantiated_to_intlist_aux([X|T]) :-
       integer(X), instantiated_to_intlist(T).

(Recall that the Prolog builtin integer/1 itself implements an instantiation check, failing if called with a variable as the argument.)

The property compatible_with_intlist/1 might in turn be written as follows (also in Prolog):

:- prop compatible_with_intlist/1.

compatible_with_intlist(X) :- var(X).
compatible_with_intlist(X) :- 
       nonvar(X), compatible_with_intlist_aux(X).

compatible_with_intlist_aux([]).
compatible_with_intlist_aux([X|T]) :-
       int_compat(X), compatible_with_intlist(T).

int_compat(X) :- var(X).
int_compat(X) :- nonvar(X), integer(X).

Note that these predicates meet the criteria for being properties and thus the prop/1 declaration is correct.

Ensuring that a property meets the criteria for “not affecting the computation” can sometimes make its coding somewhat tedious. In some ways, one would like to be able to write simply:

intlist([]).
intlist([X|R]) :- int(X), intlist(R).

(Incidentally, note that the above definition, provided that it suits the requirements for being a property and that int/1 is a regular type, meets the criteria for being a regular type. Thus, it could be declared :- regtype intlist/1.)

But note that (independently of the definition of int/1) the definition above is not the correct instantiation check, since it would succeed for a call such as intlist(X). In fact, it is not strictly correct as a compatibility property either, because, while it would fail or succeed as expected, it would perform instantiations (e.g., if called with intlist(X) it would bind X to []). In practice, it is convenient to provide some run-time support to aid in this task.

The run-time support of the Ciao system (see Run-time checking of assertions) ensures that the execution of properties is performed in such a way that properties written as above can be used directly as instantiation checks. Thus, writing:

:- calls sumlist(L,N) : intlist(L).

has the desired effect. Also, the same properties can often be used as compatibility checks by writing them in the assertions as compat(Property) (basic_props:compat/1). Thus, writing:

:- success string_concat(A,B,C) => ( compat(intlist(A)),
                                     compat(intlist(B)),
                                     compat(intlist(C)) ).

also has the desired effect.

As a general rule, the properties that can be used directly for checking for compatibility should be downwards closed, i.e., once they hold they will keep on holding in every state accessible in forwards execution. There are certain predicates which are inherently instantiation checks and should not be used as compatibility properties nor appear in the definition of a property that is to be used with compat. Examples of such predicates (for Prolog) are ==, ground, nonvar, integer, atom, >, etc. as they require a certain instantiation degree of their arguments in order to succeed.

In contrast with properties of execution states, properties of computations refer to the entire execution of the call(s) that the assertion relates to. One such property is, for example, not_fail/1 (note that although it has been used as in :- comp append(Xs,Ys,Zs) + not_fail, it is in fact read as not_fail(append(Xs,Ys,Zs)); see assertions_props:complex_goal_property/1). For this property, which should be interpreted as “execution of the predicate either succeeds at least once or loops,” we can use the following predicate not_fail/1 for run-time checking:

not_fail(Goal):-
      if( call(Goal),
          true,            %% then
          warning(Goal) ). %% else

where the warning/1 (library) predicate simply prints a warning message.

In this simple case, implementation of the predicate is not very difficult using the (non-standard) if/3 builtin predicate present in many Prolog systems.

However, it is not so easy to code predicates which check other properties of the computation and we may in general need to program a meta-interpreter for this purpose.

Usage and interface

Documentation on new declarations

p(x, v_1, ..., v_n)  :- body_1, ..., body_k.