Discrepancy in translation of similar @return conditions

[bjkeller]

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):

{
    "operation": {
      "classname": "java.io.PrintWriter",
      "name": "append",
      "parameterTypes": [
        "char"
      ]
    },
    "identifiers": {
      "parameters": [
        "c"
      ],
      "receiverName": "target",
      "returnName": "result"
    },
    "throws": [],
    "post": [
      {
        "property": {
          "condition": "result.equals(target)",
          "description": "This writer"
        },
        "description": "return This writer",
        "guard": {
          "condition": "true",
          "description": ""
        }
      }
    ],
    "pre": []
  }

Specification for java.lang.Appendable.append(char)

{
    "operation": {
      "classname": "java.lang.Appendable",
      "name": "append",
      "parameterTypes": [
        "char"
      ]
    },
    "identifiers": {
      "parameters": [
        "c"
      ],
      "receiverName": "target",
      "returnName": "result"
    },
    "throws": [],
    "post": [
      {
        "property": {
          "condition": "result.equals(c)",
          "description": "A reference to this Appendable"
        },
        "description": "return A reference to this Appendable",
        "guard": {
          "condition": "true",
          "description": ""
        }
      }
    ],
    "pre": []
  }