|Nonconformance 1: Precondition||Nonconformance 2: Postcondition||Nonconformance 3: Invariant|
|JML dev. answers||Likely cause||JML dev. answers||Likely cause||JML dev. answers||Likely cause|
|Method distPointLine didn't have any specification restraining variable y.||Weak precondition||Code can't resolve specification as getName can also return null.||Code error||Code doesn't treat values default for parameters to respect invariant.||Code error|
|-||Undefined||a pós-condição do construtor não garante que this.name é diferente de null.|
getName deve ter uma pré-condição para garantir a pós-condição. \result.equals vai retornar nullPoint exception se this.name for igual a null.
|Weak precondition||O invariante garante o que a spec determina.||Undefined|
|Não consegui categorizar a não conformidade.||Undefined||O desenvolvedor deveria ter inicializado a variável.||Code error||O desenvolvedor deveria ter feito a verificação no código para evitar a não conformidade.||Code error|
|I cannot see what the problem is here, without running the code through a runtime checker.|
I can only guess that division is called with a negative value, meaning that the code is wrong.
|Code error||The postcondition does not hold if name is null.|
I could only understand the example after rewriting the precondition to (name ==null || !name.equalls("")), and the same in the postcondition, and then the bug in the postcondition became obvious.
|Strong postcondition||To enforce the invariants, the constructor of class Diagnostic should have a precondition (namely to restrict the possible values of appointmentID and diagnosticID.)||Weak precondition|
|I get the impression that the code of distPointLine is wrong, but due to lack of specifications for this method and the square(Root) methods no violation of specification would be reported.||Undefined||Lack of initialisation of name to a non-null value in the constructor. This causes a null dereference in the post condition of getName.||Code error||Specification (precondition) of the constructor is too weak, should check the parameters to be in accordance with the invariant of the object.||Weak precondition|
|y can be negative for a division but specification stated y>0||Strong precondition||field name should be initialized to empty string||Code error||appointmentID in given test case is negative but invariant stated that it has to be more than 0||Code error|
**If we had a precondition (in distPointLine) protecting the call to division, we could prevent such precondition error.
|Weak precondition||weak precondition; a precondition or invariant that test the nullity for the fied name is enough.||Weak precondition||The call to the constructor is violating the invariant 0x00 <= appointmentID && appointmentID <= 0x7F;||Code error|
|Strong Precondition||Strong precondition||Weak Precondition||Weak precondition||Strong Invariant||Strong invariant|
|The method <int> division(int, int) has a STRONG PRECONDITION (requires y>0).||Strong precondition||getName must be aware of null variables. WEAK PRECONDITION.||Weak precondition||STRONG INVARIANT, as the appointmentID is in [0x00, 0x7F] range.||Strong invariant|
|right shift of variables in the square method may cause divide by zero exceptions.||Undefined||Constructor "requires" clause must ensure all variables are initialized||Weak precondition||Contract says appointmentID must be greater than or equal to zero and invocation is done with negative values||Code error|
|The given code is difficult to understand. That said, variable dist seems to be able to have 0, and thus at the entry of method division, y==0 is possible. However, the given requires clause is too strong to allow this precondition.||Strong precondition||At the end of getName, \result can be null, and the given ensures clause is too strong to allow that.||Strong postcondition||The given constructor does not have a proper precondition to ensure the invariant.||Weak precondition|
|Code error||Code error||Strong post-condition||Strong postcondition||Weak precondition||Weak precondition|
|Input and output ints are apparently fixed-point numbers scaled by 1024.|
This should be documented.
Code Error in that the test routine is called with integers that are not scaled.
If the arguments to distPointLine are supposed to be actual integers rather than scaled integers, then scaling must be coded into the routine.
|Code error||The specification for getName does not take into account the possibility that name is null, which is allowed elsewhere in the spec. Otherwise, name should be declared NonNull and the constructor modified.||Weak precondition||Should have a precondition that the arguments of the constructor must be non-negative, and the text case should be fixed.||Weak precondition|
|distPointLine() body||Code error||Lack of initialization within the constructor.||Code error||Invariant is very complex, I could not, from the context, infer which one is wrong.||Strong invariant|
|Code error||Code error||I don't see why this is nonconformance. The specification is correctly stating the intent of the code.||Undefined||There is an error in the specification of the constructor, where the condition on title length should have been title.length <= MAX_TITLE_LENGTH. I am not sure how this is discovered with the test case. The test case is checking for two arguments that are unrelated.||Undefined|