[Prev][Next][Index]

Graphical environment for Larch tools




Dear Larch specifiers:

My students and I have put together something that we call the
Larch Development Environment (LDE) that has greatly facilitated our
construction and use of Larch specifications and their tools. So I thought
I would share it with the group.

In a nutshell, LDE provides:

	- Graphical access to LSL traits, thus enabling a browsing of traits.
	(You can set an environment variable to represent all the directories
	where you have Larch specifications. Then when you run LDE, you have
	access to all of those in a single scrolling list, where the specs
	can be retrieved for editing or for viewing). It's quite handy if
	you have different handbooks spread out among several directories.

	- Expansion/compression of included traits 

	- Ability to look up traits (in separate window) that are included

	- Graphical access to all commands available with the Larch tools:
	sorts, signatures, syntax checking, etc.

	- Graphical access to LP and all of its commands, including graphical
	access to help (with keyword search). There are seperate templates for
	the different types of proofs that you might want to generate.

	- Similar graphical environment for LCL and LCCL specifications.

In addition, in order to create new LSL, LCL, and LCCL specifications, LDE
provides graphical templates, so you don't have to remember the order
or exact syntax of the format of the respective types of specifications.
Templates can only be used for newly created specifications. Your existing
specifications can be edited in a regular text editor. 

We have been using LDE in research as well as in the instructional settings
and it has dramatically improved our productivity with respect to specification
construction and manipulation. I'm sure that there are a few glitches
here and there, and I would like to hear your feedback on its use.

As an ``added'' feature, LDE is available for both SunOS and Solaris (getting
the latter completed was fun :-) Also, it is built with the Motif library.

The source and README for installation for LDE can be (anonymously) ftp'd from:
Included in this package is a user manual.

ftp.cps.msu.edu

under the directory: /pub/serg/tools/LDE/

- LarchBrowser.README
- LarchDevEnv1.2a.tar.gz

Have fun specifying!

Betty


----- End Included Message -----