From: volkert@nivoba.de (Volkert)
Subject: Re: Ada and Design By Contract
Date: 26 Mar 2003 01:00:42 -0800
Date: 2003-03-26T09:00:43+00:00 [thread overview]
Message-ID: <d37844cb.0303260100.58180d8d@posting.google.com> (raw)
In-Reply-To: 3E801279.80905@praxis-cs.co.uk
Dear Peter,
> > Volkert
>
> A small (but probably not the best) example:
>
> package P is
> function IsFull return Boolean;
> -- we may only want this function for assertion checking, not as
> -- part of our normally executable code
>
> procedure Push ...
> --! pre not IsFull; -- run time assertion
> ...
> end P;
IsFull is part of the contact between client/supplier.
The client needs access to IsFull. As a consequence
IsFull has to be part of the executible code.
> with P;
> package Q is
> procedure SomeOperation;
> -- Calls P.Push so we really need to propagate the precondition here
> --! pre not P.IsFull;
> ...
> end Q;
The caller has to check that not(P.isFull) is true, else
he can possibly break the contract. It is clear, that the caller
must implement this check in its own body
> with Q;
> package R is
> procedure AnotherOperation;
> -- this calls Q.SomeOperation;
> -- It's execution will involve the check not P.IsFull but P is not
> -- visible here.
> end R;
The check is made in the body of Q.SomeOperations. Why should
P.IsFull visible here?
> The really difficult cases are those that involve indirect manipulation
> of global data in remote packages. These problems are worst when trying
> to express a postcondition that depends on the initial values of that
> global data.
Part of a client/supplier contract can only the Entites visible
in the Ada Spec. For the post condition i can think that the
assertion statement can have also access to the private part of
the spec. But i see no problems to make the contract relevant
informations visible in the public part of a spec.
Volkert
next prev parent reply other threads:[~2003-03-26 9:00 UTC|newest]
Thread overview: 16+ messages / expand[flat|nested] mbox.gz Atom feed top
2003-03-23 18:55 Ada and Design By Contract Volkert
2003-03-24 9:41 ` Lutz Donnerhacke
2003-03-24 10:56 ` Peter Amey
2003-03-24 17:40 ` Volkert
2003-03-24 20:11 ` Lutz Donnerhacke
2003-03-25 8:04 ` Volkert
2003-03-25 8:25 ` Peter Amey
2003-03-25 9:55 ` Colin Paul Gloster
2003-03-25 10:09 ` Peter Amey
2003-03-26 9:00 ` Volkert
2003-03-26 9:00 ` Volkert [this message]
2003-03-26 9:38 ` Peter Amey
2003-03-26 19:00 ` Randy Brukardt
2003-03-26 19:32 ` Jeffrey Carter
2003-03-27 6:59 ` Volkert
2003-03-25 10:44 `
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox