Re: A question about substitution principle

Hello again!!

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:

Do you think it's possible to explain this so I understand it.
You are on a different level of my knowledge about this.

//Tony


"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> skrev i meddelandet
news:psnvyvi4qm7y$.2l3455284i1o$.dlg@xxxxxxxxxxxxx
> On Sun, 25 Sep 2005 12:13:17 GMT, Tony Johansson wrote:
>
>> 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?
>
> Yes.
>
> x y xVy
> -----------
> F F F
> F T T
> T F T
> T T T
>
>> You say that the postcondition of figure 2 is A.
>> and then you say this
>> Clearly A => A V B
>
> => is a logical implication:
>
> x y x=>y (= ~xVy)
> --------------
> F F T
> F T T
> T F F
> T T T
>
>> I'm not familar of this kind of writing
>> what actually does this A => A V B mean?
>
> It means that for all A, B (A=>AVB) is true. It is trivial to show:
>
> (x=>(x V y)) = (~x V (x V y)) = ((~x V x) V y) = (T V y) = T
>
>> Finaly do you mean that operation Figur1 is a subtype of the operation
>> for
>> Figure 2?
>
> It is a way different question. I don't share Liskov's view on the issue
> of
> subtyping. So my definition of subtypes differs!
>
> N.B. The idea of pre- and postconditions is wider than the issue of type
> relations. The purpose is actually to formally prove the program
> correctness. This is why implication => gets involved. That's the meaning
> of "weaker" and "stronger". You vary a correct program so that it remains
> correct. There is a technique of software development based on it, i.e.
> correctness by design. An excellent book on the issue is "The science of
> programming" by David Gries. DbC is a weaker, more pragmatic form of it.
>
> --
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de


.