about the new Ada 2012 pre/post conditions

I never used contract programming, but looking at

http://www.adacore.com/uploads/techn...nd_aspects.pdf

I can see already that they will be useful to have.

But since I did not use them before, I am just wondering
what rules of thumbs are there for using them, as I can
see already I might end up not using them correctly.

Here is a simple example of what I mean:

-----------------------------
pragma Assertion_Policy(Check);

procedure Push(S: in out Stack; X: in Item)
with
Pre => not Is_Full(S),
Post => not is Empty(S);
is
....
end Push;
---------------------

One thing to notice right away, is that the pre/post checks
can be disabled or enabled by the pragma.

In the old days, (i.e. now with no pre/post), I would code
the above, by adding an explicit check myself at the
start of the Push() to check if the stack is full, and
if so, I would return an error code (I do not think I'll
throw an exception for this).

Hence Push() will be a function that is called like this

status = push(S,element)
if status = success -- Ok, was pushed ok
etc....
else
-- stack is full, do something else
end;

But now with pre there, this means the program will
throw an assertion if the stack is full. Ok, may be
this indicate logic error by the user of the stack,
but may be not.

But, and here is the problem, when I turn off assertions, I am
now left with the push() function with no check at all for
the case of the stack is full.

So, what is one to do? use pre/post AND also add
an extra check for full stack in the code as before?
does not make sense.

Keep the pre/post on all the time? do not make sense,
they are meant for testing time only, right?

They seem to definitely be something good to have.
Just need to figure the right way to use them (just like
with exceptions). May be more examples using contract
programming with Ada 2012 will be good to see.

--Nasser

On 20.06.12 15:39, Nasser M. Abbasi wrote:

> So, what is one to do?

One of the principles of DbC is that assertion
checking is not input checking. Rather, a programmer
is checking the programmers' assertions, including
his own. One flavor of assertion is called assumption.

Conditions imply a proof obligation.

Whether or not a car is stopped by a computer should not
by any means depend on whether or not the assertions
are checked in running code. That's not the intent
of using them.

On Wed, 20 Jun 2012 08:39:50 -0500, Nasser M. Abbasi wrote:

[...]
> But, and here is the problem, when I turn off assertions, I am
> now left with the push() function with no check at all for
> the case of the stack is full.
>
> So, what is one to do? use pre/post AND also add
> an extra check for full stack in the code as before?
> does not make sense.

This is what constitutes the core inconsistency about dynamic
pre-/post-conditions. If they #1 implement behavior (e.g the stack contract
to raise something when full), then they cannot be suppressed and do not
describe the contract. If they do describe the contract #2, they may not
implement it and thus shall have no run-time effect.

> They seem to definitely be something good to have.

Not everything is what it seems...

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

On 6/20/2012 9:13 AM, Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2012 08:39:50 -0500, Nasser M. Abbasi wrote:
>
> [...]
>> But, and here is the problem, when I turn off assertions, I am
>> now left with the push() function with no check at all for
>> the case of the stack is full.
>>
>> So, what is one to do? use pre/post AND also add
>> an extra check for full stack in the code as before?
>> does not make sense.
>
> This is what constitutes the core inconsistency about dynamic
> pre-/post-conditions. If they #1 implement behavior (e.g the stack contract
> to raise something when full), then they cannot be suppressed and do not
> describe the contract. If they do describe the contract #2, they may not
> implement it and thus shall have no run-time effect.
>

That is what I was thinking. So, I guess I am not alone.

>> They seem to definitely be something good to have.
>
> Not everything is what it seems...
>

Since I myself have no experience in contract programming,
I have to wait and see how they work out. I assume they
must be good thing to have, to make the program more
robust,but if used correctly.

I do not want to end up using them as substitute for
actual logic that I would use in the code itself.

When exceptions were new thing, many started using them in
place of the old fashioned if/then to check for
error in logic and just return an error code. Everyone
started just throwing exceptions everywhere, i.e. misused
them. I can see this might happen with pre/post as they
are new thing.

Will have to wait for gnat Ada 2012 to come out and start
using them to find out.

--Nasser

On Wed, 20 Jun 2012 09:24:48 -0500, Nasser M. Abbasi wrote:

> On 6/20/2012 9:13 AM, Dmitry A. Kazakov wrote:
>> On Wed, 20 Jun 2012 08:39:50 -0500, Nasser M. Abbasi wrote:
>>
>> [...]
>>> But, and here is the problem, when I turn off assertions, I am
>>> now left with the push() function with no check at all for
>>> the case of the stack is full.
>>>
>>> So, what is one to do? use pre/post AND also add
>>> an extra check for full stack in the code as before?
>>> does not make sense.
>>
>> This is what constitutes the core inconsistency about dynamic
>> pre-/post-conditions. If they #1 implement behavior (e.g the stack contract
>> to raise something when full), then they cannot be suppressed and do not
>> describe the contract. If they do describe the contract #2, they may not
>> implement it and thus shall have no run-time effect.
>
> That is what I was thinking. So, I guess I am not alone.

Two of us, to be precise.

>>> They seem to definitely be something good to have.
>>
>> Not everything is what it seems...
>
> Since I myself have no experience in contract programming,
> I have to wait and see how they work out. I assume they
> must be good thing to have, to make the program more
> robust,but if used correctly.

No, it is impossible to use correctly what is incorrect. Choose #1 or #2,
the rest will follow automatically.

> When exceptions were new thing, many started using them in
> place of the old fashioned if/then to check for
> error in logic and just return an error code.

Many are still confused about it. Independently on exceptions, it is
inconsistent for a program to check the consistency, correctness, logic etc
of its own by whatever means.

Correctness to be checked statically or dynamically by an *independent*
program.

> Will have to wait for gnat Ada 2012 to come out and start
> using them to find out.

No. If you want #2, use SPARK (because contracts *shall* be checked
statically). If you want #1, use if- and case-statements (because the
program *shall* implement what it was contract for). Period.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

On 20.06.12 16:37, Dmitry A. Kazakov wrote:

> Correctness to be checked statically or dynamically by an *independent*
> program.

Yes, the independent program that checks the assertions is us,
fixing bugs (a.k.a. correcting partial proofs).

The human aspect of pre/post checking is why some assertions
need not be expressible in Ada (and we are free to substitute
True).
Nevertheless, if conditions/assumptions/assertions are
formally expressible, Ada 2012 lets us ask the compiler for
practical help. The programs can perform a few tests automatically,
so that we can fix faulty programs, or faulty assertions, or
faulty brains.

On Wed, 20 Jun 2012 19:02:37 +0200, Georg Bauhaus wrote:

> On 20.06.12 16:37, Dmitry A. Kazakov wrote:
>
>> Correctness to be checked statically or dynamically by an *independent*
>> program.
>
> Yes, the independent program that checks the assertions is us,
> fixing bugs (a.k.a. correcting partial proofs).

Yes, of course. This process is called "code review."

> Nevertheless, if conditions/assumptions/assertions are
> formally expressible,

and *determinable* for the checker being considered.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

On Wednesday, June 20, 2012 6:39:50 AM UTC-7, Nasser M. Abbasi wrote:
>
> One thing to notice right away, is that the pre/post checks
> can be disabled or enabled by the pragma.

GNAT provides compiler switch -gnata for this purpose. In addition, GPS has Enable assertions check box.

A. Vo

On Wednesday, June 20, 2012 6:39:50 AM UTC-7, Nasser M. Abbasi wrote:
>
> throw an exception for this).

In Ada, one raises an exception.

> Hence Push() will be a function that is called like this
>
> status = push(S,element)
> if status = success -- Ok, was pushed ok
> etc....
> else
> -- stack is full, do something else
> end;

Decades of experience show that it will usually be used as:

Dummy := Push (S, Element);
etc...

This is part of the reason exceptions exist.

If Push raises an exception, rather than returning an error code/flag, then the caller either has to handle that exception, or write

if Is_Full (S) then
-- stack is full, do something else
else
etc...
end if;

> Keep the pre/post on all the time? do not make sense,
> they are meant for testing time only, right?

Any checks worth having during testing are worth having after testing. This is why you want a way to ensure they're always done.

For your own use, the answer is to keep the checks on. The real problem is for reusable code. The caller may not be you, and so may have turned off the checks, so such code should not have the precondition, but should have the hard-coded checks.

--
Jeff Carter
jrcarter commercial-at-sign acm (period | full stop) org

On Wednesday, June 20, 2012 1:16:44 PM UTC-7, Jeffrey R. Carter wrote:
>
> if Is_Full (S) then
> -- stack is full, do something else
> else
Push (S, Element);
> etc...
> end if;

--
Jeff Carter
jrcarter commercial-at-sign acm (period | full stop) org

W dniu środa, 20 czerwca 2012 22:16:44 UTC+2 użytkownik Jeffrey R.. Carter napisał:

> Decades of experience show that it will usually be used as:
>
> Dummy := Push (S, Element);
> etc...

Yes.

> This is part of the reason exceptions exist.
>
> If Push raises an exception, rather than returning an error code/flag, then the caller either has to handle that exception,

Decades of experience (OK, Java is a bit younger) show that it will usuallybe used as:

begin
Push (S, Element);
exception
when others => null;
-- TODO: (errr, it never happens, right?)
end;

The first version is at least easier to follow in the debugger...

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

On Wed, 20 Jun 2012 13:51:32 -0700 (PDT), Maciej Sobczak wrote:

> Decades of experience (OK, Java is a bit younger) show that it will usually be used as:
>
> begin
> Push (S, Element);
> exception
> when others => null;
> -- TODO: (errr, it never happens, right?)
> end;
>
> The first version is at least easier to follow in the debugger...

Not in Ada where exceptions are not contracted. In Ada one just forgets to
catch.

Which raises an interesting question: if Ada had contracted exceptions,
people would start adding meaningless when others =>. But with contracted
exceptions the compiler would know all exceptions possible in the context.
We could make others an illegal choice in such cases. The programmer would
have to explicitly specify exceptions to catch.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

"Jeffrey R. Carter" <ggsub@pragmada.co.cc> writes:

> Any checks worth having during testing are worth having after testing.

I say: If you don't need to turn off (at least some) assertions for
efficiency reasons, then you probably don't have enough assertions.

- Bob

On 21.06.12 00:19, Robert A Duff wrote:
> "Jeffrey R. Carter"<ggsub@pragmada.co.cc> writes:
>
>> Any checks worth having during testing are worth having after testing.
>
> I say: If you don't need to turn off (at least some) assertions for
> efficiency reasons, then you probably don't have enough assertions.

One measure for "enough assertions" is, I think, when some set
of assertions will finally have been shown to be a consequence
of the program. What are we testing if this set would still be
worth testing, then?

"Nasser M. Abbasi" <nma@12000.org> wrote in message
news:jrsjr7$uuo$1@speranza.aioe.org...
....
> -----------------------------
> pragma Assertion_Policy(Check);
>
> procedure Push(S: in out Stack; X: in Item)
> with
> Pre => not Is_Full(S),
> Post => not is Empty(S);
> is
> ....
> end Push;
> ---------------------
>
> One thing to notice right away, is that the pre/post checks
> can be disabled or enabled by the pragma.

Yes, but this is not a problem if you are careful. Specifically, your
packages should at least contain

pragma Assertion_Policy (Pre => Check,
Pre'Class => Check,
Static_Predicate => Check,
Dynamic_Predicate => Check);

(That is, all of the "inbound" assertion checks.)

Then, the only way for someone to ignore these checks is to edit the source
code of your library. If they do that, they've clearly "violated the
warranty", and you have no obligation to make the body do anything useful if
they do that.
[Aside: note that assertions are "ignored", not "suppressed". The difference
is that suppressed checks can still be made; it is only a permission to the
compiler, not a requirement; ignored checks cannot be made.]

This was a major topic of the Texas ARG meeting (the last one mainly about
Ada 2012), and the above is the solution that we came up with. Note that
there was a *lot* of discussion and opinion on this topic. Some people felt
that any time someone ignores checks, that the program is erroneous and
there ought to be no expectation that it works (if the checks would fail).
Others (including me) felt that adding erroneous behavior because you added
something that was supposed to make the program safer was nonsensical.

....
> So, what is one to do? use pre/post AND also add
> an extra check for full stack in the code as before?
> does not make sense.

Do as above. Force "inbound" checks to always be on (there is no need to
leave "post" and "invariant" on, they only can fail due to a bug in your own
code, not by anything that the caller can do).

Randy.