
Elle - A Verification Environment for ML Programs
=================================================

This is a new release (2.4)  of the source code for Elle, an
experimental verification environment for ML Programs

Elle is so-called because it implements part of the Standard ML
Definition in Isabelle '93. Elle is built  on top of Isabelle's
Zermelo-Fraenkel Set Theory.

System Structure 
================

The rules for both elaboration and evaluation have been implemented for
essentially the pure functional subset F of the Core of SML.

In the spirit of the Definition, elaboration and evaluation are quite
independent of each other.  The code for them lives in Elle-2.4/Elab and
Elle-2.4/Eval. Thus the directory Elle-2.4 contains the following:

	README   	This file 
	Kernel		Common Material for both evaluation & elaboration 	 
                           (includes the concrete syntax for F).
	Eval		The Isabelle source code for evaluation
	Elab		The Isabelle source code for elaboration

How to install Elle
===================

Assuming that Isabelle has been installed, the Makefiles should
work with either Standard ML of New Jersey or PolyML (but they have
only been tested for PolyML Version 2.03). 

The Makefiles use the environment variables ISABELLECOMP and
ISABELLEBIN, which should have already been set to build the Isabelle
system. A further variable, ISABELLELOCALBIN, needs to be set to
specify the destination directory for Elle images.

To install Elle, we first need to build the Kernel, using the Makefile
provided.  This is used by both elaboration and evaluation, and only
needs to be built once. Change directory to Elle-2.4/Kernel, and run
"make" at the Unix prompt. This will write the SML image (or PolyML
database) as the file "KERNEL" to the ISABELLELOCALBIN area.

The next step is to build the theory for evaluation.  Change to the Eval directory and then run "make" to save the EVAL image (or database).

Numerous examples are contained in the test files, Test1.ml to
Test5.ml. These test files can be run in sequence by typing:

	use "Test.ml";

within EVAL. Alternatively, we can run "make test" to go through all
the test files.

The theory for elaboration can be installed in exactly the same way.
 

Reasoning About Programs
========================

The following tactics are available for evaluation (see EvalProver.ml):  

	eval_step_tac  	applies a language rule once
	step_tac  	general single step tactic
	evaluate_tac  	iterated step tactic
	eval_tac	is a general-purpose tactic for proving goals by     
                        depth-first search

Similar functions (elab_step_tac etc) are avilable for elaboration.

Interface Functions
===================

The following functions are used in the test files:

	exp_eval E s	takes a string E representing the environment
			and a string s representing the expression to be
			evaluated, and then attempts to carry out the
			evaluation using eval_tac 


(dec_eval and prog_eval are similar functions, which apply to
declarations and programs).  There are also functions exp_elab,
decl_elab and prog_elab, for elaboration.

There are some boolean reference flags which can be altered to modify
the printing of goals.

(1) Syntax Flag

SML_Syntax.show_full_syntax:

- if this flag is true, then the concrete syntax of F will be printed 
  exactly as entered.  

- if it is false, then:
  var x prints as x
  con c prints as c
  excon e prints as e

(2) Evaluation Flags

Obj.show_full_values:
- if false, values are printed in a more readable form.
Obj.show_envs: 
- if false, environments are not printed.


(3) Elaboration Flags

Obj.show_closures:
- if false, full closures are not printed.
Obj.show_contexts:
- if false, full contexts are not printed.
Obj.show_envs: 
- if false,full  environments are not printed.


=================================================================
=================================================================

A Cant and M A Ozols

Trusted Computer Systems Group
Information Technology Division
Defence Science and Technology Organisation
PO Box 1500
SALISBURY 
South Australia 5108 

(email: cant@itd.dsto.gov.au, maris@itd.dsto.gov.au)
