From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,2c6139ce13be9980
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: Joachim Durchholz <joachim.durchholz@munich.netsurf.de>
Subject: Re: Precondition Checking For Ada 0X (Was: Separation of IF and Imp:
 process issue?)
Date: 1997/09/17
Message-ID: <342023BB.4D598C60@munich.netsurf.de>#1/1
X-Deja-AN: 274062369
References: <mheaney-ya023680001009971956580001@news.ni.net>
 <EGLBMK.A5I@syd.csa.com.au> <341eac5e.0@news.uni-ulm.de>
 <184347314wnr@eiffel.demon.co.uk> <EGME6n.470@world.std.com>
X-Priority: 3 (Normal)
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-09-17T00:00:00+00:00
List-Id: <comp.lang.ada>


Robert A Duff wrote:
> My understanding is that the compiler generates run-time checks for
> invariants at both entry to and exit from each feature.  Is that
> correct?  If so, why?  How can the check-upon-entry ever fail, since
> the
> invariant must be true initially, and must be true after every exit?

Let's try another answer:

The object in question may have an invariant that refers to attibutes of
another object. Nothing in the language prevents other code from
modifying these attributes while the current object isn't active, so the
class invariant may have been made invalid in the mean time.

Unfortunately, this is a problem domain issue and can't be avoided by
programming language rules. Imagine the following situation:
  I say I had to leave my employer because he went bankrupt.
  You say you just started a new project with a customer.
Nobody will note a discrepancy until he finds out that your customer is
actually my employer.
More formally, let's say
  class EMPLOYEE
  feature
    employer: COMPANY;
  invariant
    not employer.bankrupt
  end
  class COMPANY
  feature
    bankrupt: BOOLEAN;
    feature go_bankrupt is
    do
      bankrupt := true
    end
  end

(somewhere else)
  feature
    acme: COMPANY
  ...
  me.employer := acme -- let's say acme is healthy right now
  you.customer := acme
  -- not let's violate my invariant:
  you.customer.go_bankrupt -- now the invariant of 'me' is violated
  ... -- lots of code in-between
  me.employer.do_something -- now the run-time system touches 'me'
  -- for the first time after a long period; this is the first chance
  -- is gets to check my precondition and sees that it is violated,
  -- so it raises the exception on entry to do_something

I hope this alternative explanation helps somebody understand the
issue...

Regards,
Joachim
-- 
Please don't send unsolicited ads.