Consider a Rectangle class and a Square class that inherits from the Rectangle class:

Question

a. Write post conditions for the Rectangle.setWidth(w:int) and the Rectangle.setHeight(h:int)
operations in terms of the Rectangle.getWidth():int and the Rectangle.getHeight():int
operations.
b. Write an invariant for the Square class stating that the width and height of a Square should always be the
same.
c. Consider the rules for inheriting contracts described in Section 9.4.5 in the context of the
Square.setWidth() and Square.setHeight() operations of the Square class. Are all rules met? Why
not? What should change in the model?

Answer 1

a. operations in terms of the Rectangle.getWidth():int and the Rectangle.getHeight():int
operations.
context Rectangle::setWidth(w) post:
w = getWidth() and getHeight() = @pre.getHeight()
context Rectangle::setHeight(h) post:
h = getHeight() and getWidth() = @pre.getWidth()
b. context Square inv: getWidth() = getHeight()
c. As written above, the Square.setWidth() and Square.setHeight() would violate the postconditions of the
Rectangle.setWidth() and the Rectangle.setHeight(). Square should not inherit from Rectangle as it does not
provide the same external behavior with respect to setWidth() and setHeight() (as defined by the LSP).
To make this exercise clearer, the instructor could write the postcondition for Rectangle.getWidth(), as the second
part of the postcondition is often missed.