@(#) $Id: README,v 1.5 1997/02/13 00:21:12 leavens Exp $

This directory contains the built-in traits for Larch/C++.
These traits are built-in in the sense that eventually,
the Larch/C++ checker will use these traits when sort-checking assertions.
They are also built-in in the sense that the semantics of Larch/C++ is
defined using them.

Thanks to Hua Zhong for doing the proofs that appear in the .proof files,
and for helping correct the mistakes in earlier versions of the proved traits
along the way.

The files in this directory are
Copyright (c) 1995, 1996, 1997 by Gary T. Leavens
All rights reserved.

Permission to use this software and its documentation
for educational purposes or for specifying software in
a commercial environment is hereby granted without fee.
Rights of commercial sale of this software and its documentation,
and modified versions thereof, are retained.
To copy or distribute this software, except for purposes of backups,
requires specific permission.

			   NO WARRANTY

THERE IS NO WARRANTY FOR THE PROGRAMS AND DOCUMENTS OF THIS PACKAGE. 
THE SOFTWARE IS PROVIDED AS IS.  YOU USE IT ENTIRELY AT YOUR OWN RISK.
THE AUTHORS ARE NOT RESPONSIBLE FOR ANY KIND OF LOSS OR DAMAGE THAT
MIGHT OCCUR BY USE OF THIS SOFTWARE.