Re: A question about substitution principle

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
.

Relevant Pages

  • Re: DbC, OOD and Stroustrups Rule, a concrete example
    ... If correctness cannot be stated then we just ... when a precondition just cannot be evaluated on a machine. ... there is a postcondition on the client of Thing. ...
    (comp.object)
  • Re: A question about substitution principle
    ... I'm sorry but I can't understand how you come from one postcondition ... >> I assume that your writing A V B must be understand that the ... >> Finaly do you mean that operation Figur1 is a subtype of the operation ... > correctness by design. ...
    (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: Design by contract and unit tests
    ... a precondition specifically states that there *is ... This is incorrect. ... prove the correctness of part of the contract (such as, for example, ... assertions aiming that goal can be safely deactivated in run-time. ...
    (comp.object)