This zip file contains a complete {log} system (version 4.9.9 release 2d) plus examples 
or tests showing how {log} can be used to solve problems involving arrays.


SOFTWARE REQUIREMENTS

In order to run {log} and the examples, you first need to install the SWI-Prolog 
interpreter:

https://www.swi-prolog.org/


CONTENT

* The {log} system (version 4.9.9 release 2d)

setlog-man.pdf
setlog.pl
setlog_help.pl
setlog_rules.pl
setlog_tc.pl
setlog_ttf.pl
setlog_vcg.pl
ttf_sp.pl


* The examples

arraylib.slog  - {log} library containing several predicates to work with arrays
array-run.pl   - SWI-Prolog code to run the examples
array-tests.pl - Verification conditions (VC) that make part of the examples.
                 Before giving the VCs we give an imperative program written in
                 pseudo-code annotated with pre-conditions, invariants and post-
                 conditions. Then, we give the necessary VCs to prove the
                 program verifies the post-condition if it executed from a state
                 where the pre-condition holds. Each VC is preceded with a short
                 comment describing what is it about and the expected result
                 (sat or unsat).


RUN THE EXAMPLES

To run the examples, open a terminal, go to the directory where {log} has been
installed and do the following:

$ swipl                            // execute the SWI-Prolog interpreter
?- consult('array-run.pl').        // consult the program to run the examples

array-run.pl will load {log} and the examples and will execute them one by one.
For the VCs it will output a list of the form:

vc:result:time

where vc is the identifier for the VC; result is sat or unsat; and time is the
execution time needed to discharge the VC.

Then, array-run.pl will generate 4 test cases from 4 test conditions. In this 
case, the test condition and the resulting test case is printed.






