Unverified
An implementation which isn't tested or proven.
Tested
An implementation for which a thorough test class is written, and which passes all the tests. Test classes are placed in the org.jutiltest package, where the entire package structure of org.jutil is mirrored. The name of the test class is 'Test + the name of the class to be tested'.
For example, the test class for ForAll in package org.jutil.java.collections is named TestForAll and is in package org.jutiltest.java.collections.
Putting the test code in a different tree helps keeping the packages clean.
Proven
An implementation which is proven to be correct. We don't have a notation yet to write the proof of a method. A proof must be as formal as possible because in the end we want to be able to check it using a tool.
Of course, at some point Java classes need to be used in the code. Since they aren't proven and don't have specifications that allow us to write a proof, we will write specifications for them, and assume they are correct. This is not the ideal situation, but it's the best we can do. The JML project already has some specifications for the Java API.
|
