#144 jmlc should check specifications of model methods

[Gary T. Leavens]

The jmlc tool doesn't check specifications of model methods when they are called, and thus doesn't ensure consistency between model methods and their specifications. This means that using model method specifications in static verification is suspect and doesn't necessarily correspond to runtime checking.

The attached was submitted by a user.

[Gary T. Leavens]

modelTest.java, test file that shows the problem