Re: A question about substitution principle

On Sun, 25 Sep 2005 10:09:40 GMT, Tony Johansson wrote:

> Figure 1: operation top element from a stack using weak contract
> Precondition: true
> Postcondition: If not empy
> then result = top element from stack
> else throw EmptyException
>
> Figure 2: operation top element from a stack using strong contract
> Precondition: true
> Postcondition: result = top element from stack
>
> The substitution principle and Bartrand Mayer say that in particular it does
> not make Figure 1 define a subtype of figure 2.
> Cerainly, the precondition of Figure 1 is weaker than that of Figure 2.

It is not weaker, it is equal: true <=> true

> The
> postcondition of Figure 1, however, is not stronger than that of Figure 2,
> since a thrown exception satisfies the former but not the latter.

No, it is. The postcondition of figure 1 is: A V B, where

A = (result = top element...)
B = (exception thrown)

The postcondition of figure 2 is A.

Clearly A => A V B

> Now to my question: I don't understand what it means with "The postcondition
> of Figure 1, however, is not stronger than that of Figure 2, since a thrown
> exception satisfies the former but not the latter."?

"Stronger or equal" on conditions is logical implication =>. The equality
relation is logical equivalence <=>.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.

Relevant Pages

  • Re: A question about substitution principle
    ... > I'm sorry but I can't understand how you come from one postcondition ... (result = top element from stack) ... V (EmptyException) ... as B] the second condition *implies* the first one. ...
    (comp.object)
  • Re: Best forum for OOD/Design by Contract discussions?
    ... relates to Design by Contract? ... DbC is a tool that was originally developed in R-T/E back in the '60s because it provides a rigorous approach to designing interactions among multiple state machines. ... The precondition includes algorithmic sequencing defined in requirements and the state of the overall solution as expressed in terms of state data values. ... Whatever that other behavior did can be expressed in terms of a postcondition on executing that other behavior. ...
    (comp.object)
  • Re: Client/Service relationships & Flow of Requirements.
    ... 'Observer' mean in the GoF pattern. ... Thus the precondition for executing the ... Observer action is not a precondition on a specific Subject object; ... The called must guarantee the postcondition is true *to the caller*, so it can't change the postcondition to suit its own purposes. ...
    (comp.object)
  • Re: Liskov Substitution Principle and Abstract Factories
    ... LSP tells that B's precondition should be the ... and postcondition should be the subset of A's. ... So if we want to substitute B for A (with seperate no contract enforcment), ...
    (comp.object)
  • Re: before after methods and call-next-method
    ... then the postcondition will be true if the function returns. ... let's assume that all the elements of the precondition ... Now suppose we implement a primary method that implements the generic ... method specializing on C. ...
    (comp.lang.lisp)