Re: A question about substitution principle

On Sun, 25 Sep 2005 16:38:07 GMT, Tony Johansson wrote:

> I'm sorry but I can't understand how you come from one postcondition
> saying that postcondition A is true for figure 2
> to this truth table
>
> x y x=>y (= ~xVy)
> --------------
> F F T
> F T T
> T F F
> T T T
>
> and then you say thisClearly A => A V B
> => is a logical implication:

A => A V B is a theorem. Its proof is in my previous post.

> Do you think it's possible to explain this so I understand it.

You asked why the condition

(result = top element from stack) V (EmptyException)

is weaker than or equal to

(result = top element from stack)

It is weaker because [denoting (result = top element from stack) as A and
(EmptyException) as B] the second condition *implies* the first one. To
imply means (see the truth table) than if the second condition is
satisfied, then the first one is satisfied too. I.e. if A is true, then B
is true too.

--
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 ... > imply means than if the second condition is ... Bertrand Meyer uses a precise definition of "stronger" ... I now await the proofs as to which of the two Stack post-conditions ...
    (comp.object)
  • Re: A question about substitution principle
    ... operation top element from a stack using weak contract ... > Precondition: true ... > Postcondition: If not empy ... operation top element from a stack using strong contract ...
    (comp.object)