Michael K. Smith
mksmith@cli.com
Computational Logic, Inc.
1717 West 6th Street, Suite 290
Austin, Texas 78703-4776
The subset of Z that we support includes globals, axioms, schemas and types. We parse generics, but do not yet support generating code from schemas derived from generics.
There are any number of problems translating Z specifications into executable code, th primary one being that decorations on variables are only suggestive. We assume that ?, !, and ' decorations unambiguously refer to input variables, output variables, and post schema variables, respectively.
I have only implemented Z functions as I have needed them. The set comprehension code is suspect, as it was tacked on quickly. The grammar has a large number of shift/reduce conflicts that I haven't bothered to clean up. When loaded there is a function NORMALIZE that is inteded to disambiguate ambigous output. See section [normalize].
To obtain, install and test the system see section [distribution]
The subset of Z that we support includes globals, axioms, schemas, generics and types. We parse generics, but do not yet support generating code from schemas derived from generics.
The types we generate are not identical to Z's because they are constructive. But except in the case of infinities we believe they behave identically. Syntax
type
::= integer | basic_type | ( powerset type ) |
( cross . type*) | ( schema . (name . type)*)
A base type of a type is the fully expanded form, containing
in the leaves nothing other than basic_types and integer.
The documentation of the syntax is rather spotty. The grammar is
provided in section [grammar]. We parse an ascii form of Z that
corresponds to that described for ZTC (see
ftp://ise.cs.depaul.edu/pub/ZTC/). Documentation and tool support for
ZTC are available at
"ftp://ise.cs.depaul.edu/pub/ZTC/".
We have augmented the specification with an initialization section that simplifies the assignment of concrete values. Syntax additions are detailed with the Z subset syntax in Section [initial].
We preprocess text in a ZTC file to a form suitable for parsing. We support "boxed" and "ascii" formats. A % to end of line is always taken to be a comment. In zsl mode lines beginning with anything other than a tab are considered comments.
The default mode is zsl ascii.
This may be set by an initial line of the form:
% [ z | zsl ] [ ascii | boxed | latex ]
The distinction between ``z'' and ``zsl'' input lines is that
the later begin with tabs, other lines being comments.
At the moment, boxed and ascii ZSL input can be mixed and we don't handle latex. See "ZTC: A Type Checker for Z".
The conversion steps taken by the preprocessor are:
Following the specification section, specification ... end specification we support an initialization section in order to create an interesting initial state.
INITIALIZE
MaxCopiesAllowed = 5;
Book = { mobydick, huckfinn, it, dictionary };
DATA BookInfo
about = { mobydick -> { whales, sea },
huckfinn -> { river, mississippi },
it -> { horror },
dictionary -> { words } };
END DATA
DATA LibraryDB
borrower = { bob , ted , carol , alice };
staff = { wayne };
checkedout = { m1, i1 };
borrowedby = { m1 -> bob , i1 -> ted };
END DATA
END INITIALIZE
The syntax of the initialization section is as follows (reserved words
in caps, brackets indicate zero or more repetitions).
Syntaxinitial init [ ; init ] END INITIALIZE
init id = expression | data
data DATA id init [ ; init ] END DATA
The id = expr form can provide a value for a global or a set of possible values for types. Braces indicate sets, -> a mapsto. The id in the data production must be a schema name and the init clauses should reference variables of that schema.
See test/lib.z for a more complete example.
You can invoke the parser in a standalone fashion as follows:
parse input > output
'parse' will take in a Ztc file and produce a file of syntactic s-expressions (lists) representing the program. The parser proper is in the executable 'ztc'. 'parse' first pipes the input through a Perl program ( fixup) to remove text (comments), detect boxes, etc.
pparse input
will pretty print parser output by running it through lisp, using read-print.lisp.
The entry points to EZ are listed in section . Test examples can be seen in section [examples]. Additional examples of the Z input format are contained in files parser/test/*.z and execute/test/*.z.
The function LOADZ invokes the parser and reads in the resulting data, creating a database from which executable functions may be generated.
These forms must remain in synch with parser. Doing (loadz "file.z") or (load "file.lisp") adds to the various global vars as indicated below. LOADZ expects the following forms from the parser:
(base-type-decl . names) Adds to *types*
(free-type name branches) Adds to *types, *constants*, *constructors*
(schema name decls preds) Adds to *schemas*
(gendef name decls preds) Adds to *generics*
(genequiv lhs schema-exp) Adds to *generics*
(schemadef name-args exp) Adds to *schemas* or *generics*
(axiom decls preds) Adds to *axioms*, *globals* and *functions*
See structures.lisp.
The lists below constitute the database. They are all either lists of structures or mappings from name to structure for the corresponding data type.
*types* - basetype additions due to basic-type-decls.
*constants* - basetype additions due to free-types
*globals* - global vars
*axioms* -
*schemas* -
*generics* -
You can create executable Z by following the steps shown in the library-extend.log file.
The NORMALIZE function (in zlisp.lisp) is critical. It cleans up odd constructions that the parser produces. For example,
{ S }
may be a singleton set containing the constant S or a set-comprehension, where S is a schema name. Actually, Spivey's book says the singletom should be entered as {(S)}. Be that as it may, my parser depends on NORMALIZE to figure this out and it is currently pretty ad hoc.
The NIL argument case is not yet implemented. The intention is that TEST will randomly select from the executable functions (choosing arguments as it needs to). I am not sure how useful this would be. Some more elaborate constraining script language would be more useful.
Our basic model of a state is as a collection of schemas that hold variable bindings. A simple schema macro generates a function that takes input variables as arguments and global inputs from schema variables, and produces output variables as well as binding the primed schema variables.
A schema macro that includes input or output variables may generate a transition function that executes the transition. The function will be a multiple-valued function from the set of ? variables and, implicitly, state, to (mv . !variables) and state.
The executable translation depends on the predicates that the variables are constrained by. Suppose x is of type integer. We handle the following cases:
| Predicate form | Action | |
| 1. | x = f(..) | Compute f(..). |
| 2. | P(.. x ..) | x := choose(x, integer, P(.. x ..)) |
| 3. | default | x := choose(x, integer, true) |
The function choose depends on a generator for values of the type of x. We test to see if the generated value satisfies the (optional) predicate. We limit the number of guesses. If exceeded, we ask the user to supply a value.
We do not backtrack between choices. Consider
choose(x!, integer, x! > 0) choose(y!, integer, y! < x! or y! > 2)The first choose will bind x! to 1. The second will fail, because we need x! to be > 3.
When calling a schema function we should save the input/output mapping so that we can provide the same output if called again with the same inputs. We do not curently do this.
input = ?vars & ivars = domain(input) output = !vars & ovars = domain(output) primes = 'vars & pvars = domain(primes) notprimes = all other vars & svars = domain(notprimes) invars = ivars @ svars outvars = ovars @ pvars axioms = axioms of S
From such a schema we generate a function according to the following template:
function S-fn (ivars)
declare(special, ovars @ pvars);
*current-schema* := lookup(S);
Every v in ivars | setv(v, S);
Every v in svars | bind(v, getv(v, S));
Every v in ivars | type-check(v, type(v,input));
Every v in svars | type-check(v, type(v,notprimes));
Every p in axioms s.t. ~mentions(p,ovars @ pvars) | eval(p);
for v in output @ primes,
let fn = choose_function(v, axioms),
do bind(v, eval(fn));
Every v in ovars | setv(v, S);
Every v in pvars | setv(v, S);
Every v in ovars | type-check(v, type(v,output));
Every v in pvars | type-check(v, type(v,primes));
Every p in axioms s.t. mentions(p,ovars @ pvars) | eval(p);
< ovar_1 , ... , ovar_n >
This system comes as a Unix distribution.
To obtain EZ by ftp using Unix or a Unix variant,
Create a directory in which you wish to build the system and move the tar file there.
Untar the distribution by executing
tar xpf ez.tar
This will create subdirectories named `execute' and `parser', which contain the sources and examples, as well as a top level makefile and README.
We assume you are running Unix with versions of sed, Perl and the following GNU tools - Bison, Flex, GCC \ & GCL. C compilers other than GCC are possible but we haven't tried them. We use GCL for our Common Lisp and have not experimented with other Lisp implementations.
If you use something other than GNU Common Lisp you may need to check the semantics of DEFSTRUCT as used in execute/structures.lisp. You will definitely need to modify the top level makefile setting for lisp:
LISP = gcl
We assume that a Perl executable is located in /usr/local/bin/perl. If not, edit the first line of parser/fixup
To build the system, execute
makeThe following files may be of some interest.
execution/zlisp.lisp callse parser and generates executable.
parser/ztc-gram.y is the grammar.
parser/ztc-lex.l is the scanner definition.
parser/fixup performs the preprocessing.
Most of the .c files in the parser directory are support for the structure building that the parser does.
The file ``addstart'' is not neccessary unless you wish to create a parser that will parse one unit at a time.
make tests
To determine whether everything is working you will need to look at the output. The parser tests will show up as
Making tests in parser
doalltest .
test/free-type.z
test/lib.z
test/library.z
test/test.z
...
If parse errors are encountered (there should be none) they will be printed to your terminal as
;; *** parse error at end on line 73
;Skipping to next form from line 74.
The next set of tests are of the generation of executable forms. Search your output for strings that begin "Parsing and generating". You should find lines of the form:
Parsing and generating executable for ./test/lib.z.
(RETURN-FN CHECKOUTCOPY-FN LIBRARYSTATE'-FN LIBRARYDB'-FN
BOOKINFO'-FN LIBRARYSTATE-FN LIBRARYDB-FN BOOKINFO-FN)
The list following the "Parsing and generating" line is a list of
functions defined from the input Z specification in the execute/test/
subdirectory. No errors should be encountered.
See the log in execute/library-extended.log Change to directory execute/, start lisp and follow the script below.
% cd execute % gcl >(load "zlisp.o") .. >(in-package "Z") .. Z>(check-install) ..CHECK-INSTALL runs 3 operations in the library model from test/lib.z.
It first clears the database (reset), loads test/lib.z (loadz "test/lib.z"), generates executable functions (generate-executable) and then runs TEST on three operations:
(test (return-fn 'm1) (checkoutcopy-fn 'bob 'i2)(return-fn 'i2)))
I have extended the ZTC syntax to provide initial bindings (see section [syntaxaddition]). TEST will print out the schema bindings after each operation. Between operations, TEST calls the function STEP, which updates all of the paired variable and variable' bindings. That is:
x := x' & x' := unset