Removed non-existent class AssertionFactory from Makefile. Oops.
Additions and modifications to generate runtime assertion checking in separate
Removed the use of String.split() int WrapperPrettyPrinter, split() is not
The main modification here is to add support for subclasses. All wrapped
Added some simple tests.
This version also outputs in a limited fashion what the "original" java file
made changes as suggested by David.
Fixed a bug that does not take into account methods that are not overridden
Committing a couple of fizes to bugs in the List spec:
Fix a small bug in the specs for the add method of Set where I think it
In the model method abstractvalue, res.insert(new JMLInteger(i)); should be:
Some corrections for Set.spec:
Fixed a couple of spec bugs, notably, for List, subList is exclusive of the
Runner.java allows running classes without the gui.
some improved error handling for the class loader
fixing some one-off errors in subList. Specifically, when
Observable is better modeled as a set, rather than a bag of observers.
fixed a small bug that output the "original" file twice
Changes to these files to make JML-generated files compatible with
Change TransInvariant to head off a bug in multijava by adding the inner
These changes make the compiler actually generate bytecode (!)
Added paper citation: