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.

print.sig, print.mod

Printing routines for formulas and programs.

prover.sig, prover.mod

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.

tl.sig, tl.mod

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.