This page requires the following content:

• Overview of the basic model (a good figure would be nice)

• Link to Alaina's example (how the process works by hand)

• Generated wrapper class structure

• Auxiliary files generated by the JML compiler

• Class loading at run-time

Control Options Data Structure

The control options data structure is a tree stored in the JavaClassTree class. The JavaClassTree is a singleton class (it can only have one instance at any time). When it is instanciated, the class retrieves a list of all possible locations for directories that might contain .java or .jar files. It recurses through all subdirectories and .jar files and creates a tree that mimics that structure. Each node is a subclass of a JavaUnit node, an internal node is a JavaPackage and a leaf is a JavaClass.

JavaUnit

Each node in the tree is a subclass of this class. There are 5 attributes for every node regardless of what type it is.

1. Wrap - a bool to represent whether wrapping is turned on ; a set and get function
2. Precondition - a bool to represent whether precondition checks are on ; a set and get function
3. Postcondition - a bool to represent whether postcondition checks are on ; a set and get function
4. Invariant - a bool to represent whether invariant checks are on ; and a set and get function
5. Checkable - a bool to represent whether the node can have checks enabled ; get function only

JavaPackage

JavaPackage is the subclass of JavaUnit used for representing internal nodes in the tree. They have 3 areas that distinguish them from a JavaClass node.

1. JavaPackages are always checkable.

2. They contain a list of children and a method that returns an enumeration of the children for traversing the sub tree structure.

3. The set methods for the first 4 attributes, listed under JavaUnit, have a propogation argument so the sub-tree's options values can be updated or left intact.

JavaClass

JavaClass is the subclass of JavaUnit used for representing leaf nodes in the tree.

1. JavaClass nodes checkable if and only if the 4 supporting auxillary files are present for the class represented by the node.

2. The set functions will not change the value for the attributes unless the node is checkable