Re: A question about substitution principle

Dmitry A. Kazakov wrote:

> 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.

For the record, Bertrand Meyer uses a precise definition of "stronger"
(that the great majority of people don't actually know) :

X stronger-than Y = (X implies Y) AND NOT(X = Y)

For those with the CS101 propositional logic skills, the stronger-than
function is equivalent to :

Y AND NOT(X)


I now await the proofs as to which of the two Stack post-conditions
is stronger.

Or perhaps there is a contradiction (Circle/Ellipse anyone) . :-)


Regards,
Steven Perryman

.