LETOS -- A Lightweight Execution Tool for Operational Semantics

Pieter H. Hartel, Univ. of Southampton, May 1999

A lightweight tool is proposed to aid in the development of operational semantics. To use letos, an operational semantics must be expressed in its meta-language, which itself is a superset of Miranda. The letos compiler is smaller than comparable tools, yet letos is powerful enough to support publication quality rendering using LaTeX, fast enough to provide competitive execution and tracing using Miranda or Haskell, and versatile enough to support derivation tree browsing using Netscape. Letos has been applied to a Java Secure Processor, which is a version of the Java Virtual Machine intended to run on smart cards. Letos has also been used with subsets of various programming languages. Letos is unique in that it helps to check that a specification is operationally conservative.

The latest version of letos is described in detail in a paper, which is included with the program and some sample inputs in a gzipped tar file.

An older version of letos (called latos) is described in a technical report DSSE-TR-97-1, published by the Declarative Systems & Software Engineering Group Department of Electronics and Computer Science University of Southampton. technical report .

The paper referred to above provides a fairly abstract description of letos, the present web page describes some of the details that are necessary to actually use letos. The paper should be read first.

Command line arguments

Letos reads the input from stdin and writes the output to stdout. By default a Miranda program is generated without debug or trace. Syntax error messages are written to stderr.

Only one of [-c|-m|-l|-p] must be selected.

-c: Check source dependency and issue warnings to stdout.
-m: Generate a Miranda program on stdout.
-l: Generate a LaTeX document on stdout.
-p: Dump the parse tree to stdout.

Select one of [-d|-dd] or neither.

-d: Debugging mode, causes creation of parse tree nodes to be displayed.
-dd: This selects -d and also causes the yacc generated parser to trace its actions.

Select one of [-t|-tt|-ttt] or neither.

-t: Add calls to parameterless uniform tracing functions in the generated Miranda. These functions display only the name of the rules.
-tt: More detailed trace, giving access to the parameters of the rules being traced. In this case the same function is used for all rules/axioms making up a realtion.
-ttt: As above, but a separate function is used for each rule or axiom.

Files

The distribution consists of the following files:

Sources and make script:

letos.l: lex and C source.
letos.y: yacc and C source. This file contains the main ( ).
make.sh: A shell script to compile and test letos.

Support files for Miranda and LaTeX:

support.m: letos support for the generated Miranda.
support.tex: letos support for the generated LaTeX.
a4paper.tex: Ensure that the LaTeX output makes good use of A4 paper.

Test input:

while.os: The sos, ns, ds and am semantics of While.
mf.os: The ns for Mini-Freija, a functional language.
cycle.os: A short test for mutual recursive hypotheses.
bpa.os: A fragment of CCS.
bpa.os: A fragment of basic process algebra.
lambda.os: A type checker for Chruch' simply typed lambda-calculus
success.os: A series of slides explaining how backtracking logic programs can be translated into lazy functional programs.
trans.os: Translation of patterns into conditionals.

Compiling and testing

The shell script make.sh calls lex, yacc and the gcc compiler to create the letos binary. The script then runs letos, LaTeX and Miranda on the *.os files. This has only been tried on Suns, under SunOS and under Solaris.

The script generates various kinds of error messages, none of which are serious.

Yacc complains about 63 shift/reduce and 50 reduce/reduce conflicts.
On some systems the C compiler reports warning: assignment makes pointer from integer without a cast in two places in letos.l.
The test inputs that generate slides draw LaTeX warnings about font sizes not being available. The effect is not visible in the postscript.
Some tests cause LaTeX to complain about overfull hboxes.
Some of the tests draw warnings from Miranda, about unused local definitions.

Browsing derivation trees.

To browse a derivation tree, it should first be generated. Three levels of detail can be chosen. If specific information about the rules being processed (other than the name of the rule) should be rendered then specific trace functions must be provided. A good example may be found in the semantics of while. Once the trace has been generated by the Miranda program (which itself is generated by letos), the trace should be textually included in a bookmarks file.

A brief note on the implementation

Letos is nearly a functional program. It uses lex and yacc to build up a parse tree for each separate input unit (that is a sequence of lines between .MS and .ME). The unit is then processed using a fairly general mechanism of pattern matching. Patterns are built up from the same nodes as the parse tree, with additional nodes to effect bindings. Wild cards are also possible in case any sub-tree may be matched. The function letos.y:match() does the actual matching.

Everything else is fairly straightforward, although quite messy at times, in particular when generating appropriate where clauses to support premises for the rules.

Bugs

Letos generates only one kind of error message: syntax error at line ...

The source dependency check does not know about the identifiers in the Miranda prelude, the support file and any other imported files. It errs on the side of caution.

The control over the layout in the generated LaTeX is primitive. Any expression can be adorned with identity functions with conspicuous names, such as \nltabtabid (see while.os), but the non-expression parts of the input language cannot be treated in this way. Currently it is possible to obtain a newline after the turn style symbol and after the vertical bars separating alternatives in the definition of an algebraic data type.

The translation of rules and axioms into Miranda is combined with the printing of the Miranda. This should have been separated so that it would be easier to generate code in another lazy functional language.

Letos has space leaks in the sense that parts of the parse tree that have become redundant during translations of rules and axioms are never reclaimed. Patterns are always reclaimed.

Letos restricts the number of type variables to four, but this can easily be increased.

An n-ary distfix construction should perhaps give rise to an n-ary LaTeX macro. Presently a separate macro is used for each of the constructors in the distfix-construction.

Letos relies on Miranda and LaTeX to detect most errors. The line numbers reported by these programs bear no relationship to the source line numbers in the letos document. Original letos input line numbers are embedded in the generated Miranda and LaTeX as comments.

Detailed traces and explicilty typed rules and axioms are incompatible because the addition of tracing changed the type of rules and axioms. The solution is to comment out any explict types on rules and axioms.