# Static Analysis of Logic Programs (October 2007)

Accompanying the paper *A Proof-Theoretic Approach to the Static
Analysis of Logic Programs* by Dale Miller is a simple
λProlog implementation of the underlying static analysis
algorithm (deduction in linear logic). This implementation is mean to
be simplistic so that the structure of procedures remains clear. This
code will compile and execute directly on the Teyjus implementation of
λProlog. Below are the main source files for this
implementation.

Linear logic connectives.
Some predicates for basic manipulations of linear logic formulas.

Constants that are used to represent Horn clause program.

Printing routines for formulas and programs.

The multiplicative prover is now working on some tests. In order to
stop the prover from cycling with symmetric assumptions (as in the
case for equivalences o-o), I simply deleted a rewrite rule each
time it was selected. This is a probable loss of completeness that
I should check more carefully.

The harness for the two programs above. This is the main module.

## A Makefile and two executables

A Makefile can be used to call the Teyjus
compiler `tjcc`

The Teyjus bytecode intepreter `tjsim` can be called
interactively of via a couple different executable scripts:` mprove` will apply the `mcheck` predicate to
the argument given at the unix command line. For example,

% mprove lists

will apply the multiplicative prover on the clauses and invariances in
the file `lists.hc`. This executable also makes sure that the
top-level predicates are compiled. Similarly, the `aprove` calls the additive prover instead.
## Some Horn clause programs

Example Horn clause programs put into files using the `.hc`
extension. Since I have not written a parser, we need to enter
abstract syntax directly (using lambda Prolog's concrete syntax in a
direct fashion). The `.txt` files are the result of running
the `mprove` command on the associated `.hc` file.

- btcounting.hc, btcounting.txt
- Height approximations of binary trees used with sorting.
- btrees.hc, btrees.txt
- Multiset approximations of binary trees used with sorting.
- counting.hc, counting.txt
- Some examples of using multisets to prove some simple arithmetic invariants.
- length.hc, length.txt
- Show that the length of a list is the length of a list (using multisets).
- lists.hc, lists.txt
- Some simple list manipulation predicates.
- sort.hc, sort.txt
- Sort specification without keeping duplicates.