Creating Interactive Verification Tutorials

This part describes advanced uses of LPdoc and the Ciao Playground to create and maintain interactive tutorials for analysis and verification using CiaoPP.

These documents require the features provided in the exfilter bundle, which extends LPdoc and the playground with functionality to extract, filter, and compare the output of program analyses, both statically and dynamically.

Non-interactive examples (static content)

Messages and output generated during Ciao compilation or CiaoPP analysis, for a particular code snippet, can be filtered and included in manuals with the following LPdoc command:

@exfilter{Code}{Action, FlagsValues, Filters}.

In order to enable this functionality it is necessary to include this line in the LPdoc document configuration files (e.g., SETTINGS.pl):

load_doc_module := exfilter(exfilter_lpdoc).

This process happens in two phases: first the document is processed to identify the different (compilation, analysis, verification, etc.) tasks, then the ciao-exfilter command needs to be executed to process the tasks and filter the results necessary for the manual. Typically the results are statically committed in the respository, which enables easy detection of regressions.

For instance, consider the app/3 program:

:- module(_,app/3,[assertions]).

:- pred app(Xs, Ys, Zs) : ( list(Xs), list(Ys) ) => list(Zs) .
  
app([],     Ys, Ys).
app([X|Xs], Ys, [X|Zs]) :-
  app(Xs, Ys, Zs).

where the pred assertion indicates how app/3 should be called in this program. We would like to display the part of the analysis output that shows if the assertion has been checked. This fragment can be generated by including in the source file the following code:

@exfilter{app.pl}{V,output=on,filter=check_pred}

This command is composed of the file that we are looking to filter (app.pl), the analysis and the filter options that we want applied (V,output=on,filter=check_pred). The result is:

:- checked calls app(Xs,Ys,Zs)
   : ( list(Xs), list(Ys) ).

:- checked success app(Xs,Ys,Zs)
   : ( list(Xs), list(Ys) )
   => list(Zs).

CiaoPP/filters options

Usage: @exfilter {Code }{Action, FlagsValues, Filters}.

CiaoPP flags and actions

Action must be one of the following:

A : Analyzes the code program.
O : Optimizes the code program.
V : Verifies the assertions of the code program.

FlagsValues is a list of options FlagName=FlagValue where FlagName is a valid CiaoPP flag name. This list is optional and the flags not included in this list will be assumed to take their default value. Check CiaoPP Reference Manual for the different available flags.

Filters

Filters is composed of an option filter=Filter and an optional list of supplementary filters. Filter must be one of the following:

all : keep all data.
tpred : all true (predicate) assertions.
tpred_plus : all true assertions including comp properties.
tpred_regtype : all true assertions and all regtypes.
regtype : only all regtypes definitions.
warnings : all warning messages
error : all error messages.
check_pred : all check assertions, false assertions and checked assertions.
warn_error : all warning and error messages.
test : all tests.

Include these options with one of the filters for more precise results.

name=Pred : results of a specific predicate, with Pred being the predicate.
assertion=[Terms] : assertions that contain a series of terms, where Terms is the list of terms to be matched.
comments=on : If we add this option together with the filter check_pred then the comments of the assertions will be added as well.
absdomain=AD : AD can be types or can be modes. We have to add this option together with filter tpred, tpred_regtype or tpred_plus to obtain the assertions related to the types or modes.

Example Usage

The following are very simple examples of use:

Run analyse on app.pl file with default options and obtain the true assertions related to types:

@exfilter{app.pl}{A,filter=tpred,absdomain=types}

Output result:

:- true pred app(Xs,Ys,Zs)
   : ( list(Xs), list(Ys), term(Zs) )
   => ( list(Xs), list(Ys), list(Zs) ).

Setting a cost domain and extracting the true assertions including comp properties:

@exfilter{app.pl}{A,ana_cost=resources,filter=tpred_plus}

Output result:

:- true pred app(Xs,Ys,Zs)
   : ( list(Xs), list(Ys), term(Zs) )
   => ( list(Xs), list(Ys), list(Zs) )
   + cost(lb,steps,0).

:- true pred app(Xs,Ys,Zs)
   : ( list(Xs), list(Ys), term(Zs) )
   => ( list(Xs), list(Ys), list(Zs) )
   + cost(ub,steps,inf).

Setting a cost domain and extracting the true assertions including comp properties, but only the assertion of the upper bound analysis:

@exfilter{app.pl}{A,ana_cost=resources,assertion=[ub],filter=tpred_plus}

Output result:

:- true pred app(Xs,Ys,Zs)
   : ( list(Xs), list(Ys), term(Zs) )
   => ( list(Xs), list(Ys), list(Zs) )
   + cost(ub,steps,inf).

Interactive examples (dynamic content)

The playground already included specific commands for embedding editable and runnable code in place. The exfilter bundle extends this functionality with additional steps that turns code snippents into exercises. In particular, the analysis and the filtering method are executed directly from the browser.

For example, in this exercise we want the user to correct the singleton variable written in the base case of predicate app/3:

:- module(_,app/3,[assertions]).
%! \begin{code}
app([],     Ys, Yss).
app([X|Xs], Ys, [X|Zs]) :-
  app(Xs, Ys, Zs).   
%! \end{code}
%! \begin{opts}
solution=errors,message=singleton
%! \end{opts}
%! \begin{solution}
app([],     Ys, Ys).
app([X|Xs], Ys, [X|Zs]) :-
  app(Xs, Ys, Zs).

% In our case, we type Yss instead of Ys.
%! \end{solution}

When users submit their answers, the playground will return appropriate feedback showing the error messages related to the singleton variables. We have defined lpdoc-style commands which mark different parts of the program. The playground identifies the different parts and classifies them. For example, the playground will recognize a solution, a set of filters that we want to apply, and the part of the interactive code that will be shown in the documentation. In this case, the solution will be shown only when the Show solution button is clicked. The code part is always visible. Hence, the previous exercise can be generated by including in the source file the following code:

```ciao_runnable
:- module(_,app/3,[assertions]).
%! \begin{code}
app([],     Ys, Yss).
app([X|Xs], Ys, [X|Zs]) :-
  app(Xs, Ys, Zs).   
%! \end{code}
%! \begin{opts}
solution=errors,message=singleton
%! \end{opts}
%! \begin{solution}
app([],     Ys, Ys).
app([X|Xs], Ys, [X|Zs]) :-
  app(Xs, Ys, Zs).

% In our case, we type Yss instead of Ys.
%! \end{solution}
```

Modes of interactive exercises

For the inclusion of exercises in the documentation three distinct modes of exercises have been developed:

solution=equal : Prints out the clauses from the user's answer that do not match with the file that contains the solution. It takes care of trivial differences such as different variable names and different formatting of the code in the files.
solution=errors : Another task is to find bugs in a program and fix them. Users submit their solutions and the filter checks them. If there are none then the program has been corrected successfully. Additionally, a message filter has been created to extract a message or messages by a certain term.
solution=verify_assert : Analysis information allows us to conclude that the program is incorrect or incomplete, i.e., that the program does not satisfy the requirements. The idea is that given the solution of the user, the filter checks if the user's program verifies the assertions (specifications).

Example Usage

Example 1. What is the correct assertion?

%! \begin{code}
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => var(C).

app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).  
%! \end{code}
%! \begin{opts}
solution=verify_assert
%! \end{opts}  
%! \begin{solution}
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => list(C).

app([],Y,Y). 
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).   
%! \end{solution}

It can be generated by including in the source file the following code:

```ciao_runnable
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => var(C).

app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).  
%! \end{code}
%! \begin{opts}
solution=verify_assert
%! \end{opts}  
%! \begin{solution}
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => list(C).

app([],Y,Y). 
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).   
%! \end{solution}
```

Note that you can also generate interactive examples, for example:

%! \begin{code}
:- module(_,app/3,[assertions]).

:- pred app(Xs, Ys, Zs) : ( list(Xs), list(Ys) ) => list(Zs) .
  
app([],     Ys, Ys).
app([X|Xs], Ys, [X|Zs]) :-
  app(Xs, Ys, Zs).
%! \end{code}
%! \begin{opts}
A,ana_det=nfdet,filter=tpred_plus
%! \end{opts}

This block runs analysis on the program with a determinism domain and displays the true assertions including comp properties.