Note: I have read a similar post, but my problem seems different from that. Read my attempts to understand the problem for why I believe they are different.

My problem:

I know that (see this and this)

  1. A subtype of another type should give stronger or the same specifications of the supertype.
  2. Spec $A$ is stronger than spec $B$ iff the set of implementations that satisfy $A$ is a proper subset of the set of those that satisfy $B$. Therefore, $A$ is stronger than $B$ if either
    • i. $A$ has weaker preconditions than $B$ does, or
    • ii. $A$ has stronger postconditions than $B$ does.

However, I have encountered a confusing situation in today's programming:

  • I have a base class Essay, and subclasses of different kinds of essays, say EssayA and EssayB, that inherit Essay.
  • To summarise a list of a specific kind of essay, I define the base class EssaySummariser that
    • has a virtual method include(Essay e) that takes an essay into account for the future summary.
      • include()'s precondition: e must all be of a certain type of Essay.
      • include()'s postcondition: e is included in the summariser and will be used to form the summary.
    • has a virtual method summarise() that summarises all included essays.
  • Now to implement a summariser for essays of type A, EssayA, I define a subclass of EssaySummariser, EssayASummariser, which overrides the include() method:
    • new include()'s precondition: e must all be of the type EssayA
    • new include()'s postcondition: e is included in the summariser and will be used to form.

It appears that EssayASummariser's spec of include() has a stronger precondition than EssaySummariser's. However, it also doesn't seem wrong as a subtype.

My attempts to understand the problem

  1. I have attempted to treat the new specification as having the same precondition but as having a stronger postcondition: only e's of type A are included. Other types will cause the method to throw.

    • This attempt to interpret it seems wrong, because the new postcondition I imagined violates the original one (original one says any type of e's will be included)
  2. I have just read a similar post here. Trying to apply the answer to that post, I may imagine that my EssaySummariser is not a true ADT, but EssayASummariser is.

    • However, the situation in my problem here is different from that in that post. Specifically, my EssaySummariser is not a genetic type.
    • More seriously, if the two situations are the same, then I imagine I can convert genetic classes in that problem to non-genetic classes in my problem, and say that some classes cannot be ADT because of such specifications. This does not sound right because I think any specs can be allowed into an ADT.  

My questions

  1. Is it legitimate to create subtypes like I did in my problem? In particular, was my attempt 2 correct in applying that post's knowledge to my problem?
  2. If it is, how do I map the theories to the reality in the problem?

1 Answer 1


I'm not an expert on this, but with the way you have defined EssayASummarizer, I don't believe it is a subtype of EssaySummarizer. You have already explained why: the set of implementations that can instantiate EssayASummarizer is not a subset of the set of implementations that can instantiate EssaySummarizer. Specifically, an instance of EssayASummarizer has an include() method that cannot accept an EssayB, so it does not qualify as an instance of EssaySummarizer.

I suggest you read more about covariance and contravariance, e.g., https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science). Your EssaySummarizer is like a function Essay -> Output, and your EssayASummarizer is like a function EssayA -> Output. The latter function is not a subtype of the former function, due to contravariance of the type of the input to the function.

  • $\begingroup$ Thank you very much. It feels amazing to discover a new topic from a daily problem. From a programming perspective, do you think it is still reasonable to inherit EssayASummariser from EssaySummariser then? It seems more convenient than Java's way of first creating genetics and second subtyping from instantiations, although Java's way ensures that inheritance always results in subtypes. $\endgroup$ Commented Mar 2 at 8:35
  • $\begingroup$ @GuanyumingHe, I don't know what is reasonable. Sorry. $\endgroup$
    – D.W.
    Commented Mar 2 at 9:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.