Compile before proving correctness #24
Description
Many contextual tests are left unchecked in the TrueJ compiler and left to the Java compiler to find and issue error messages. For instance, trying to subtract a number from a boolean. This means that the Java compile needs to happen before the proofs in order to give the most direct error messages. The error messages from a failed proof will make it look like something is wrong with the proof statement's provability and give no clue about the simple error.