These specs are close to the original specs shipeed with Esc/Java.
They are modified where necessary to be consistent with current syntax
and typechecking of Esc/Java2.  These are used as a stable set of specs to
use when running many of the original tests that are part of the Esc/Java2
test suite.  You should not add to these specs any more than necessary to
keep the tests working.
