synrels@GVAX.CS.CORNELL.EDU (Tim Teitelbaum) (05/22/87)
[Forwarded from the Stanford bboard by Laws@STRIPE.SRI.COM.]
Introducing the Synthesizer Generator:
a tool for creating editors
Thomas Reps Tim Teitelbaum
Computer Science Department Computer Science Department
University of Wisconsin Cornell University
Madison, WI 53706 Ithaca, NY 14853
1. What is the Synthesizer Generator
The Synthesizer Generator is a tool for creating editing
environments for complex objects. The editor designer
prepares a specification that includes rules defining a
language's abstract syntax, context-sensitive relationships,
display format, and concrete input syntax. From this
specification, the Generator creates a full-screen editor
for manipulating objects according to these rules.
2. Who might want to use the Synthesizer Generator?
The Synthesizer Generator can be used by researchers who
need to construct an editing environment for objects that
can be described by a grammar. The Generator has been suc-
cessfully used to create a Pascal editor with full static
semantic checking, editors for C and Fortran 77, and many
editors for program verification and proof editing. It has
also been used to construct WYSIWYG editors for right-
justified text and mathematical formulae.
Using the Synthesizer Generator is much faster than
producing a hand-crafted editor, just as using a compiler
compiler is faster than writing a compiler. The Generator
maintains abstract representations for objects and incor-
porates algorithms for propagating context-sensitive infor-
mation through the objects being manipulated. It also pro-
vides the many mundane features that any editor must have,
such as binding of key sequences to generic commands, creat-
ing and manipulating buffers for edited objects, multiple
windows, etc., that would otherwise distract the editor
designer from his primary interest. The relative ease of
generating editors makes the Generator ideal for prototype
development and experimental use.
3. Are there serious applications beyond program editors?
Applications of the Synthesizer Generator are not limited to
editors for programming languages. At Cornell the Generator
is being used to implement environments for formal reasoning
that allow users to interactively construct proofs. Proofs
are represented as trees whose nodes correspond to inference
rules, while proof correctness is represented by context-
sensitive constraints between the nodes of the tree. Two
approaches to building such environments have been investi-
gated: in one the environment designer hand-tailors a Syn-
thesizer specification for a particular formal system [Reps
and Alpern]; in the other, the Synthesizer Generator is used
to implement an environment for defining formal systems that
allows a user to interactively define a particular logic and
to conduct formal reasoning in that logic.
[Reps and Alpern] Reps. T. and Alpern, B. "Interactive Proof
Checking," Eleventh POPL, 1984, 36-45.
4. How does it work?
The Synthesizer Generator is particularly well suited for
creating editors that enforce the syntax and static seman-
tics of objects that can be described in a particular
language. Each object to be edited is represented as a con-
sistently attributed derivation tree. When these objects
are modified, some of the attributes may no longer have con-
sistent values; incremental analysis is performed by updat-
ing attribute values throughout the tree in response to
modifications. If an editing operation modifies an object
in such a way that context-dependent constraints are
violated, the attributes that indicate satisfaction of con-
straints will receive new values; thus, these attributes can
be used to annotate the display in order to provide the user
with feedback about the existence of errors.
Editor specifications are written in the Synthesizer
Specification Language (SSL), which is based on the concepts
of a term algebra and an attribute grammar, although certain
features are tailored to the application domain of
language-based editors.
The Synthesizer Generator has two components:
a) a translator that takes an SSL specification as input,
and produces grammar tables as output, and
b) an editor kernel that consists of an attributed-tree
data-type and a driver for interactively manipulating
attributed trees; the kernel takes input from the key-
board and executes appropriate operations on the
current tree.
A shell program handles the details of invoking the transla-
tor and producing a language-based editor from the resulting
tables.
5. How to get a copy of the Generator
The Generator is written in C and runs under Berkeley UNIX
on VAX computers, Sun workstations (using SunWindows), and
the IBM PC/RT. Porting to other versions of UNIX is
straightforward. We are in the process of porting the Gen-
erator to XWindows. Editors generated with the Synthesizer
Generator will work on any crt terminal described in the
UNIX termcap database. A keyboard description file speci-
fies the layout of special function keys used by the gen-
erated editors. The distribution, which is available for
$200.00, consists of:
a) Source and object code for the SSL translator and edi-
tor kernel.
b) A collection of demonstration editors and their specif-
ications, including a Pascal editor with full static-
semantic checking and several proof editors.
c) A copy of The Synthesizer Generator Reference Manual.
6. References
The Synthesizer Specification Language is described in:
Reps, T. and Teitelbaum, T. The Synthesizer Genera-
tor. In Proceedings of the ACM SIGSOFT/SIGPLAN
Software Engineering Symposium on Practical Software
Development Environments, Pittsburgh, Penn., Apr.
23-25, 1984. (Appeared as joint issue: SIGPLAN No-
tices (ACM) 19, 5 (May 1984), and Soft. Eng. Notes
(ACM) 9, 3 (May 1984), 42-48).
A complete manual is available:
Reps, T. and Teitelbaum, T. The Synthesizer Genera-
tor Reference Manual. Department of Computer Sci-
ence, Cornell University, Ithaca, NY, 14853, August,
1985.
A description of the theory underlying the Generator may be
found in:
Reps, Thomas W. Generating Language-Based Environ-
ments, The MIT Press, 1984.
To request further information about acquiring a copy of the
system, please respond with the name of your organization and
your postal address to
ARPA: synrels@gvax.cs.cornell.edu
UUCP: {rochester, allegra}!cornell!synrels
Bitnet: synrels@crnlcs.Bitnet
USMail: Prof. Tim Teitelbaum
Synthesizer Generator Distribution
Dep't of Computer Science, Upson Hall
Cornell University
Ithaca, NY 14853
USA
We will send you the terms of the distribution and copies
of the distribution agreement.
-----
-------