The version of the browser you are using is no longer supported. Please upgrade to a supported browser.Dismiss

View only
Nonconformance 1: PreconditionNonconformance 2: PostconditionNonconformance 3: Invariant
JML dev. answersLikely causeJML dev. answersLikely causeJML dev. answersLikely cause
Method distPointLine didn't have any specification restraining variable y.Weak preconditionCode can't resolve specification as getName can also return null.Code errorCode doesn't treat values default for parameters to respect invariant.Code error
-Undefineda pós-condição do construtor não garante que é diferente de null.
getName deve ter uma pré-condição para garantir a pós-condição. \result.equals vai retornar nullPoint exception se for igual a null.
Weak preconditionO invariante garante o que a spec determina.Undefined
Não consegui categorizar a não conformidade.UndefinedO desenvolvedor deveria ter inicializado a variável.Code errorO 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 errorThe 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 postconditionTo 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.UndefinedLack of initialisation of name to a non-null value in the constructor. This causes a null dereference in the post condition of getName.Code errorSpecification (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>0Strong preconditionfield name should be initialized to empty stringCode errorappointmentID in given test case is negative but invariant stated that it has to be more than 0Code error
weak precondition

**If we had a precondition (in distPointLine) protecting the call to division, we could prevent such precondition error.
Weak preconditionweak precondition; a precondition or invariant that test the nullity for the fied name is enough.Weak preconditionThe call to the constructor is violating the invariant 0x00 <= appointmentID && appointmentID <= 0x7F;Code error
Strong PreconditionStrong preconditionWeak PreconditionWeak preconditionStrong InvariantStrong invariant
The method <int> division(int, int) has a STRONG PRECONDITION (requires y>0).Strong preconditiongetName must be aware of null variables. WEAK PRECONDITION.Weak preconditionSTRONG 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.UndefinedConstructor "requires" clause must ensure all variables are initializedWeak preconditionContract says appointmentID must be greater than or equal to zero and invocation is done with negative valuesCode 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 preconditionAt the end of getName, \result can be null, and the given ensures clause is too strong to allow that.Strong postconditionThe given constructor does not have a proper precondition to ensure the invariant.Weak precondition
Code errorCode errorStrong post-conditionStrong postconditionWeak preconditionWeak 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 errorThe 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 preconditionShould have a precondition that the arguments of the constructor must be non-negative, and the text case should be fixed.Weak precondition
distPointLine() bodyCode errorLack of initialization within the constructor.Code errorInvariant is very complex, I could not, from the context, infer which one is wrong.Strong invariant
Code errorCode errorI don't see why this is nonconformance. The specification is correctly stating the intent of the code. UndefinedThere 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