Re: A question about substitution principle

Hello!
I did a typo I meant that the precondition for the operation Figure 2 should
be not empty
of course.

You say the following
The postcondition of figure 1 is: A V B, where
A = (result = top element...)
B = (exception thrown)

I assume that your writing A V B must be understand that the
preconditionn is A or B. I'm right?
So to right A V B when you have the above for A and B is just equivalent of
writing
then result = top element from stack
else throw EmptyException
I'm right here also?

You say that the postcondition of figure 2 is A.
and then you say this
Clearly A => A V B

I'm not familar of this kind of writing
what actually does this A => A V B mean?

Finaly do you mean that operation Figur1 is a subtype of the operation for
Figure 2?

//Tony

"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> skrev i meddelandet
news:9s6nkuhjyvp1.1h6d9iitsw4a3$.dlg@xxxxxxxxxxxxx
> 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: not empty
>> 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: 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: precondition and postcondition
    ... >precondition by a weaker one, and its postcondition by a stronger one. ... An overriding method may strengthen the postcondition. ... class Rectangle { ... virtual void setHeight{ ...
    (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)