How to determine whether the postcondition of overridden methods is weaker or stronger if there is no return value?

Question

To reiterate the question - what does it mean to have a weaker or stronger postcondition when overriding a method that only does side effects with another one that only does side effects?

P.S. What about a mix of side effects & return values?

Answer 1

A Stronger Post-Condition -> Guarantees More

Essentially not only will it do X, it will also do X this way.

If it returns a type Shape, then a stronger post-condition might be that it returns a type Quadrilateral which derives from Shape.

If it throws an exception, then a stronger post-condition might limit the kinds of exception, or even not throw at all.

Similarly for side-effects. If the original agreement was that it updates some object Bread by Cooking it, then a stronger post-condition would be to Cooking it in a Bread Oven. The former agreement equally permits a flame-thrower, and use of lava.

A more computer sciencey example would be sorting. void sort(data[]) with the post-condition being that data conforms to for i..datalength-2 -> data[i] <= data[i+1].

void logsort(data[]) implements that agreement, except it has a stronger post-condition: Stable Sort.

A Stable Sort also guarantees that elements that would compare equal maintain there relative order.

Given: [ d, c1, a, c2, b, e, c3]
where c1 == c2 == c3, and all the letters sort: a, b, c, d, e

A sort might give:
   [ a, b, c3, c1, c2, d, e]
or [ a, b, c1, c3, c2, d, e]
or [ a, b, c2, c3, c1, d, e]
or ...

Log Sort would always give:
   [ a, b, c1, c2, c3, d, e]

Log Sort as such has a Stronger Post Condition.

That isn't the only Post-Condition that Log-Sort provides. It also guarantees that it will be finished in O(NlogN) (with a sizeable coeffiecient, and overhead for allocating buffer space and move elements around).

Another Sort such as void quicksort(data[]) also implements the sort guarantees and offers a stronger guarantee by sorting the data in O(nlogn) with a worst case of W(N^2).

Generally speaking a quicksort will be faster than a logsort for most unsorted data, at the price of not necessarily maintaining the relative order of equivalent elements. Which means that while both sorts provide stronger post-conditions than is required by void sort(data[]) they aren't necessarily stronger or weaker than each other.