Running Randoop over specifications generated from OpenJDK, we ran into two specifications that apply to the same method that show a discrepancy in translation of conditions.
The method java.io.PrintWriter.append(char c) has the post-condition
true => result.equals(target)
that is the correct interpretation of the tag @return This writer.
However, this method also inherits a post-condition
true => result.equals(c)
from java.lang.Appendable.append(char) that is an incorrect translation of the tag @return A reference to this Appendable .
Specification for java.io.PrintWriter.append(char c):
Running Randoop over specifications generated from OpenJDK, we ran into two specifications that apply to the same method that show a discrepancy in translation of conditions.
The method
java.io.PrintWriter.append(char c)
has the post-conditiontrue => result.equals(target)
that is the correct interpretation of the tag@return This writer
.However, this method also inherits a post-condition
true => result.equals(c)
fromjava.lang.Appendable.append(char)
that is an incorrect translation of the tag@return A reference to this Appendable
.Specification for
java.io.PrintWriter.append(char c)
:Specification for
java.lang.Appendable.append(char)