Ada and Design By Contract

Ada and Design By Contract

[Volkert]

Some time ago in c.l.a. was a discussion on 
adding Assertions (preconditions, postconditions
and invatiants) to Ada 95. 

- what is the current status? 
- who is working on this topic
- who is interested in Dbc for Ada

Volkert

Re: Ada and Design By Contract

[Lutz Donnerhacke]

* Volkert wrote:
> Some time ago in c.l.a. was a discussion on 
> adding Assertions (preconditions, postconditions
> and invatiants) to Ada 95. 
> 
> - what is the current status?

man SPARK.

> - who is working on this topic

Praxis Critical Systems.

> - who is interested in Dbc for Ada

The SPARK community.

Re: Ada and Design By Contract

[Peter Amey]

Volkert wrote:
> Some time ago in c.l.a. was a discussion on 
> adding Assertions (preconditions, postconditions
> and invatiants) to Ada 95. 
> 
> - what is the current status? 
> - who is working on this topic
> - who is interested in Dbc for Ada
> 
> Volkert

To keept this thread under some sort of control, I suggest we agree a 
clear distinction between contracts enforced at run time (by the 
evaluation of checks and, typically, the raising of exceptions if the 
contract is vilated) and contracts enforced statically, prior to 
execuation (typically using proof technology).

As Lutz has pointed out in an earlier reply, SPARK certainly provides 
the latter and has done for some years.

There have been some proposals for run-time assertions in Ada 0Y 
although many participants in the review process have found them 
wanting.  The big problem here is that the really interesting 
contractual claims may involve items not visible at the point where the 
contract is being checked (unless the code is rewritten with reduced 
abstraction to make them visible).

Peter

Re: Ada and Design By Contract

[Volkert]

> To keept this thread under some sort of control, I suggest we agree a 
> clear distinction between contracts enforced at run time (by the 
> evaluation of checks and, typically, the raising of exceptions if the 
> contract is vilated) and contracts enforced statically, prior to 
> execuation (typically using proof technology).
I know Spark and i like it, but my question is more in the direction
of Eiffel-like Assertion mechanisms (runtime monitoring/checking).


> There have been some proposals for run-time assertions in Ada 0Y 
> although many participants in the review process have found them 
> wanting.  
Can you/someone give me a pointer to it ...i found only
a paper from Ehud Lamm from the last Ada-Europe Meeting.

> The big problem here is that the really interesting 
> contractual claims may involve items not visible at the point where the 
> contract is being checked (unless the code is rewritten with reduced 
> abstraction to make them visible).
I see not the problem. Can you give a short example.

Volkert

Re: Ada and Design By Contract

[Lutz Donnerhacke]

* Volkert wrote:
>> To keept this thread under some sort of control, I suggest we agree a 
>> clear distinction between contracts enforced at run time (by the 
>> evaluation of checks and, typically, the raising of exceptions if the 
>> contract is vilated) and contracts enforced statically, prior to 
>> execuation (typically using proof technology).
> I know Spark and i like it, but my question is more in the direction
> of Eiffel-like Assertion mechanisms (runtime monitoring/checking).

So you are looking for Anna. The sites are off since years, but the Internet
archive did have it two years ago.

Re: Ada and Design By Contract

[Volkert]

> So you are looking for Anna. The sites are off since years, but the Internet
> archive did have it two years ago.
Anna is for Ada 83. As far is i remember does it
not support a concept like PRE-Conditions. Has anybody 
ever used Anna?

Volkert

Re: Ada and Design By Contract

[Peter Amey]

Volkert wrote:
[snip]
> 
>>The big problem here is that the really interesting 
>>contractual claims may involve items not visible at the point where the 
>>contract is being checked (unless the code is rewritten with reduced 
>>abstraction to make them visible).
> 
> I see not the problem. Can you give a short example.
> 
> 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;

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;

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

SPARK avoids these problems by having two different sets of scopes: 
program (i.e. Ada) context and proof context.  In the above example, we 
would make IsFull a proof function (i.e. not part of the executable 
code) and make use of "inherit" to make it visible without having to 
increase the number of with clauses.

regards


Peter

Re: Ada and Design By Contract

[Colin Paul Gloster]

Peter Amey wrote:
"The big problem here is that the really interesting 
contractual claims may involve items not visible at the point where the 
contract is being checked (unless the code is rewritten with reduced 
abstraction to make them visible)."

Yesterday I received in the post an application form for another Adaxia
event which is to have a presentation by a very pro-OO, pro-C++, probably
pro-abstraction expert so I would have a doubt that he practises all the
pro-correctness policies of SPARK users'. I quoted an email of this
speaker's in which he/she disapproved of one way of emulating a very small
part of Ada with C in "some people who have seen the light still do not
learn (single = in C conditions)" on Team Ada which is currently archived
at HTTP://WWW.ACM.org/archives/wa.cgi?A2=ind0211&L=team-ada&F=&S=&P=300
with timestamp Tue, 19 Nov 2002 14:57:41 +0000. Examining his email
closely he could be interpreted to be pro-Ada. On the plus side, he
provided me with moral support to learn Ada and in coping with gross
inefficiency from an ACM office when I was joining the Association for
Computing Machinery.

In a later post, Peter Amey said:

"[..]  In the above example, we 
would make IsFull a proof function (i.e. not part of the executable 
code) and make use of "inherit" to make it visible without having to 
increase the number of with clauses."

Could you please describe the SPARK concept of "inherit"?

Regards,
Colin Paul Gloster

Re: Ada and Design By Contract

[Peter Amey]

[snip]

> In a later post, Peter Amey said:
> 
> "[..]  In the above example, we 
> would make IsFull a proof function (i.e. not part of the executable 
> code) and make use of "inherit" to make it visible without having to 
> increase the number of with clauses."
> 
> Could you please describe the SPARK concept of "inherit"?
> 
> Regards,
> Colin Paul Gloster

Inherit, in this context, is a package-level annotation which behaves 
rather like "with" (actually rather like the transitive closure of the 
with clauses) but in proof context.  In my example, package R would 
inherit packages P and Q even though it only withs Q.  This would make 
the proof function P.IsFull visible at the place needed to check the 
contract.

Inheritance does of course have other connotations nowadays!

Peter

Re: Ada and Design By Contract

[Volkert]

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

Re: Ada and Design By Contract

[Peter Amey]

Volkert wrote:
> 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? 
> 

Because it is too late to wait until Q.SomeOperation is executed in 
breach of contract.  The real cause of the contract failure is 
AnotherOperation's attempt to call Q.SOmeOtherOperation in a way that 
will cause the stack to overflow.  If we want to try and deal with the 
problem we need to know where the dangerous condition started.   In our 
view this is better done by proof than by dynamic checks.

Peter

Re: Ada and Design By Contract

[Randy Brukardt]

Peter Amey wrote in message <3E817504.5040806@praxis-cs.co.uk>...
>> The check is made in the body of Q.SomeOperations. Why should
>> P.IsFull visible here?
>
>Because it is too late to wait until Q.SomeOperation is executed in
>breach of contract.  The real cause of the contract failure is
>AnotherOperation's attempt to call Q.SOmeOtherOperation in a way that
>will cause the stack to overflow.  If we want to try and deal with the
>problem we need to know where the dangerous condition started.   In our
>view this is better done by proof than by dynamic checks.


Which is why Janus/Ada was always included a call walkback with every
unhandled exception, and includes this information in
Exception_Information. It's often the case that the location of an
exception being raised (assertion failure) isn't enough information.
But, usually (probably more than 90% of the time), knowing the caller(s)
allow tracing/fixing the bug without having to add additional code (or
even run the program again).

Proof has its place, of course, but I don't think that most systems can
justify the extra work to develop that way. A few carefully placed
run-time assertions (combined with good compiler suppprt - it's not
surprising that Gnat added a walkback feature) are sufficient for
non-critical systems.

               Randy.

Re: Ada and Design By Contract

[Jeffrey Carter]

Peter Amey wrote:
> 
> Volkert wrote:
> 
>>> 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?
> 
> Because it is too late to wait until Q.SomeOperation is executed in 
> breach of contract.  The real cause of the contract failure is 
> AnotherOperation's attempt to call Q.SOmeOtherOperation in a way that 
> will cause the stack to overflow.  If we want to try and deal with the 
> problem we need to know where the dangerous condition started.   In our 
> view this is better done by proof than by dynamic checks.

It seems to me that R.Anotheroperation is responsible for checking the 
precondition to Q.Someotheroperation, not the client of R.

-- 
Jeff Carter
"This school was here before you came,
and it'll be here before you go."
Horse Feathers

Re: Ada and Design By Contract

[Volkert]

> 
> It seems to me that R.Anotheroperation is responsible for checking the 
> precondition to Q.Someotheroperation, not the client of R.
Exactly ... 

Volkert

Re: Ada and Design By Contract

[Volkert]

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

Re: Ada and Design By Contract

[@ 2003-03-25 10:44 UTC (permalink / raw)]

Volkert wrote:
> Some time ago in c.l.a. was a discussion on 
> adding Assertions (preconditions, postconditions
> and invatiants) to Ada 95. 
> 
> - what is the current status? 

   By now, I think each compiler provides its own assertions mechanism. 
For example, in GNAT you have "pragma Assert (<boolean expr>)".

   There is an AI now that proposes a standard way to do that. Take a 
look at:

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00286.TXT?rev=1.5

Rodrigo