You will need to get the LSL checker, so that the Larch/C++ tools can check on any traits you specify. It can be obtained by anonymous ftp from the following URL.
ftp://larch.lcs.mit.edu/pub/Larch/
Get the `LSL-README.new' file in that directory for detailed instructions.
After you install LSL, some steps have to be taken to ensure that everyone using both Larch/C++ and LSL can find the traits that come with Larch/C++. You can take care of it yourself as follows. On Unix, set your LARCH_PATH environment variable to include the directory where the Larch/C++ built-in traits live, followed be the directory where the LSL handbook traits live. In our example installation, you would set your LARCH_PATH environment variable to the following value.
.:/u/Larch/LCPP/lib:/u/Larch/LSL/lib
If you wish to do more extensive debugging of specifications or theorem proving, you may want to also get LP. You can get this from the global home page for Larch at the following URL.
http://www.sds.lcs.mit.edu/spd/larch/
You can also get it from the MIT ftp directory at the following URL.
ftp://larch.lcs.mit.edu/pub/Larch/lp/
Go to the first, previous, next, last section, table of contents.