about the new Ada 2012 pre/post conditions

about the new Ada 2012 pre/post conditions

[Nasser M. Abbasi]

I never used contract programming, but looking at

http://www.adacore.com/uploads/technical-papers/Ada2012_Rationale_Chp1_contracts_and_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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

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.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

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

Re: about the new Ada 2012 pre/post conditions

[Nasser M. Abbasi]

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

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.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

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

Re: about the new Ada 2012 pre/post conditions

[Anh Vo]

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

Re: about the new Ada 2012 pre/post conditions

[Jeffrey R. Carter]

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

Re: about the new Ada 2012 pre/post conditions

[Jeffrey R. Carter]

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

Re: about the new Ada 2012 pre/post conditions

[Maciej Sobczak]

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

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

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

Re: about the new Ada 2012 pre/post conditions

[Robert A Duff]

"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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

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?

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

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

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
...
> 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.

You're right, but I don't see any inconsistency. They are clearly #1, and 
that includes all of the existing Ada checks as well. And you are right, it 
*never* makes logical sense in Ada to suppress or ignore anything. They 
*are* part of the contract. The old saw about wearing seatbelts in the 
garage and taking them off when you leave is totally in operation here.

The *only* reason to suppress or ignore checks is for performance reasons, 
and those are clearly outside of any program logic. Moreover, this should be 
very rare, since this should only happen in the very narrow band when the 
program is too slow with the checks on and fast enough with them off (most 
programs will be fast enough always, and most of the rest will be too slow 
always).

I know Bob and some others disagree with this, and they're just outright 
wrong. (In part because I don't believe in requiring any checks as part of 
the contract that are too expensive to leave on always. The sorts of 
assertions that you might want to suppress because they are too expensive 
should *never* be part of the contract and I think they should be 
categorized differently from those that are part of the contract. But I 
found no traction for that idea, unfortunately.)

                                             Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Jeffrey R. Carter" <ggsub@pragmada.co.cc> wrote in message 
news:4f0d55a9-83e1-44fe-8943-0c73a34a594d@googlegroups.com...
...
> Any checks worth having during testing are worth having after testing. 
> This is why you want a way to ensure they're always done.

Right on.

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

"Hard-coded checks" prevent the compiler from doing call-site optimizations 
and tools from doing much of anything. They should be avoided. The solution 
is the pragma I showed earlier:

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

put in *every* reusable package spec. They still can suppress the checks by 
manually deleting the pragma, but it will render command line switches and 
IDE checkboxes ineffective. And if they do delete the pragma, they've 
intentionally shot themselves in the foot, and it is no longer your (the 
package maintainers) problem. (Unless of course they want to spend extra 
$$$.)

                                          Randy.

Re: about the new Ada 2012 pre/post conditions

[Jeffrey Carter]

On 06/21/2012 01:37 PM, Randy Brukardt wrote:
>
> "Hard-coded checks" prevent the compiler from doing call-site optimizations
> and tools from doing much of anything. They should be avoided. The solution
> is the pragma I showed earlier:
>
>     pragma Assertion_Policy (Pre =>  Check,
>                                             Pre'Class =>  Check,
>                                             Static_Predicate =>  Check,
>                                             Dynamic_Predicate =>  Check);
>
> put in *every* reusable package spec. They still can suppress the checks by
> manually deleting the pragma, but it will render command line switches and
> IDE checkboxes ineffective. And if they do delete the pragma, they've
> intentionally shot themselves in the foot, and it is no longer your (the
> package maintainers) problem. (Unless of course they want to spend extra
> $$$.)

Interesting. I wasn't aware of checks that can't be overridden by compiler 
options, and will be surprised if most compilers don't include a way to override 
these as well.

-- 
Jeff Carter
"Death awaits you all, with nasty, big, pointy teeth!"
Monty Python & the Holy Grail
20

--- Posted via news://freenews.netfront.net/ - Complaints to news@netfront.net ---

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
> ...
>> 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.
> 
> You're right, but I don't see any inconsistency. They are clearly #1, and 
> that includes all of the existing Ada checks as well.

If you take a stance on #1, then checking stack full is no more evaluation
of the precondition, which does not depend on the stack state anymore, as
it of course should be. So the "true" precondition is just: True. Then why
on earth anybody would denote it as:

   Pre => not Is_Full (S)

And implementations leaking into declarations is certainly a very bad idea.
An even worse idea is to slice implementations into parts of unclear
purpose. Instead of one package body, the maintainer will have to inspect
the body, and so-.called pre-/post-conditions slices.

Neither #1 nor #2 is defendable.

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

Re: about the new Ada 2012 pre/post conditions

[Martin]

On Thursday, June 21, 2012 9:23:57 PM UTC+1, Randy Brukardt wrote:
[snip]
>    pragma Assertion_Policy (Pre => Check,
>                                            Pre'Class => Check,
>                                            Static_Predicate => Check,
>                                            Dynamic_Predicate => Check);

Just created a 'to keep' file called 'randys_maxim.ada'...will be copy-n-pasting that a lot from now on I suspect! :-)

-- Martin

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 09:23, Dmitry A. Kazakov wrote:
> Neither #1 nor #2 is defendable.

Maybe dynamic checking is not defendable when the attack is
based on some biased, and, frankly, narrow set of assumptions.
Which is probably OK in some narrow field.

But from a workshop point of view, I'd throw in that
Pre/Post gives us vastly better error messages, as follows.

A clause of the contract, involving exceptions, looks
like this:

If you, client, do not obey the constract *Pre*, then I,
supplier, may fail to produce in accord with the contract
*Post*. I will throw something at you.

Exceptions will happen in any case. The Pre/Post aspects
show that this is the case.

However, exceptions will point to somewhere *inside* the
supplier's package if Pre/Post checking is off, or Pre = True.
Whereas, if Pre/Post checking is on as intended, exceptions
can pinpoint a *contract* violation by the client.

This behavior requires that pre/post conditions are properly
reflected in the supplier's implementation.

(I have indicated alternative possibilities (just on Pop),
as the specific contract of this example is probably one
among a number of choices. For the sake of simplicity, this
is a single stack package; the contractual behavior shouldn't
change much with a stack type declared instead.)

Compare

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
  failed precondition from stk.ada:20 instantiated at stk.ada:79

vs

raised CONSTRAINT_ERROR :
  stk.ada:60 range check failed


Note that the first message mentions a specific precondition
from the spec.  The second message points to the body. This
body may not be available for inspection! That is, if you want
to spend time finding your own error by understanding
the supplier's implementation first!


generic package Stk is

   pragma Elaborate_Body (Stk);

   Capacity : constant := 10;   -- or use a constrained subtype

   type T is interface;
   type Stackable is access constant T'Class;


   function Length return Natural;
   --  Number of items currently on the stack.

   procedure Push (Item : Stackable)
     with   Pre  => Length < Capacity,
            Post => Top = Item and Length = Length'Old + 1;
   -- Item becomes topmost if there is room

   procedure Pop
     with  Pre  => Length > 0,
           Post => Length = Length'Old - 1;
   -- Drops the topmost item, if any.
   -- [ALTERNATIVELY,
   --     Pre => True,
   --    Post => Length = Natural'Max (0, Length'Old - 1)]

   function Top return Stackable
     with   Pre => Length > 0;
   --  A copy of the topmost item.
   -- [ALTERNATIVELY ...]

end Stk;



package body Stk is

   Ptr : Natural range 0 .. Capacity;
   Data : array (Natural range 1 .. Capacity) of Stackable;

   --
   -- Strategy: there is a 1:1 correspondence between
   -- Ptr being in range and the pre/post conditions
   --

   function Length return Natural is
   begin
      return Ptr;
   end Length;

   procedure Push (Item : Stackable) is
   begin
      -- cannot produce Post if the stack is full, may raise C_E
      Data (Ptr + 1) := Item;
      -- Ptr not increased in case of failure
      Ptr := Ptr + 1;
   end Push;

   procedure Pop is
   begin
      Ptr := Ptr - 1;  -- if Ptr = 0, then C_E
   end Pop;

   function Top return Stackable is
   begin
      -- if Ptr not in 1 .. Capacity, then C_E
      return Data (Ptr);
   end Top;

begin
   Ptr := 0;
end Stk;

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 13:54, Georg Bauhaus wrote:

> (I have indicated alternative possibilities (just on Pop),
> as the specific contract of this example is probably one
 s/probably/certainly/

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote:

> On 22.06.12 09:23, Dmitry A. Kazakov wrote:
>> Neither #1 nor #2 is defendable.
> 
> Maybe dynamic checking is not defendable when the attack is
> based on some biased, and, frankly, narrow set of assumptions.

Sure, the most effective defence is just not to take any position. You
might get exposed otherwise.

BTW, narrower the set of assumptions is, wider is the context where the
conclusion stays true. I would not be so proud about liberally sweeping
assumptions, they may occasionally include flat earth or the Moon composed
of cheese...

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 14:43, Dmitry A. Kazakov wrote:
> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote:
> 
>> On 22.06.12 09:23, Dmitry A. Kazakov wrote:
>>> Neither #1 nor #2 is defendable.
>>
>> Maybe dynamic checking is not defendable when the attack is
>> based on some biased, and, frankly, narrow set of assumptions.
> 
> Sure, the most effective defence is just not to take any position. You
> might get exposed otherwise.

Who isn't taking a position?

Sir Tony Hoare back then took the position that Ada would
be far too big. Jean Ichbiah more or less answered in 1984 that
Ada is not to be measured against the capabilities of two guys
sitting in the corner wanting to understand everything about.


> BTW, narrower the set of assumptions is, wider is the context where the
> conclusion stays true.

As context is widened, the set of assumptions being narrowed,
the more specific and less informative the full text.
Context widening forces a general concept such as pre/post
to be specific, which it isn't.

I bet that most car electronics software does assume a flat earth
for velocity vectors.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 16:30, Georg Bauhaus wrote:

> I bet that most car electronics software does assume a flat earth
> for velocity vectors.

I mean, the car is moving, hopping, sliding on a plane,
not on a curved surface.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 22 Jun 2012 16:30:52 +0200, Georg Bauhaus wrote:

> On 22.06.12 14:43, Dmitry A. Kazakov wrote:
>> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote:
>> 
>>> On 22.06.12 09:23, Dmitry A. Kazakov wrote:
>>>> Neither #1 nor #2 is defendable.
>>>
>>> Maybe dynamic checking is not defendable when the attack is
>>> based on some biased, and, frankly, narrow set of assumptions.
>> 
>> Sure, the most effective defence is just not to take any position. You
>> might get exposed otherwise.
> 
> Who isn't taking a position?

You.

On the contrary, Randy was unambiguously clear that he supports #1.

You might also be surprised by Robert Dewar's opinion on and around the
subject, see recent discussion in LinkedIn, group: "Ada Programming
Language", thread: "Imaginary proposal for the next Ada standard: Ada
compilers will automatically generate Package Specification from Package
Body"

(He was ready to debunk use of exceptions, to dismiss design of Ada I/O.
People could do anything in order to save dynamic checks! (:-))

>> BTW, narrower the set of assumptions is, wider is the context where the
>> conclusion stays true.
> 
> As context is widened, the set of assumptions being narrowed,
> the more specific and less informative the full text.
> Context widening forces a general concept such as pre/post
> to be specific, which it isn't.

No, you cannot narrow any context so that laws of logic would not apply. If
you wanted to make an inherently inconsistent concept working, you would
have to rather widen the context to include alogical things and false
inherence.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 17:05, Dmitry A. Kazakov wrote:
> No, you cannot narrow any context so that laws of logic would not apply.

There is much more to programming than the laws of logic can express.
For example, human activity.

The world happens, including computers, and the laws of logic are
far too insufficient to capture it.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 22 Jun 2012 17:52:53 +0200, Georg Bauhaus wrote:

> The world happens, including computers, and the laws of logic are
> far too insufficient to capture it.

Great, now we are in cordial agreement that dynamic checks of Ada 2012 are
in breach with laws of logic! (:-))

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 17:05, Dmitry A. Kazakov wrote:
> On Fri, 22 Jun 2012 16:30:52 +0200, Georg Bauhaus wrote:
> 
>> On 22.06.12 14:43, Dmitry A. Kazakov wrote:
>>> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote:
>>>
>>>> On 22.06.12 09:23, Dmitry A. Kazakov wrote:
>>>>> Neither #1 nor #2 is defendable.
>>>>
>>>> Maybe dynamic checking is not defendable when the attack is
>>>> based on some biased, and, frankly, narrow set of assumptions.
>>>
>>> Sure, the most effective defence is just not to take any position. You
>>> might get exposed otherwise.
>>
>> Who isn't taking a position?
> 
> You.

I don't think that #1 xor #2 can be the basis of a meaningful
discussion of DbC, because of the frames of reference.

The ideal design is when the contract is nothing but documentation,
independent of implementation, and checks not affecting the program in
ways other than--within specifications--SPACE and TIME. *But*,
this state of pre/post is not a property of pre/post per se,
it is a property of programmers' style of working.

It is not adequate to apply the same reasoning to pre/post
aspects and to the non-ignorable part of the program's source.

Pre/Post are essentially a tool, not essentially a program;
only accidentally. This is why the on/off discussion cannot
be decided on the basis of mixing the two (pre/post and the
"intended program proper") conceptually. More on accidental
accidents below.

If the contract "behaves", it does so during the effort
at proving a piece of software correct. Ideally.

This is why, in the end--provided there is a suitable notion of
"end"--assertion checking can be safely turned off, where "safely"
means "safe" just as in formal semantics, not physical systems.

DbC is a tool. The technical meaning of programs--again in the sense
of a "goal"--is to be entirely determined by the program without
the assertions, but consistent with the assertions. A goal.
The accidental effects of assertions should not matter other than
as a programming tool. If they cause accidents, then these
accidents are as accidental as all other accident caused by
statically undecidable program behavior.

The overlap in effects is what makes assertion checking
a management issue to be aware of. But it is no major hurdle,
since anything that can happen unpredictably, at run time,
creates a risk to be assessed based on *business* criteria,
not on computer science criteria.


> You might also be surprised by Robert Dewar's opinion on and around the
> subject, see recent discussion in LinkedIn, group: "Ada Programming
> Language", thread: "Imaginary proposal for the next Ada standard: Ada
> compilers will automatically generate Package Specification from Package
> Body"

I don't currently see anything on LinkedIn, takes admission.

If the comment is "we will see pre/post being just derived from programs",
this has been suggested in Eiffel context before, and is easily answered
by referring to the proper discipline: psychology, management, and
sociology of the workplace, not DbC. This is an issue of management,
and of attitude, not of DbC.


> (He was ready to debunk use of exceptions, to dismiss design of Ada I/O.

A similar comment on omitting exceptions might be circulated with Parasail,
I think. The same Robert Dewar, lecturing at MIT, praises exceptions,
comparing them to C's solution (checking return values all along).

Could this conviction and readiness to debunk exceptions be
a consequence of running a particular business, the small and
profitable niche  of immensely well funded high tech?

> People could do anything in order to save dynamic checks! (:-))

Can you report the gist of the argument?

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 22.06.12 18:35, Dmitry A. Kazakov wrote:
> On Fri, 22 Jun 2012 17:52:53 +0200, Georg Bauhaus wrote:
> 
>> The world happens, including computers, and the laws of logic are
>> far too insufficient to capture it.
> 
> Great, now we are in cordial agreement that dynamic checks of Ada 2012 are
> in breach with laws of logic! (:-))

Anything dynamic (non-static, or otherwise unpredictable) is
demonstrably right or wrong, after the fact. Sometimes with the
help of the post-hoc fallacy :-)

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 22 Jun 2012 18:45:16 +0200, Georg Bauhaus wrote:

> On 22.06.12 17:05, Dmitry A. Kazakov wrote:
>> On Fri, 22 Jun 2012 16:30:52 +0200, Georg Bauhaus wrote:
>> 
>>> On 22.06.12 14:43, Dmitry A. Kazakov wrote:
>>>> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote:
>>>>
>>>>> On 22.06.12 09:23, Dmitry A. Kazakov wrote:
>>>>>> Neither #1 nor #2 is defendable.
>>>>>
>>>>> Maybe dynamic checking is not defendable when the attack is
>>>>> based on some biased, and, frankly, narrow set of assumptions.
>>>>
>>>> Sure, the most effective defence is just not to take any position. You
>>>> might get exposed otherwise.
>>>
>>> Who isn't taking a position?
>> 
>> You.
> 
> I don't think that #1 xor #2 can be the basis of a meaningful
> discussion of DbC, because of the frames of reference.

#1 and #2 are mutually exclusive and complete. The rest is hand waving.

>> (He was ready to debunk use of exceptions, to dismiss design of Ada I/O.
> 
> A similar comment on omitting exceptions might be circulated with Parasail,
> I think. The same Robert Dewar, lecturing at MIT, praises exceptions,
> comparing them to C's solution (checking return values all along).
> 
> Could this conviction and readiness to debunk exceptions be
> a consequence of running a particular business, the small and
> profitable niche of immensely well funded high tech?

Robert Dewar seem to consider exceptions as manifestations of contract
violations. That immediately leads to rejection of exceptions, on the
obvious basis that the contracts must be respected. The next step is, of
course, that any program raising exceptions is illegal. This is the point
where the proponents of #2 providently disconnect, because legality is to
be checked statically.

>> People could do anything in order to save dynamic checks! (:-))
> 
> Can you report the gist of the argument?

I cannot honestly summarize his argument, because as I said, there is no
way to make it. It is inconsistent.

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

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Jeffrey Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message 
news:js01ol$76g$1@adenine.netfront.net...
> On 06/21/2012 01:37 PM, Randy Brukardt wrote:
>>
>> "Hard-coded checks" prevent the compiler from doing call-site 
>> optimizations
>> and tools from doing much of anything. They should be avoided. The 
>> solution
>> is the pragma I showed earlier:
>>
>>     pragma Assertion_Policy (Pre =>  Check,
>>                                             Pre'Class =>  Check,
>>                                             Static_Predicate =>  Check,
>>                                             Dynamic_Predicate =>  Check);
>>
>> put in *every* reusable package spec. They still can suppress the checks 
>> by
>> manually deleting the pragma, but it will render command line switches 
>> and
>> IDE checkboxes ineffective. And if they do delete the pragma, they've
>> intentionally shot themselves in the foot, and it is no longer your (the
>> package maintainers) problem. (Unless of course they want to spend extra
>> $$$.)
>
> Interesting. I wasn't aware of checks that can't be overridden by compiler 
> options, and will be surprised if most compilers don't include a way to 
> override these as well.

A compiler option is essentially equivalent (or should be) to a 
configuration pragma. Nested pragmas override any outer pragmas (or 
switches). The same is true for Suppress/Unsuppress.

You might be right, but that would be evil in the extreme. This pragma is 
used in the same way that Unsuppress is used for other checks, and 
overrriding an explicit Unsuppress would be very, very bad (as it would 
cause code to malfunction). The same is true here.

                                 Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net...
> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
>> ...
>>> 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.
>>
>> You're right, but I don't see any inconsistency. They are clearly #1, and
>> that includes all of the existing Ada checks as well.
>
> If you take a stance on #1, then checking stack full is no more evaluation
> of the precondition, which does not depend on the stack state anymore, as
> it of course should be. So the "true" precondition is just: True.

Huh? This makes no sense whatsoever.

We can't require static detection of precondition failures any more than we 
can demand static detection of range violations. And Ada *always* has had 
dynamic preconditions:

    procedure New_Line (Spacing : in Positive_Count := 1);

Here, the precondition is "Spacing in Positive_Count". Your contention that 
a dynamic expression cannot be a precondition is the same as saying that no 
parameter can include a range (and thus ought be written as Count'Base 
above).

...
> And implementations leaking into declarations is certainly a very bad 
> idea.

This is NOT implementation; it's part of the contract. For the vast majority 
of subprograms, callers aren't supposed to call routines such that an 
exception is raised; it represents a bug. The only question is to whether 
those conditions are expressed in executable terms or in comments.

For instance, the containers have operations like:

procedure Insert_Space (Container : in out Vector;
                        Before    : in     Extended_Index;
                        Count     : in     Count_Type := 1);

If Before is not in the range First_Index (Container) .. Last_Index 
(Container) + 1, then Constraint_Error is propagated. If Count is 0, then 
Insert_Space does nothing. Otherwise, it computes the new length NL as the 
sum of the current length and Count; if the value of Last appropriate for 
length NL would be greater than Index_Type'Last, then Constraint_Error is 
propagated. {more text here}

It would have much better if this was written as:
procedure Insert_Space (Container : in out Vector;
                        Before    : in     Extended_Index;
                        Count     : in     Count_Type := 1)
    with Pre => (if Before not in First_Index (Container) .. Last_Index 
(Container) + 1 or else
                           Container.Length  > Index_Type'Last - Count then 
raise Constraint_Error);

The latter is less likely to be misinterpreted, it still can be checked at 
run-time, the compiler can use it to completely eliminate redundant checks 
(which cannot be done for checks in the body absent of inlining -- which is 
usually a bad idea), and static analysis tools (and compilers, for that 
matter) can detect and complain about cases where the checks are known to 
fail (that is, where the program has bugs). And you get all of this without 
peeking into the body of the subprogram.
We can't require the latter: it's beyond the state of the art to do that in 
most cases, but by doing this at runtime now, we get people writing these 
conditions so that as the state of the art improves more can be done for 
static detection. There never will be any static detection of conditions 
written as comments!

Also note that in the above, this precondition is NOT part of the body 
(implementation) of the subprogram. This is required of all 
implementations -- it's part of the contract, not the part that varies 
between implementations. As such, it makes the most sense to write it as 
part of the contract.

...
> Neither #1 nor #2 is defendable.

Nothing you say on this topic makes any sense, at least from an Ada 
perspective. Here you are saying that Ada's entire design and reason for 
existing is "not defendable" (that's the separation of specification from 
implementation). How your ideal language might work is irrelevevant in this 
forum. Please talk about Ada, not impossible theory.

                                         Randy.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net...
>> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
>>> ...
>>>> 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.
>>>
>>> You're right, but I don't see any inconsistency. They are clearly #1, and
>>> that includes all of the existing Ada checks as well.
>>
>> If you take a stance on #1, then checking stack full is no more evaluation
>> of the precondition, which does not depend on the stack state anymore, as
>> it of course should be. So the "true" precondition is just: True.
> 
> Huh? This makes no sense whatsoever.
> 
> We can't require static detection of precondition failures any more than we 
> can demand static detection of range violations.

You seem to imply that value in the range is a precondition of the
operation constrained to that range. This is wrong. If S is a subtype of T
then the precondition is

   X in T

The postcondition is

   (X in S and <something>) or (X not in S and Constraint_Error propagated)

> And Ada *always* has had dynamic preconditions:
> 
>     procedure New_Line (Spacing : in Positive_Count := 1);

The precondition here is Spacing in Positive_Count'Base because the
behavior of New_Line is *defined* when Spacing is not in
Positive_Count'Range.

   New_Line(0) 

is a *legal* Ada program.

>> And implementations leaking into declarations is certainly a very bad 
>> idea.
> 
> This is NOT implementation; it's part of the contract.

OK, you switched from #1 to #2.

>> Neither #1 nor #2 is defendable.
> 
> Nothing you say on this topic makes any sense, at least from an Ada 
> perspective. Here you are saying that Ada's entire design and reason for 
> existing is "not defendable"

Why entire? Dynamic correctness checks are not defendable, as demonstrated
on numerous examples.

> (that's the separation of specification from implementation).

On the contrary, it is #1 which breaks that separation. #2 it is just flat
wrong.

> How your ideal language might work is irrelevevant in this forum.

It is not mine language. It is a methodology of defining and proving
program correctness as introduced by Dijkstra. It applies to all languages
without exemption.

> Please talk about Ada, not impossible theory.

The only impossible theory here is about meaning of dynamically checked
preconditions, e.g. #1 or #2? That is indeed impossible, because
inconsistent. Otherwise Dijkstra's approach works pretty well with any
language, e.g. SPARK does for Ada.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 23.06.12 01:08, Dmitry A. Kazakov wrote:
>> And Ada*always*  has had dynamic preconditions:
>> >
>> >       procedure New_Line (Spacing : in Positive_Count := 1);
> The precondition here is Spacing in Positive_Count'Base because the
> behavior of New_Line is*defined*  when Spacing is not in
> Positive_Count'Range.
>
>     New_Line(0)
>
> is a*legal*  Ada program.
  
The behavior of New_Line is not relevant, because New_Line's body
is not performed when "Spacing not in Positive_Count". New_Line does not
behave, because it can't; it also does not propagate anything from its
body. The program does behave without New_Line being called.
But that's the point.

Although there is a post-state in the program, the subprogram New_Line
does not get a chance to run, hence cannot establish its (its!)
postcondition.  Its postcondition is conceptually different
from the condition the program is in, at the place after the New_Line
statement.

When New_Line (Spacing) where

  Spacing in Positive_Count'Base

is legal Ada, then still New_Line (Spacing) where

  Spacing not in Positive_Count

is a contract violation, duly noted by an Ada program executing
properly.

The notions of precondition seem to differ.

Looking at assignments of variables before a call and then calling
this set the precondition, and then looking at assignments and exceptions
after the call, if any, and calling that set the postcondition,
is too meaningless and narrow to be equated to DbC.

There are two separate kinds of rules working here.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sat, 23 Jun 2012 12:46:56 +0200, Georg Bauhaus wrote:

> On 23.06.12 01:08, Dmitry A. Kazakov wrote:
>>> And Ada*always*  has had dynamic preconditions:
>>> >
>>> >       procedure New_Line (Spacing : in Positive_Count := 1);
>> The precondition here is Spacing in Positive_Count'Base because the
>> behavior of New_Line is*defined*  when Spacing is not in
>> Positive_Count'Range.
>>
>>     New_Line(0)
>>
>> is a*legal*  Ada program.
>   
> The behavior of New_Line is not relevant,

It is OK if New_Line(0) would reboot the computer?

New_Line(0) is not straight legal, it not an error in the classification of
errors (RM 1.1.5).

Compare: a contract violation is an *unbounded ERROR*.

Aside. If you could estimate the effect of a contract violation, in order
to make the case for a bounded error, that would not save the idea of
checking either. Because, of course, in that case you also could detect the
violation itself, which is a much simpler task than tracking all possible
consequences down.

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

Re: about the new Ada 2012 pre/post conditions

[AdaMagica]

On Saturday, June 23, 2012 1:01:17 PM UTC+2, Dmitry A. Kazakov wrote:
> It is OK if New_Line(0) would reboot the computer?

Really, I do not understand your argument.
If the argument of New_Line is 0, the procedure is not even called, so its body is irrelevant. The evaluation of the argument raises Constraint_Error as defined in the RM. How could it reboot the computer? The consequences of CE are well-defined.

So what? I think I'm not the only one who is often lost in following your arguments.

> New_Line(0) is not straight legal, it not an error in the classification of
> errors (RM 1.1.5).

What? You surely have read 1.1.5(5)?
> 
> Compare: a contract violation is an *unbounded ERROR*.
> 
> Aside. If you could estimate the effect of a contract violation, in order
> to make the case for a bounded error, that would not save the idea of
> checking either. Because, of course, in that case you also could detect the
> violation itself, which is a much simpler task than tracking all possible
> consequences down.
> 
> -- 
> Regards,
> Dmitry A. Kazakov
> http://www.dmitry-kazakov.de

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sat, 23 Jun 2012 10:46:35 -0700 (PDT), AdaMagica wrote:

> On Saturday, June 23, 2012 1:01:17 PM UTC+2, Dmitry A. Kazakov wrote:
>> It is OK if New_Line(0) would reboot the computer?
> 
> Really, I do not understand your argument.

It was Georg's argument. I only asked a simple question. Is the behavior of
New_Line defined for the case when the argument is 0, or not? Possible
answer is either "yes" or "no."

> If the argument of New_Line is 0, the procedure is not even called, so its
> body is irrelevant.

If New_Line is not called, why this construct is named "procedure call"?

Let New_Line(1) were inlined would you also argue that its body is not
called?

Would be an implementation checking the constraint within the body illegal?

How do you know if the given piece of code raising an exception does or
does not belong to the body?

How all this could be relevant to the semantics of New_Line and its
contract describing this semantics?

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 23.06.12 13:01, Dmitry A. Kazakov wrote:
> Compare: a contract violation is an *unbounded ERROR*.

Do you mean, I should imagine a contract violation that,
when checks are turned off, result in erroneous execution?

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote:

> On 23.06.12 13:01, Dmitry A. Kazakov wrote:
>> Compare: a contract violation is an *unbounded ERROR*.
> 
> Do you mean, I should imagine a contract violation that,
> when checks are turned off, result in erroneous execution?

The effect of contract violation is unbounded because not contracted.

When you say that something behaves in a certain way under specified
conditions, e.g. raises exception when out of range, that is the contract.
 
1. violation => nothing guaranteed
2. effect is bounded => these bounds are in the contract

1+2 = contract violation is necessarily *equivalent* to undefined behavior.

What is so difficult about this?

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 24.06.12 18:06, Dmitry A. Kazakov wrote:
> On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote:
>
>> On 23.06.12 13:01, Dmitry A. Kazakov wrote:
>>> Compare: a contract violation is an *unbounded ERROR*.
>>
>> Do you mean, I should imagine a contract violation that,
>> when checks are turned off, result in erroneous execution?
>
> The effect of contract violation is unbounded because not contracted.

The effect of a contract violation is part of the contract between
client and supplier, by definition, even when it appears to be rather
trivial:

When working under the rules of DbC, a violation that is detected by
the contract checking system must engage the exception mechanism.
This mechanism is supposed to entail a rescuing action, recursively,
or a bail out---and there is LRM 11.6, anyway.

So,

1. if X0 might violate the contract of ADT[*] Y, then X0, or some Xn
    on X0's behalf, must handle the effect of the violation,
    as outlined. There is a guarantee that every (efficiently decidable,
    let us say) violation is detected if (a) checks are on, or
    (b) the proof obligation has had the effect of showing that there
     is no violation, for all inputs.
  
2. Effects of exceptional situations may or may not be expressible
    at all, due to the nature of Ada exceptions that, unfortunately,
    cover both "exceptional situation" and "non-local transfer of
    control". In "exceptional situation", there may not be any form of
    control because this is what the word "exception" means in this
    case: the program can control all situations except those whose
    effects are not known when designing. We would be trying to handle
    Program_Error in advance.


> When you say that something behaves in a certain way under specified
> conditions, e.g. raises exception when out of range, that is the contract.
>
> 1. violation =>  nothing guaranteed
> 2. effect is bounded =>  these bounds are in the contract
>
> 1+2 = contract violation is necessarily *equivalent* to undefined behavior.
>
> What is so difficult about this?

It is a theory in a different universe of notions.


__
[*] A contract as in Design by Contract applies to ADTs only, somewhat like
the full set of different aspects is made for ADTs in Ada 2012.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote:

> On 24.06.12 18:06, Dmitry A. Kazakov wrote:
>> On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote:
>>
>>> On 23.06.12 13:01, Dmitry A. Kazakov wrote:
>>>> Compare: a contract violation is an *unbounded ERROR*.
>>>
>>> Do you mean, I should imagine a contract violation that,
>>> when checks are turned off, result in erroneous execution?
>>
>> The effect of contract violation is unbounded because not contracted.
> 
> The effect of a contract violation is part of the contract between
> client and supplier,

Like the actual effect of violation of the expected effect of violation of
the contract.

Credo quia absurdum

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote:

> It is a theory in a different universe of notions.

http://en.wikipedia.org/wiki/Paradox_of_the_Court 

As Littlewood once said, self-referential jokes are fun. Further reading on
the subject of your universe:

http://www.cut-the-knot.org/selfreference/index.shtml

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 25.06.12 09:48, Dmitry A. Kazakov wrote:
> On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote:
> 
>> On 24.06.12 18:06, Dmitry A. Kazakov wrote:
>>> On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote:
>>>
>>>> On 23.06.12 13:01, Dmitry A. Kazakov wrote:
>>>>> Compare: a contract violation is an *unbounded ERROR*.
>>>>
>>>> Do you mean, I should imagine a contract violation that,
>>>> when checks are turned off, result in erroneous execution?
>>>
>>> The effect of contract violation is unbounded because not contracted.
>>
>> The effect of a contract violation is part of the contract between
>> client and supplier,
> 
> Like the actual effect of violation of the expected effect of violation of
> the contract.
> 
> Credo quia absurdum

That's what true exceptions always are.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 25.06.12 10:08, Dmitry A. Kazakov wrote:
> On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote:
> 
>> It is a theory in a different universe of notions.
> 
> http://en.wikipedia.org/wiki/Paradox_of_the_Court 

Indeed, it helps to remember that logicians and mathematicians
have learned that logic and mathematics cannot justify themselves.

We have to do something. DbC is something. Better than nothing.

So logic and mathematics become tools that happen to exist,
tools in the hands of designers whose goals transcend both
mathematics and logics into the realm of the physical
world of computer based systems. DbC is a best effort thing like
every system building effort.

> As Littlewood once said, self-referential jokes are fun. Further reading on
> the subject of your universe:
> 
> http://www.cut-the-knot.org/selfreference/index.shtml

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote:

> On 25.06.12 10:08, Dmitry A. Kazakov wrote:
>> On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote:
>> 
>>> It is a theory in a different universe of notions.
>> 
>> http://en.wikipedia.org/wiki/Paradox_of_the_Court 
> 
> Indeed, it helps to remember that logicians and mathematicians
> have learned that logic and mathematics cannot justify themselves.

No, they never ever did that. From very beginning mathematicians used
axiomatic approach instead. What they did, was constructing frameworks
within which one could not deduce both A and not A.

> We have to do something. DbC is something. Better than nothing.

Is SPARK nothing? Is strong typing nothing?

But you seemingly did not read what I wrote earlier. There is either #1 or
#2. #2 is inconsistent and thus is out. Left is #1: so-called Ada 2012
preconditions simply are misplaced implementations. This is flawed and
misleading, but not because of some cosmogonic problems like your
Promethean trampling laws of logic. Just a much more humble ignoring
principles of good language design. Nothing really new.

> DbC is a best effort thing like every system building effort.

How are you going to prove this, if "DbC" contradicts logic itself?

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 25.06.12 13:54, Dmitry A. Kazakov wrote:

>> Indeed, it helps to remember that logicians and mathematicians
>> have learned that logic and mathematics cannot justify themselves.
> 
> No, they never ever did that.

They tried, though. I didn't even say that they did.

Frege thought, for some time, that he had done.
Russel sent a correction. Hilbert did not give up, though:

http://en.wikipedia.org/wiki/File:HilbertGrab.jpg

 WIR M�SSEN WISSEN
 WIR WERDEN WISSEN

Optimism!

>> We have to do something. DbC is something. Better than nothing.
> 
> Is SPARK nothing?

Try

 new Data'(Size => More_than_4k);

> Is strong typing nothing?

Until Ada 2012, there was nothing in addition to the strong type
system of Ada 2005.

> But you seemingly did not read what I wrote earlier. There is either #1 or
> #2.

I have tried to explain that neither #1 nor #2 are applicable
because they assume applicability of exhaustive formal analysis
to general program design (not programs). Wrong frame of reference.

DbC does not claim to be a replacement for a type system.

>> DbC is a best effort thing like every system building effort.
> 
> How are you going to prove this, if "DbC" contradicts logic itself?

A program that is known to be covered entirely by logic
is really an exception. Its notion, however, sells and is
a good, justifiable tool in political rhetoric, IMHO.

Proving things in a DbC framework is similar to proving things
with the help of more than Ada, as is done when using SPARK.
If we can't have a more proof friendly type system, let's have
at least aspects. Proofs isn't everything. Writing programs
for system is.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 25.06.12 14:39, Georg Bauhaus wrote:
>> > But you seemingly did not read what I wrote earlier. There is either #1 or
>> > #2.
> I have tried to explain that neither #1 nor #2 are applicable
> because they assume applicability of exhaustive formal analysis
> to general program design (not programs). Wrong frame of reference.

Let me ad this:

  procedure P (X : S) is null;

is o.K., but

  procedure P (X : S'Base)
    with  Pre => ...
  is null;

is not legal.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 14:39:06 +0200, Georg Bauhaus wrote:

> On 25.06.12 13:54, Dmitry A. Kazakov wrote:
> 
>>> Indeed, it helps to remember that logicians and mathematicians
>>> have learned that logic and mathematics cannot justify themselves.
>> 
>> No, they never ever did that.
> 
> They tried, though. I didn't even say that they did.
> 
> Frege thought, for some time, that he had done.
> Russel sent a correction. Hilbert did not give up, though:

Not at all. All three used axiomatic approach. None of them would ever seek
to justify logic by means of logic.

>>> We have to do something. DbC is something. Better than nothing.
>> 
>> Is SPARK nothing?
> 
> Try
> 
>  new Data'(Size => More_than_4k);

How does this make SPARK null and void?

>> Is strong typing nothing?
> 
> Until Ada 2012, there was nothing in addition to the strong type
> system of Ada 2005.

And the point is? Some hidden Ada version between 2005 and 2012?

>> But you seemingly did not read what I wrote earlier. There is either #1 or
>> #2.
> 
> I have tried to explain that neither #1 nor #2 are applicable
> because they assume applicability of exhaustive formal analysis
> to general program design (not programs).

So #2 does not apply, I missed where you agreed with me on that.

Ergo, Ada 2012 preconditions are not contract (not #2). 

Please confirm this, and we will proceed to #1 and whether (not #2 is
equivalent to #1). 

>>> DbC is a best effort thing like every system building effort.
>> 
>> How are you going to prove this, if "DbC" contradicts logic itself?
> 
> A program that is known to be covered entirely by logic
> is really an exception.

Please, show this without logic.
 
> Proving things in a DbC framework is similar to proving things
> with the help of more than Ada, as is done when using SPARK.

No. You claimed that what you call DbC does not obey laws of logic. I am
eager to learn how are you going to "prove things" without these laws.

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

Re: about the new Ada 2012 pre/post conditions

[stefan-lucks]

I am not sure if I can cool down this heated discussion, but I'll give it 
a try. 

On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:

> On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote:
> 
> > Indeed, it helps to remember that logicians and mathematicians
> > have learned that logic and mathematics cannot justify themselves.
> 
> No, they never ever did that. From very beginning mathematicians used
> axiomatic approach instead. What they did, was constructing frameworks
> within which one could not deduce both A and not A.

A bit off topic -- but this is not quite true. 

Firstly, the axiomatic approach has become mathematical mainstream only 
since about the times of David Hilbert. The "very beginning" of 
Mathematics and Logic are quite a bit earlier. ;-)

Secondly, Hilbert's program was to construct frameworks being both 
complete (all correct conclusions should be deducible) and one should not 
be able to deduce both A and not A. Kurt Goedel eventually showed that 
this is *logically* impossible. 

But back to the real topic. 

> Is SPARK nothing? Is strong typing nothing?
>
> But you seemingly did not read what I wrote earlier. There is either #1 or
> #2. 

This the axiom that *you* choose to start with. Starting from there, your 
reasoning may be logically correct.

But actually, by choosing that axiom as your logical starting point, you 
have made several logical errors by yourself. 


*Firstly*, you don't seem to separate between syntax and semantic. 

Ada 2012 provides pre- and postconditions (and also invariants) allow to 
*specify* contracts. That is a great advantage over writing more or less 
informal contracts -- and even to SPARK's annotations inside Ada comments.

This is a syntax for specifications, no more, no less! What is wrong with 
that syntax? If you like SPARK, you should welcome it!

So much about syntax, now comes the semantic. 


*Secondly*, you seem to overlook that there are three semantical options, 
rather than the two you mention:

  1 ignore the conditions 

  2 check them dynamically at run time 

  3 prove them statically at compile time

The language requires the compiler to support the first two, but the 
language allows the third one just as well. I anticipate that we will soon 
see tools to support proving Ada 2012 annotations statically. Even SPARK 
may soon support the Ada 2012 syntax for its annotations.


*Thirdly*, you seem to assume that a tool that can be used in a 
destructive way cannot also be used properly.

The support for the second option is such a tool. I agree with you, any 
program that claims some preconditions, postconditions and invariants 
should stop and must be fixed when any such check fails. Silently handling 
the exception and then continuing is 

  - a logical contradiction in itself, and also

  - the result from some lousy programming practice.

There is no justification for handling the exception instead of fixing the 
flaw!

But the same tool can properly be used for debugging and testing -- if any 
assertion fails, and you detect this at run time, write all relevant 
details into a log file, stop the program, and fix the bug. Which is what 
you try do do without dynamic checks, or by writing your 

  pragma Assert(...)

in current Ada, just as well!

Used that way, dynamic checks in Ada 2012 will ease testing and debugging. 
Which is good!



-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 16:08:01 +0200, stefan-lucks@see-the.signature wrote:

> I am not sure if I can cool down this heated discussion, but I'll give it 
> a try. 
> 
> On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote:
>> 
>>> Indeed, it helps to remember that logicians and mathematicians
>>> have learned that logic and mathematics cannot justify themselves.
>> 
>> No, they never ever did that. From very beginning mathematicians used
>> axiomatic approach instead. What they did, was constructing frameworks
>> within which one could not deduce both A and not A.
> 
> A bit off topic -- but this is not quite true. 
> 
> Firstly, the axiomatic approach has become mathematical mainstream only 
> since about the times of David Hilbert. The "very beginning" of 
> Mathematics and Logic are quite a bit earlier. ;-)

Euclid

> Secondly, Hilbert's program was to construct frameworks being both 
> complete (all correct conclusions should be deducible) and one should not 
> be able to deduce both A and not A. Kurt Goedel eventually showed that 
> this is *logically* impossible. 

Hilbert's program by no means was intended to justify logic or mathematics
themselves. This is outright wrong.

>> Is SPARK nothing? Is strong typing nothing?
>>
>> But you seemingly did not read what I wrote earlier. There is either #1 or
>> #2. 
> 
> This the axiom that *you* choose to start with. Starting from there, your 
> reasoning may be logically correct.

If Ada precondition is neither implementation (#1) nor
specification/contract (#2) then what is it? Since nobody ever came with
#3, I considered only #1 and #2.
 
> *Firstly*, you don't seem to separate between syntax and semantic. 

I said nothing about the syntax. It could be better, but syntax is always
the most difficult part.

> *Secondly*, you seem to overlook that there are three semantical options, 
> rather than the two you mention:
> 
>   1 ignore the conditions 
> 
>   2 check them dynamically at run time 
> 
>   3 prove them statically at compile time

I didn't:

Assuming #1, only no.2 is possible. #1 <=> no.2

Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or
no.2.

One *cannot* mix no.1/3 with no.2, that is what upsets me.

> Even SPARK may soon support the Ada 2012 syntax for its annotations.

That is OK to me, however, considering syntax I wished a clearer separation
of pre-/post-conditions from other declarations. But since GPS rules, I
suppose it would not be much difficult to have a view cutting
pre-/post-conditions off and displaying them in a side-by-side window
scrolled upon mouse hovering etc.

> *Thirdly*, you seem to assume that a tool that can be used in a 
> destructive way cannot also be used properly.

In this particular case (#2 + no.3) we wave a very strong evidence:
accessibility checks. It was a disaster.

> The support for the second option is such a tool. I agree with you, any 
> program that claims some preconditions, postconditions and invariants 
> should stop and must be fixed when any such check fails. Silently handling 
> the exception and then continuing is 
> 
>   - a logical contradiction in itself, and also
> 
>   - the result from some lousy programming practice.
> 
> There is no justification for handling the exception instead of fixing the 
> flaw!
> 
> But the same tool can properly be used for debugging and testing -- if any 
> assertion fails, and you detect this at run time, write all relevant 
> details into a log file, stop the program, and fix the bug.

No objection whatsoever. I covered this case earlier. It is OK to check
dynamically under the condition that the checker is an *independent*
program. A debugger, checker, reasonably protected Ada run-time verifying
preconditions and *handling* failed checks is perfectly consistent and
advisable.

That clearly precludes no.2: handling is within the checker, checker is
outside the testee.

And, very importantly, we want to contract exceptions some day, don't we?
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 16:36:09 +0200, Dmitry A. Kazakov wrote:

> Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or
> no.2.

typo error: no.1 or 3

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

Re: about the new Ada 2012 pre/post conditions

[stefan-lucks]

On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:

> Hilbert's program by no means was intended to justify logic or mathematics
> themselves. This is outright wrong.

Hilbert's program was an attempt to re-build the very foundations of 
Mathematics. No more, no less. See 
<http://en.wikipedia.org/wiki/Hilbert%27s_program>. 

> If Ada precondition is neither implementation (#1) nor
> specification/contract (#2) then what is it? 

A syntax for specifications. 

> I said nothing about the syntax. It could be better, but syntax is always
> the most difficult part.

OK. 

> > *Secondly*, you seem to overlook that there are three semantical options, 
> > rather than the two you mention:
> > 
> >   1 ignore the conditions 
> > 
> >   2 check them dynamically at run time 
> > 
> >   3 prove them statically at compile time
> 
> I didn't:
> 
> Assuming #1, only no.2 is possible. #1 <=> no.2
> 
> Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or
> no.2.
> 
> One *cannot* mix no.1/3 with no.2, that is what upsets me.

But you are not locked into either option 1, 2, or 3, you can choose, 
without having to change the language, or to rewrite a single character 
of your program source. 

> > Even SPARK may soon support the Ada 2012 syntax for its annotations.
> 
> That is OK to me, however, considering syntax I wished a clearer separation
> of pre-/post-conditions from other declarations. But since GPS rules, I
> suppose it would not be much difficult to have a view cutting
> pre-/post-conditions off and displaying them in a side-by-side window
> scrolled upon mouse hovering etc.

That is a matter of taste. In any case, emacs rules. ;-)

> > *Thirdly*, you seem to assume that a tool that can be used in a 
> > destructive way cannot also be used properly.
> 
> In this particular case (#2 + no.3) we wave a very strong evidence:
> accessibility checks. It was a disaster.

I agree that dynamic accessibility checks have failed to become a good 
tool for reliable program development. But the standard requires no 
compiler switch to allow them turning on and off on demand -- in contrast 
to assertions and Ada 2012 conditions.I.e., the accessibility checks are 
really part of the language, the checks are a tool that you have the 
freedom to use or not to use!

> No objection whatsoever. I covered this case earlier. It is OK to check
> dynamically under the condition that the checker is an *independent*
> program. A debugger, checker, reasonably protected Ada run-time verifying
> preconditions and *handling* failed checks is perfectly consistent and
> advisable.

Agreed. 

> That clearly precludes no.2: handling is within the checker, checker is
> outside the testee.

Well, this separation is ideal. But most of the time, a testee that 
discovers itself being in a faulty state (and that is, what a failed 
dynamic check actually reveals), the testee is still able to write some 
information to a log file. Sure, you can construct or find the odd 
counterexample -- but in practice almost all the time this approach works.
(OK, I am assuming your system allows to write some log output at all.) 

> And, very importantly, we want to contract exceptions some day, don't we?

Sure! So what? 

Ada.Assertions.Assertion_Error is one exception like Constraint_Error or 
the like. Either, you prove that this or that exception will not be 
raised. Or you claim that such an exception is not raised. If it is 
actually raised this is a violation of the contract. Which is a big deal 
for, say, Constraint_Error, but not for Ada.Assertions.Assertion_Error ... 
the exception that indicates the violation of a contract, anyway. (Assuming 
that Ada.Assertions.Assertion_Error is not raised manually -- but no sane 
programmer would do that.)

Actually, there is one exception that is difficult to specify. It is our
old fellow 

    Storage_Error. 

On the level of source code analysis, you 
actually cannot prove that this exception will not be raised. 




-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 25.06.12 15:19, Dmitry A. Kazakov wrote:
> All three used axiomatic approach. None of them would ever seek
> to justify logic by means of logic.

My choice of "justify" was bad. I'll leave it at Stefan Lucks' replies,
only noting that what mathematicians did when working in math mode
is different from what they did when seeking the ultimate foundation
of how what they did might be really true, a certainty.

>>  new Data'(Size => More_than_4k);
> 
> How does this make SPARK null and void?

It's void for Ada. It's really good for some programs.

The point is that with Ada 2012 assertions, now there is something.

> Ergo, Ada 2012 preconditions are not contract (not #2). 

"Ergo" is an indication of accepting the frames of reference
for #1 and #2, and the connotation of a notional divide.

Assertions are (1) a tool for best effort and (2) need not
even relate to what some body does. They should, of course.
That's in the hands of the programmers, though. Malicious
programmers can write Pre => F (X) and then, in bodies, write
something that corresponds to not F (X). (Note: corresponds to.
That could be "not F(X)".)


>>>> DbC is a best effort thing like every system building effort.
>>>
>>> How are you going to prove this, if "DbC" contradicts logic itself?
>>
>> A program that is known to be covered entirely by logic
>> is really an exception.
> 
> Please, show this without logic.

Again, bad choice of words.
There hardly is a situation qualified by complete formal knowledge
of a program. Stopping all programming that leads to such situations
is not acceptable. Improving the situation via DbC is, if only as
an educational effort in combination with good will.


>> Proving things in a DbC framework is similar to proving things
>> with the help of more than Ada, as is done when using SPARK.
> 
> No. You claimed that what you call DbC does not obey laws of logic.

I remember having said "transcend", also "insufficient", and "goal".
"Transcend" is different from "not obeying", in particular when
the subject of "transcend" is the human activity called "design",
not some ready made "program". "Transcend" may be a pompous euphemism,
or not.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 18:26:18 +0200, stefan-lucks@see-the.signature wrote:

> On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> Hilbert's program by no means was intended to justify logic or mathematics
>> themselves. This is outright wrong.
> 
> Hilbert's program was an attempt to re-build the very foundations of 
> Mathematics. No more, no less. See 
> <http://en.wikipedia.org/wiki/Hilbert%27s_program>. 

Right, and this had nothing to do with justification either logic or
mathematics by means of themselves. Such an epic task would rather be a job
for baron Muenchausen. Just scroll through the Hilbert's program list of
problems:

http://en.wikipedia.org/wiki/Hilbert_problems

>> If Ada precondition is neither implementation (#1) nor
>> specification/contract (#2) then what is it? 
> 
> A syntax for specifications. 

Syntax only?

>>> *Secondly*, you seem to overlook that there are three semantical options, 
>>> rather than the two you mention:
>>> 
>>>   1 ignore the conditions 
>>> 
>>>   2 check them dynamically at run time 
>>> 
>>>   3 prove them statically at compile time
>> 
>> I didn't:
>> 
>> Assuming #1, only no.2 is possible. #1 <=> no.2
>> 
>> Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or
>> no.2.
>> 
>> One *cannot* mix no.1/3 with no.2, that is what upsets me.
> 
> But you are not locked into either option 1, 2, or 3, you can choose, 
> without having to change the language, or to rewrite a single character 
> of your program source. 

Same syntax for things which are far more apart than just semantically
different. What a bizzare idea! You would be switching between contract
specification and implementation per compiler switch! Is this C
preprocessor or Ada?

>> That clearly precludes no.2: handling is within the checker, checker is
>> outside the testee.
> 
> Well, this separation is ideal. But most of the time, a testee that 
> discovers itself being in a faulty state (and that is, what a failed 
> dynamic check actually reveals), the testee is still able to write some 
> information to a log file. Sure, you can construct or find the odd 
> counterexample -- but in practice almost all the time this approach works.
> (OK, I am assuming your system allows to write some log output at all.) 

Tracing is OK, but what happens afterwards? If continuation is possible,
that requires some cleanup, rollback, retry etc, which has the goal of
putting the system into some definite state. This is not over before over.

>> And, very importantly, we want to contract exceptions some day, don't we?
> 
> Sure! So what? 

How are going to marry exceptions propagating from contracts with contracts
on exceptions? Some exceptions are more exceptional than others? Aren't we
fed up with Program_Error?
 
> Ada.Assertions.Assertion_Error is one exception like Constraint_Error or 
> the like. Either, you prove that this or that exception will not be 
> raised. Or you claim that such an exception is not raised. If it is 
> actually raised this is a violation of the contract. Which is a big deal 
> for, say, Constraint_Error, but not for Ada.Assertions.Assertion_Error ... 
> the exception that indicates the violation of a contract, anyway. (Assuming 
> that Ada.Assertions.Assertion_Error is not raised manually -- but no sane 
> programmer would do that.)
> 
> Actually, there is one exception that is difficult to specify. It is our
> old fellow 
> 
>     Storage_Error. 
> 
> On the level of source code analysis, you 
> actually cannot prove that this exception will not be raised.

Firstly, you if you don't want to prove anything about a certain exception,
you would add this exception to all contracts involved and take care about
exceptions of interest.

Secondly, you would rather prove conditionals, like: Storage_Error is not
propagated when given amount of memory is available in the specified pools.
This is good enough for most cases, which are not about any exact bound,
but about existence of such bound, i.e. about memory leak detection.

Thirdly, you would be able to provide axioms. E.g. for some complex
recursive operation, you could just specify the upper memory consumption
bound known to you from other sources, and let the prover to go with that
(the oracle).

I think conservative Storage_Errror proof is pretty doable. If you move the
upper bound a pair Kbytes upward it would eliminate most of problems.

We certainly could learn from Java mistakes rather than repeating them
(e.g. interfaces).

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

Re: about the new Ada 2012 pre/post conditions

[stefan-lucks]

On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:

> > Hilbert's program was an attempt to re-build the very foundations of 
> > Mathematics. No more, no less. See 
> > <http://en.wikipedia.org/wiki/Hilbert%27s_program>. 
> 
> Right, and this had nothing to do with justification either logic or
> mathematics by means of themselves. 

Hilbert was very explicit that he wanted to formalize *all* of mathematics 
axiomatically, and prove the whole formalization consistent. There is an 
interesting article <http://plato.stanford.edu/entries/hilbert-program/>. 

> Such an epic task would rather be a job for baron Muenchausen. 

Here we are in violent agreement. ;-)

The program was quite successful in making mathematicans re-think the 
foundations of their field. BUT it turned out that the required 
formalization of *all* of mathematics could not work, for the same reason 
Muenchhausen's famous trick would not work. So Hilbert's program was an 
epic failure!

In any case, this is quite off topic, and we need not discuss Hilbert's 
program in c.l.a.

> Same syntax for things which are far more apart than just semantically
> different. What a bizzare idea! You would be switching between contract
> specification and implementation per compiler switch! Is this C
> preprocessor or Ada?

There is a well-defined syntax for contracts, and you can choose between 
different ways to use them. But contracts are still contracts. No 
relationship to the C preprocessor.

> >> That clearly precludes no.2: handling is within the checker, checker is
> >> outside the testee.
> > 
> > Well, this separation is ideal. But most of the time, a testee that 
> > discovers itself being in a faulty state (and that is, what a failed 
> > dynamic check actually reveals), the testee is still able to write some 
> > information to a log file. Sure, you can construct or find the odd 
> > counterexample -- but in practice almost all the time this approach works.
> > (OK, I am assuming your system allows to write some log output at all.) 
> 
> Tracing is OK, but what happens afterwards? If continuation is possible,
> that requires some cleanup, rollback, retry etc, which has the goal of
> putting the system into some definite state. This is not over before over.

Don't do that! Emit your messages to to the log file and then terminate!

Or try to continue -- but you should never forget that any failed 
condition indicates a bug that must be fixed soon!

This feature may be misused by handling an Assertion_Error and then not 
fixing the bug. And this feature will be misused by some program authors. 

But then, what is more important:

  - Provide tools that support good software engineering practice?

or
  
  - Prohibit any tools that can be misused?

Dynamically checked contracts are such a tool. 

> How are going to marry exceptions propagating from contracts with contracts
> on exceptions? 

The contract must always state "Assertion error is not raised!" Anything 
else violates some contract, anyway. (But note that if contracts are not 
proven, they can be lies.)

> Some exceptions are more exceptional than others? Aren't we
> fed up with Program_Error?

What are your issues with Program_Error? I don't have any. 

> > Actually, there is one exception that is difficult to specify. It is our
> > old fellow 
> > 
> >     Storage_Error. 
> > 
> > On the level of source code analysis, you 
> > actually cannot prove that this exception will not be raised.
> 
> Firstly, you if you don't want to prove anything about a certain exception,
> you would add this exception to all contracts involved and take care about
> exceptions of interest.

So you just add "can raise Storage_Error" to any contract? (Maybe 
implicitly.)

> Secondly, you would rather prove conditionals, like: Storage_Error is not
> propagated when given amount of memory is available in the specified pools.
> This is good enough for most cases, which are not about any exact bound,
> but about existence of such bound, i.e. about memory leak detection.

You are so violately against dynamically checked conditions ... and then 
you propose some heuristic that you just claim to be "good enough for most 
cases"?

> Thirdly, you would be able to provide axioms. E.g. for some complex
> recursive operation, you could just specify the upper memory consumption
> bound known to you from other sources, and let the prover to go with that
> (the oracle).
> 
> I think conservative Storage_Error proof is pretty doable. If you move the
> upper bound a pair Kbytes upward it would eliminate most of problems.

Good luck with any recursive program.

And (I am sure you know this) any approach to really prove upper bounds 
on the storage requirements would imply to solve the Halting Problem.

> We certainly could learn from Java mistakes rather than repeating them
> (e.g. interfaces).

Which is probably why Ada so far has no contracted exceptions. Not that 
they cannot be done -- but nobody knows how to write such contracts that 
they really become useful.



-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote:

> On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> Same syntax for things which are far more apart than just semantically
>> different. What a bizzare idea! You would be switching between contract
>> specification and implementation per compiler switch! Is this C
>> preprocessor or Ada?
> 
> There is a well-defined syntax for contracts, and you can choose between 
> different ways to use them. But contracts are still contracts. No 
> relationship to the C preprocessor.

They are contracts when checked statically and implementations when checked
dynamically. It is like

   #define is :=

>>>> That clearly precludes no.2: handling is within the checker, checker is
>>>> outside the testee.
>>> 
>>> Well, this separation is ideal. But most of the time, a testee that 
>>> discovers itself being in a faulty state (and that is, what a failed 
>>> dynamic check actually reveals), the testee is still able to write some 
>>> information to a log file. Sure, you can construct or find the odd 
>>> counterexample -- but in practice almost all the time this approach works.
>>> (OK, I am assuming your system allows to write some log output at all.) 
>> 
>> Tracing is OK, but what happens afterwards? If continuation is possible,
>> that requires some cleanup, rollback, retry etc, which has the goal of
>> putting the system into some definite state. This is not over before over.
> 
> Don't do that! Emit your messages to to the log file and then terminate!

Contract violation => terminate. Exceptional state => recover.

> But then, what is more important:
> 
>   - Provide tools that support good software engineering practice?
> 
> or
>   
>   - Prohibit any tools that can be misused?
> 
> Dynamically checked contracts are such a tool. 

A wrench sold as shoe polish.

>>> Actually, there is one exception that is difficult to specify. It is our
>>> old fellow 
>>> 
>>>     Storage_Error. 
>>> 
>>> On the level of source code analysis, you 
>>> actually cannot prove that this exception will not be raised.
>> 
>> Firstly, you if you don't want to prove anything about a certain exception,
>> you would add this exception to all contracts involved and take care about
>> exceptions of interest.
> 
> So you just add "can raise Storage_Error" to any contract? (Maybe 
> implicitly.)

Contracts will be inheritable. I don't know how it goes with aspects, never
understood what they are good for, but true contracts are inherited while
possibly weakening pre- and strengthening post-conditions (LSP).

Another necessary contract mechanism is composition. That is when you pass
a downward closure to an operation, that could say: I raise what the
argument does. Note that this will require proper procedural types to have
interfaces to carry the contract with. E.g. you would be able to limit the
closure operation to what it is allowed to raise.

>> Secondly, you would rather prove conditionals, like: Storage_Error is not
>> propagated when given amount of memory is available in the specified pools.
>> This is good enough for most cases, which are not about any exact bound,
>> but about existence of such bound, i.e. about memory leak detection.
> 
> You are so violately against dynamically checked conditions ... and then 
> you propose some heuristic that you just claim to be "good enough for most 
> cases"?

Why does this surprise you? No contract can describe all semantics. It only
vaguely describes it. You may have all sorts of possible contracts with the
same implementation and conversely.

It is free choice how much of the semantics a contract to mandate: from few
in a trow away program to much for a mission critical one.

>> Thirdly, you would be able to provide axioms. E.g. for some complex
>> recursive operation, you could just specify the upper memory consumption
>> bound known to you from other sources, and let the prover to go with that
>> (the oracle).
>> 
>> I think conservative Storage_Error proof is pretty doable. If you move the
>> upper bound a pair Kbytes upward it would eliminate most of problems.
> 
> Good luck with any recursive program.
> 
> And (I am sure you know this) any approach to really prove upper bounds 
> on the storage requirements would imply to solve the Halting Problem.

No problem. If you cannot prove it, that is compile error. It is a
conservative estimation, estimations have no halting problem issue, Boolean
values are bounded.

The real problem lies elsewhere. Prover to tell program legality is thin
ice. Depending on the technique used the same program could be legal (good
prover) or illegal (poor prover). I don't know how to address this, though
nobody cares anyway...

>> We certainly could learn from Java mistakes rather than repeating them
>> (e.g. interfaces).
> 
> Which is probably why Ada so far has no contracted exceptions. Not that 
> they cannot be done -- but nobody knows how to write such contracts that 
> they really become useful.

Huh, they didn't much hesitate to borrow flawed Java interfaces, although
the language already had abstract types.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 26.06.12 15:07, Dmitry A. Kazakov wrote:

> They are contracts when checked statically and implementations when checked
> dynamically. 

What do pre/post implement, if so, in your view?


> Contract violation => terminate. Exceptional state => recover.

How does a client do make the program recover if an exception
stands for "unforeseen"?

Or is an exception just a special value of a type, a value
with an "exception" label that is nothing special, but allows
an elaborate goto?

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Tue, 26 Jun 2012 15:49:24 +0200, Georg Bauhaus wrote:

> On 26.06.12 15:07, Dmitry A. Kazakov wrote:
> 
>> They are contracts when checked statically and implementations when checked
>> dynamically. 
> 
> What do pre/post implement, if so, in your view?

   if Pre(...) then
      <body>
      if Post(...) then
         null;
      else
         raise Constraint_Error;
      end if;
   else
      raise Constraint_Error;
   end if;

>> Contract violation => terminate. Exceptional state => recover.
> 
> How does a client do make the program recover if an exception
> stands for "unforeseen"?

How does a client recover if X contains 3 rather than 1?

Answer: it recovers by continuing its program further.

> Or is an exception just a special value of a type, a value
> with an "exception" label that is nothing special, but allows
> an elaborate goto?

Yes, exception an "ideal" value. It is used to fix contracts, when
otherwise no outcome existed. E.g. Constraint_Error is the value of x/0.
With Constraint_Error "+", "-", "*", "/" become defined for all possible
values of the arguments. Compare to IEEE NaN, +Inf, -Inf.

With exceptions you can continue execution when you otherwise could not,
because exceptions add new computational states for which no value
otherwise existed. Continuation goes to these states, which are called
exceptional.

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

Re: about the new Ada 2012 pre/post conditions

[stefan-lucks]

On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote:

> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote:

> > Don't do that! Emit your messages to to the log file and then terminate!
> 
> Contract violation => terminate. Exceptional state => recover.

Yes, exactly!

> > But then, what is more important:
> > 
> >   - Provide tools that support good software engineering practice?
> > 
> > or
> >   
> >   - Prohibit any tools that can be misused?
> > 
> > Dynamically checked contracts are such a tool. 
> 
> A wrench sold as shoe polish.

This is my point! A wrench is good when used as a wrench, also quite good 
as a tool for cryptanalysis <http://xkcd.com/538/>, but bad when misused 
as a shoe polish. 

> > And (I am sure you know this) any approach to really prove upper bounds 
> > on the storage requirements would imply to solve the Halting Problem.
> 
> No problem. If you cannot prove it, that is compile error. It is a
> conservative estimation, estimations have no halting problem issue, Boolean
> values are bounded.
> 
> The real problem lies elsewhere. Prover to tell program legality is thin
> ice. Depending on the technique used the same program could be legal (good
> prover) or illegal (poor prover). I don't know how to address this, though
> nobody cares anyway...

It is even worse! An Ada program is either legal or not. It would be a 
fatal mistake to make legality depend on the theorem prover one is using. 

That is precisely the reason for checked contracts: Within the language, 
we cannot prove them. With additional tools, we may be able to prove at 
least some of them. The tools will improve over time -- hopefully faster 
than new Ada standards arrive. In the mean time, we can do our best to 
figure out contract violations by testing. That means, dynamic checks in 
the test cases.

> >> We certainly could learn from Java mistakes rather than repeating them
> >> (e.g. interfaces).
> > 
> > Which is probably why Ada so far has no contracted exceptions. Not that 
> > they cannot be done -- but nobody knows how to write such contracts that 
> > they really become useful.
> 
> Huh, they didn't much hesitate to borrow flawed Java interfaces, although
> the language already had abstract types.

Yes, indeed. With respect to borrowing ideas from Java, the ARG has 
learned! 



-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Tue, 26 Jun 2012 16:54:45 +0200, stefan-lucks@see-the.signature wrote:

> On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote:
> 
>> The real problem lies elsewhere. Prover to tell program legality is thin
>> ice. Depending on the technique used the same program could be legal (good
>> prover) or illegal (poor prover). I don't know how to address this, though
>> nobody cares anyway...
> 
> It is even worse! An Ada program is either legal or not.

It is an old problem. Not every legal program is compilable:

   X : constant := 2**(2**<compiler-dependent>);

> It would be a 
> fatal mistake to make legality depend on the theorem prover one is using. 

You cannot avoid this. The problem is to find right balance by moving most
variations out of the sensitive area.

> That is precisely the reason for checked contracts: Within the language, 
> we cannot prove them. With additional tools, we may be able to prove at 
> least some of them. The tools will improve over time -- hopefully faster 
> than new Ada standards arrive. In the mean time, we can do our best to 
> figure out contract violations by testing. That means, dynamic checks in 
> the test cases.

I don't believe in tools. A full integration of the prover would open a
completely new level of engineering, when amount of static checks could be
adjusted by the programmer incrementally as the project matures by adding
or removing goals to prove.

>>>> We certainly could learn from Java mistakes rather than repeating them
>>>> (e.g. interfaces).
>>> 
>>> Which is probably why Ada so far has no contracted exceptions. Not that 
>>> they cannot be done -- but nobody knows how to write such contracts that 
>>> they really become useful.
>> 
>> Huh, they didn't much hesitate to borrow flawed Java interfaces, although
>> the language already had abstract types.
> 
> Yes, indeed. With respect to borrowing ideas from Java, the ARG has 
> learned!

Nope, they just switched to Eiffel.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 26.06.12 16:45, Dmitry A. Kazakov wrote:
> On Tue, 26 Jun 2012 15:49:24 +0200, Georg Bauhaus wrote:
> 
>> On 26.06.12 15:07, Dmitry A. Kazakov wrote:
>>
>>> They are contracts when checked statically and implementations when checked
>>> dynamically. 
>>
>> What do pre/post implement, if so, in your view?
> 
>    if Pre(...) then
>       <body>
>       if Post(...) then
>          null;
>       else
>          raise Constraint_Error;
>       end if;
>    else
>       raise Constraint_Error;
>    end if;

There is a different understanding of "implement". Pre/Post
do not implement anything essential. <body> is supposed to
implement something that essentially agrees with Pre/Post.

Some confusion here, I think.



>>> Contract violation => terminate. Exceptional state => recover.
>>
>> How does a client do make the program recover if an exception
>> stands for "unforeseen"?
> 
> How does a client recover if X contains 3 rather than 1?
> 
> Answer: it recovers by continuing its program further.

In a truly exceptional situation, as opposed to when there is
a catch-all "special value", there is no contract that could have
been violated, because the contract does not in any way cover the
situation There is no known good value contained in X, for example,
because there is no (practically) meaningful state.
For this truly exceptional situation, which is necessarily
unforeseen (otherwise it could have been covered by the contract),
I'd include

 Exception(foreseeable) => recover.
 Exception(unforeseen) => STOP.

Unforeseen is a modest word for "the exception handling mechanism
might be broken in this situation". However, Exception(foreseeable)
would include violations of Ada-Pre/Ada-Post, unless checking these
results in Exception(unforeseeable).

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Tue, 26 Jun 2012 18:48:05 +0200, Georg Bauhaus wrote:

> On 26.06.12 16:45, Dmitry A. Kazakov wrote:
>> On Tue, 26 Jun 2012 15:49:24 +0200, Georg Bauhaus wrote:
>> 
>>> On 26.06.12 15:07, Dmitry A. Kazakov wrote:
>>>
>>>> They are contracts when checked statically and implementations when checked
>>>> dynamically. 
>>>
>>> What do pre/post implement, if so, in your view?
>> 
>>    if Pre(...) then
>>       <body>
>>       if Post(...) then
>>          null;
>>       else
>>          raise Constraint_Error;
>>       end if;
>>    else
>>       raise Constraint_Error;
>>    end if;
> 
> There is a different understanding of "implement". Pre/Post
> do not implement anything essential.

They implement raising exceptions.

> <body> is supposed to
> implement something that essentially agrees with Pre/Post.

Sure. Anything that follows "then" in any if-statement implements something
in agreement with the condition tested by the statement. That is the nature
of if-statements.

>>>> Contract violation => terminate. Exceptional state => recover.
>>>
>>> How does a client do make the program recover if an exception
>>> stands for "unforeseen"?
>> 
>> How does a client recover if X contains 3 rather than 1?
>> 
>> Answer: it recovers by continuing its program further.
> 
> In a truly exceptional situation, as opposed to when there is
> a catch-all "special value", there is no contract that could have
> been violated, because the contract does not in any way cover the
> situation There is no known good value contained in X, for example,
> because there is no (practically) meaningful state.

If program continues, it does to some state.

> For this truly exceptional situation, which is necessarily
> unforeseen (otherwise it could have been covered by the contract),

An unforeseen situation cannot be tested for. You cannot evaluate a
predicate P you don't know. Even a test for "others" is foreseen. Others is
merely:

   Others = not (P1 or P2 or ... or Pn)

"Go there, do not know where. Bring that, do not know what"

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 26.06.12 21:43, Dmitry A. Kazakov wrote:

>> <body>  is supposed to
>> implement something that essentially agrees with Pre/Post.
>
> Sure. Anything that follows "then" in any if-statement implements something
> in agreement with the condition tested by the statement. That is the nature
> of if-statements.

That's not what agreement of <body> with Pre/Post should mean, actually.
In a DbC-correct program, the following two bodies shall have essentially
the same effect:


A: begin
   if Pre (...) then
     Stmts;
   else
     raise Assertion_Failure;
   end;
   ...

B: begin
   Stmts;
   ...

When <body> is supposed to implement something that essentially
agrees with Pre/Post, this sameness is it.  Regardless of checks
being on or off, A and B should have the same effects, essentially.

Immediate consequences:

1)  Pre is not for testing validity of input to Stmts
2)  A violation of Pre (i.e. = False) indicates a bug

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Wed, 27 Jun 2012 10:23:47 +0200, Georg Bauhaus wrote:

> On 26.06.12 21:43, Dmitry A. Kazakov wrote:
> 
>>> <body>  is supposed to
>>> implement something that essentially agrees with Pre/Post.
>>
>> Sure. Anything that follows "then" in any if-statement implements something
>> in agreement with the condition tested by the statement. That is the nature
>> of if-statements.
> 
> That's not what agreement of <body> with Pre/Post should mean,

If that is not, change the code. Bugs not to be tolerated.

> actually.
> In a DbC-correct program, the following two bodies shall have essentially
> the same effect:
> 
> A: begin
>    if Pre (...) then
>      Stmts;
>    else
>      raise Assertion_Failure;
>    end;
>    ...
> 
> B: begin
>    Stmts;
>    ...

They evidently do not have same effect. Prove that they do!

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 27.06.12 10:52, Dmitry A. Kazakov wrote:
> On Wed, 27 Jun 2012 10:23:47 +0200, Georg Bauhaus wrote:
>
>> On 26.06.12 21:43, Dmitry A. Kazakov wrote:
>>
>>>> <body>   is supposed to
>>>> implement something that essentially agrees with Pre/Post.
>>>
>>> Sure. Anything that follows "then" in any if-statement implements something
>>> in agreement with the condition tested by the statement. That is the nature
>>> of if-statements.
>>
>> That's not what agreement of<body>  with Pre/Post should mean,
>
> If that is not, change the code. Bugs not to be tolerated.

What bug? I am defining what it means for a statement
to, in essential effects, agree with what an explicitly
stated Pre says, the latter being part of an ante factum
contract.  Consider

A:
   if Pre (...) then
      A (X) := 1;
   else
      raise Assertion_Failure;
   end if;

B:
   A (X) := 1;

A and B can be shown to both be implementations of the behavior
that some contract stipulates.

Just like these implementations of a Procedure Add_2 (X : in out Integer)
can be essentially the same

   X := X + 1;                   null;
   X := X + 1;                   X := X + 2;

A compiler might produce code for these that, for example, is not efficient
enough. If there is no efficiency constraint stated as part of the contract,
the difference is unessential, and the two implementations are essentially
the same, judging by the contract.


> They evidently do not have same effect. Prove that they do!

A and B have *essentially* the same effect once the program
is correct. "Essential effects" is an important consideration
when designing a program. With or without DbC, one choice can be
just as good as another if they yield essentially the same
effect. Unessential things do not count here.  The bug hunting
features of DbC do, as does the value it adds to documentation.

We would not be using compilers or high level languages at all
if there wasn't that notion of "essentially the same".

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Wed, 27 Jun 2012 12:30:41 +0200, Georg Bauhaus wrote:

> On 27.06.12 10:52, Dmitry A. Kazakov wrote:
>> On Wed, 27 Jun 2012 10:23:47 +0200, Georg Bauhaus wrote:
>>
>>> On 26.06.12 21:43, Dmitry A. Kazakov wrote:
>>>
>>>>> <body>   is supposed to
>>>>> implement something that essentially agrees with Pre/Post.
>>>>
>>>> Sure. Anything that follows "then" in any if-statement implements something
>>>> in agreement with the condition tested by the statement. That is the nature
>>>> of if-statements.
>>>
>>> That's not what agreement of<body>  with Pre/Post should mean,
>>
>> If that is not, change the code. Bugs not to be tolerated.
> 
> What bug?

That the code is in disagreement with your objective.

> A:
>    if Pre (...) then
>       A (X) := 1;
>    else
>       raise Assertion_Failure;
>    end if;
> 
> B:
>    A (X) := 1;
> 
> A and B can be shown to both be implementations of the behavior
> that some contract stipulates.

This is wrong on multiple accounts:

1. It cannot be shown: if Pre (HALT (p)) then ... else ... end if;
2. For any program there exist an infinite set of contracts satisfied by;
3. It is irrelevant to whether both pieces are equivalent. If they are,
one can be replaced by another. DO IT, where is the check? If they cannot
be swapped, they are not equivalent.

(Your previous position was more consistent. The point can only be made by
getting rid of logic first.)

>> They evidently do not have same effect. Prove that they do!
> 
> A and B have *essentially* the same effect once the program
> is correct.

I don't know what "essentially same effect" is, but whatever formal
definition of essential you took you would have to prove that two programs
are equivalent according to the definition. That will require proving that
the exception is not propagated or else handled to an "essentially" same
result. Good luck with that.

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

Re: about the new Ada 2012 pre/post conditions

[Nasser M. Abbasi]

On 6/27/2012 7:19 AM, Dmitry A. Kazakov wrote:

>
>> A:
>>     if Pre (...) then
>>        A (X) := 1;
>>     else
>>        raise Assertion_Failure;
>>     end if;
>>
>> B:
>>     A (X) := 1;
>>
>> A and B can be shown to both be implementations of the behavior
>> that some contract stipulates.

>> A and B have *essentially* the same effect once the program
>> is correct.
>

> I don't know what "essentially same effect" is, but whatever formal
> definition of essential you took you would have to prove that two programs
> are equivalent according to the definition. That will require proving that
> the exception is not propagated or else handled to an "essentially" same
> result. Good luck with that.
>

Hello;

I did not check, but I assumed all along that the evaluation
of pre() can have no side effects?

i.e. in the process of executing

        with pre ==> boolean valued expression

Then X could not be _modified_ during this check?

Because if X is modified, as a side effect of the check, from
say 3 to 5 then A(X):=1 will act differently  if pre() was NOT
present.

Hence both code examples shown above will not be equivalent.

Therefore, I assume this can not happen, and it is guaranteed by
the language and compiler that pre() and post() do not have
side-effects?

Else this becomes like Heisenberg uncertainty principle.

thanks,
--Nasser

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 27.06.12 14:19, Dmitry A. Kazakov wrote:

>> A and B can be shown to both be implementations of the behavior
>> that some contract stipulates.
> 
> This is wrong on multiple accounts:
> 
> 1. It cannot be shown: if Pre (HALT (p)) then ... else ... end if;

For run time parameters P1 and P2, and for static or dynamic K:

if P1 + P2 < K then ... else ... end if;

The client programmer sees Pre (P1 + P2 < K) in a spec. She or he will
make sure that all values passed as parameters will satisfy P1 + P2 < K,
QED.

If one programmer can write Pre (HALT (p)) then no programmer should
be able to read or write Pre (P1 + P2 < K)?  This seems overly
restrictive because it prevents *working* towards a man made proof.

> 2. For any program there exist an infinite set of contracts satisfied by;

For any Ada 2012 program there exists just one relevant contract,
which is the contract explicitly stated using Ada with Pre/Post/Inv.
Any program satisfying this contract is fine.

> 3. It is irrelevant to whether both pieces are equivalent.

Equivalence of programs in terms of a given contract can be the goal.
I have given an example of a stack that shows essentially the
same behavior with checks on or off. That is,

 if Pre (...) then Stmnts; else raise ...

vs

 Stmnts;

The difference was in the quality of the error reports.
The "essential sameness" was that the same stack operations
would result in the same stacks.
From a business point of view, the programs fulfill the
necessary conditions of equivalence.


> I don't know what "essentially same effect" is, but whatever formal
> definition of essential you took you would have to prove that two programs
> are equivalent according to the definition. That will require proving that
> the exception is not propagated or else handled to an "essentially" same
> result. Good luck with that.

Wow, finally. ;-) With the addition of having the exception
stop the program according to Assertion_Policy, this is DbC,
a human activity that includes a proof obligation.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 27.06.12 15:41, Nasser M. Abbasi wrote:
> I did not check, but I assumed all along that the evaluation
> of pre() can have no side effects?

Perhaps evaluating Pre's expression has exactly the
side effects that the programmer intends it to have.

It is not even necessary to infiltrate the expression
with side effects to make it harmful. They can well
be pure, see below.

If you want to be a wicked programmer using a reliable
language for doing evil things reliably, use Ada:
write a function K, presumably constant and omit a post
condition that affirms its constant result. Or, specify the
postcondition and make it appear to be constant when
it isn't,  A suitably redefined "=" can modify its arguments:

   with Post => K'Result = 123.

In any case, if what K returns is a random number,
refer to this "constant" function K in

   procedure P (X : Natural)
      with Pre => (X < K);


This issue with Pre's programmer isn't different from side effects
he or she puts in pragma Assert, or, more generally, anywhere
a non-static expression is allowed to do what the programmers
want it to do.

Indeed, using more pure, "functional" approach,
define ">" to return true when its left argument = 0.
Then side effects are not needed for wreaking havoc:

   function ">" (left, right: Natural) return Boolean is
   begin
      return left = 0;
   end ">";

   if Y > 0 then
      return F (X / Y);
   end if;

Re: about the new Ada 2012 pre/post conditions

[Shark8]

> > What do pre/post implement, if so, in your view?
> 
>    if Pre(...) then
>       <body>
>       if Post(...) then
>          null;
>       else
>          raise Constraint_Error;
>       end if;
>    else
>       raise Constraint_Error;
>    end if;

Ok, but this is just what preconditions [and post] are supposed to do.

After all, we had a way to specify some preconditions before (in Ada 2005):
Type Some_Type is ...;
Type Access_Some is Access Some_Type;
Subtype NN_Access_Some is Not Null Access_Some;

Procedure Default_Handler( Object : NN_Access_Some );

defines a a function [spec] in which the body may assume that Object is not null, as if it is it will raise Constraint_Error, thereby allowing us to get rid of the checking logic within the function.

How does pulling that out into the Pre clause in Ada 2012 change things? Also, is not the general concept now generalizable? (IE so that these assumptions may be safely made.)

I'm really confused on why you seem to think the Pre- and Post-conditions are bad things. That you can compile something that *could* violate them is irrelevant, you could do the same with the given default_handler procedure, especially if you were pulling it from user-input. It has a well defined behavior for the error of trying to pass null in, and moreover you can catch-and-correct it if it is correctable.

Post seems a bit less useful than Pre, but maybe that's because I'm being unimaginative today.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 29 Jun 2012 14:03:27 -0700 (PDT), Shark8 wrote:

>>> What do pre/post implement, if so, in your view?
>> 
>>    if Pre(...) then
>>       <body>
>>       if Post(...) then
>>          null;
>>       else
>>          raise Constraint_Error;
>>       end if;
>>    else
>>       raise Constraint_Error;
>>    end if;
> 
> Ok, but this is just what preconditions [and post] are supposed to do.

[That is POV #1]

No they are not. True pre-/post-conditions are not supposed to implement
anything.

Formally speaking, pre-/post-conditions are statements of another language
L. The language Ada is what you use to program some P. P operates  bits and
bytes. The language L is used to operate P itself. In L you can say Correct
(P) or Incorrect (P).

> After all, we had a way to specify some preconditions before (in Ada 2005):
> Type Some_Type is ...;
> Type Access_Some is Access Some_Type;
> Subtype NN_Access_Some is Not Null Access_Some;

It is important to understand that constraint is not a precondition.

> How does pulling that out into the Pre clause in Ada 2012 change things?

Ignoring the fact that the name is misguiding, it is bad because ad-hoc. It
hugely extends the number of places where anonymous subtypes may appear.
Effectively a constraint on the argument defines a subtype for the purpose
of this only subprogram and this only argument.

I am not against extending algebra of subtypes, but it should be done with
great care.

> I'm really confused on why you seem to think the Pre- and Post-conditions
> are bad things.

That is because you didn't follow the discussion. Pre- and post-conditions
are great things, but only when done correctly.

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

Re: about the new Ada 2012 pre/post conditions

[Niklas Holsti]

On 12-06-30 11:26 , Dmitry A. Kazakov wrote:
> On Fri, 29 Jun 2012 14:03:27 -0700 (PDT), Shark8 wrote:
>
>>>> What do pre/post implement, if so, in your view?
>>>
>>>     if Pre(...) then
>>>        <body>
>>>        if Post(...) then
>>>           null;
>>>        else
>>>           raise Constraint_Error;
>>>        end if;
>>>     else
>>>        raise Constraint_Error;
>>>     end if;
>>
>> Ok, but this is just what preconditions [and post] are supposed to do.
>
> [That is POV #1]
>
> No they are not. True pre-/post-conditions are not supposed to implement
> anything.
>
> Formally speaking, pre-/post-conditions are statements of another language
> L. The language Ada is what you use to program some P. P operates  bits and
> bytes. The language L is used to operate P itself. In L you can say Correct
> (P) or Incorrect (P).

Perhaps the Ada 2012 "Pre" and "Post" constructs should be called 
"precheck" and "postcheck" instead of "precondition" and 
"postcondition". Then it would be clearer that they are not the same as 
the logical, side-effect-free pre/postconditions used in program proofs.

An Ada compiler or prover can include (as a conjunct) the "precheck" 
condition in the precondition of a call to the subprogram, and include 
the "postcheck" condition in the postcondition of the call (with 
alternative paths to exception handling). But the pre/post-checks are 
not the *whole* pre/post-conditions in the compiler's analysis or proof.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

(Note: I haven't yet read anyone else's response to this thread; but I 
thought I owed Dmitry a response. If this ground was previously covered, 
please feel free to ignore my response.)

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net...
> On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net...
>>> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote:
>>>
>>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net...
>>>> ...
>>>>> 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.
>>>>
>>>> You're right, but I don't see any inconsistency. They are clearly #1, 
>>>> and
>>>> that includes all of the existing Ada checks as well.
>>>
>>> If you take a stance on #1, then checking stack full is no more 
>>> evaluation
>>> of the precondition, which does not depend on the stack state anymore, 
>>> as
>>> it of course should be. So the "true" precondition is just: True.
>>
>> Huh? This makes no sense whatsoever.
>>
>> We can't require static detection of precondition failures any more than 
>> we
>> can demand static detection of range violations.
>
> You seem to imply that value in the range is a precondition of the
> operation constrained to that range. This is wrong.

It can't be "wrong", because the programmer of an abstraction decides what 
the preconditions and postconditions are.

>  If S is a subtype of T then the precondition is
>
>   X in T
>
> The postcondition is
>
>   (X in S and <something>) or (X not in S and Constraint_Error propagated)
>
>> And Ada *always* has had dynamic preconditions:
>>
>>     procedure New_Line (Spacing : in Positive_Count := 1);
>
> The precondition here is Spacing in Positive_Count'Base because the
> behavior of New_Line is *defined* when Spacing is not in
> Positive_Count'Range.
>
>   New_Line(0)
>
> is a *legal* Ada program.

Legality has nothing to do with preconditions or postconditions. 
Preconditions and postconditions are two sides of the same coin. They're 
checks made on the way into and the way out of a subprogram. There is 
absolutely no justification for saying that these are different in some way. 
You are saying that only a postcondition can have dynamic components, which 
is nonsense.

You seem to want to associate the actions of the precondition with the 
subprogram itself, but that is also wrong. Preconditions are checked 
*before* a subprogram is called, so those actions occur *before* anything in 
the subprogram (and thus anything in the postcondition to the subprogram).

You're trying to fit all exceptions into a single box, which is silly. Some 
exceptions are clearly part of the preconditions of the subprogram -- the 
only reason that they are exceptions is because it is currently beyond the 
state of the art to check these statically. Any occurrence of these 
exceptions in a program represents a bug; they should never happen in a 
correct program. For instance, the mode check for a file.

OTOH, some exceptions are reporting issues that only are detectable *after* 
the subprogram has been called (for example, the Use_Error caused when a 
disk is full). Those should be in the exception contract (not the 
postcondition; that's only for "normal" return; the exception contract might 
have a separate postcondition for each exceptional return).

Deciding between these is something that only the designer of a subprogram 
can do. No mathematical theory can ever do that.

...
>> Nothing you say on this topic makes any sense, at least from an Ada
>> perspective. Here you are saying that Ada's entire design and reason for
>> existing is "not defendable"
>
> Why entire? Dynamic correctness checks are not defendable, as demonstrated
> on numerous examples.

The only kind of correctness checks that *can* exist in general are dynamic. 
Ada's entire reason to exist is to include checks like range checks and 
overflow checks to programs. Without them you get the buffer overflows and 
other errors that plague C code.

Compile-time detection of bugs is only possible in very limited and not very 
useful cases. Limiting a programming language to those cases only makes it 
unusable (exhibit #1 - SPARK).

I suppose you have a totally different definition of "correctness checks" 
than I do; as usual, we can't have a useful discussion because you have your 
own set of terminology.

...
>> How your ideal language might work is irrelevevant in this forum.
>
> It is not mine language. It is a methodology of defining and proving
> program correctness as introduced by Dijkstra. It applies to all languages
> without exemption.

We're not interested in "proving program correctness". That's (still) beyond 
the state of the art for any realistic programming language. We *are* 
interested in dynamic features that can provide information to future static 
analysis tools. But realistic analysis tools will never (and should never) 
try for "complete" analysis.

>> Please talk about Ada, not impossible theory.
>
> The only impossible theory here is about meaning of dynamically checked
> preconditions, e.g. #1 or #2? That is indeed impossible, because
> inconsistent. Otherwise Dijkstra's approach works pretty well with any
> language, e.g. SPARK does for Ada.

SPARK is next to useless for real programs - at best it can be used only to 
prove small parts of a program, and it takes a lot of effort to get there. 
It's the sort of thing that turns programmers off (it *certainly* has done 
that to me!) and essentially pushes them to stick with the unsafe languages 
that they are using. Instead of getting the benefits of building in Ada now, 
and getting more and more static checks as compilers improve.

This idea of "perfect" proving has essentially prevented these techniques 
from moving into the mainstream, and it is sad that this is the case.

Anyway, if you are going to push "program proving", then we literally have 
nothing to talk about. So this conversation is done.

                                          Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:bdpvyb9h7rvt.zbq0kbiq72wj.dlg@40tude.net...
...
>> Sure! So what?
>
> How are going to marry exceptions propagating from contracts with 
> contracts
> on exceptions? Some exceptions are more exceptional than others? Aren't we
> fed up with Program_Error?

That's trivial. Exceptions from contracts occur at the call site; they're 
not part of the subprogram. Of course they *are* part of the contract of the 
subprogram that made the call. It works just like propagation.

You have far too narrow of a view of what a contract is. Open up your mind, 
and it will all make far more sense.

                                   Randy. 

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote:
...
> They are contracts when checked statically and implementations when 
> checked
> dynamically.

No, they're always contracts. They certainly aren't "implementation", 
because they do *not* belong to the subprogram; they're checked *before* the 
subprogram is called. (The check, if any, belongs to caller, not the 
callee.)

Besides, I don't understand why it is such a disaster to have precondition 
contracts be dynamically evaluated in some cases, while it is OK to have a 
postcondition be dynamically evaluated in some cases -- it too is a contract 
(one that is evaluated *after* the subprogram finishes).

In any case, you want to prevent the any mechanism for specifying these 
things in code rather than in comments are currently. It should never be 
necessary for anyone to look into the body ("implementation") of a routine 
to see the contract (static or dynamic); tools that have to see within 
bodies (that is, only operate on all of the source) are close to useless 
(since they can only be used at the end of the development cycle when fixing 
bugs is at its most expensive).

...
>> So you just add "can raise Storage_Error" to any contract? (Maybe
>> implicitly.)
>
> Contracts will be inheritable. I don't know how it goes with aspects, 
> never
> understood what they are good for, but true contracts are inherited while
> possibly weakening pre- and strengthening post-conditions (LSP).

Yes, of course. Class-wide preconditions are inherited (potentially with 
weakening, although that's almost never useful), as are class-wide 
postconditions (with strengthening). (Don't use specific preconditions and 
postconditions if you care about inheritance.)

> Another necessary contract mechanism is composition. That is when you pass
> a downward closure to an operation, that could say: I raise what the
> argument does. Note that this will require proper procedural types to have
> interfaces to carry the contract with. E.g. you would be able to limit the
> closure operation to what it is allowed to raise.

I agree with the need for composition; we had that in the never-finished 
"global in/out" contracts. But that doesn't require "procedural types" 
per-se; it can be done quite easily with the existing facilities. (Whether 
the result really would be any good, I can't say, but I'm pretty sure that 
the existence of "procedural types" would make no difference in how useful 
is is.)

...
> The real problem lies elsewhere. Prover to tell program legality is thin
> ice. Depending on the technique used the same program could be legal (good
> prover) or illegal (poor prover). I don't know how to address this, though
> nobody cares anyway...

I think some of us care, the problem is assuming that the prover can prove 
everything important (that will never, ever happen). For me, the biggest 
impediment is coming up with rules that would allow proving what they can 
without (a) requiring too much of all compilers and (b) bounding what an 
implementation can do. There's clearly a portability problem here -- it's 
quite possible that that problem will prevent ever implementing exception 
contracts in the Ada language (as opposed to specific implementations).

                      Randy.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net...

>> You seem to imply that value in the range is a precondition of the
>> operation constrained to that range. This is wrong.
> 
> It can't be "wrong", because the programmer of an abstraction decides what 
> the preconditions and postconditions are.

No. He cannot decide them to implement the contract. That he actually can,
per allowing dynamic checks, is a language design bug.

>>  If S is a subtype of T then the precondition is
>>
>>   X in T
>>
>> The postcondition is
>>
>>   (X in S and <something>) or (X not in S and Constraint_Error propagated)
>>
>>> And Ada *always* has had dynamic preconditions:
>>>
>>>     procedure New_Line (Spacing : in Positive_Count := 1);
>>
>> The precondition here is Spacing in Positive_Count'Base because the
>> behavior of New_Line is *defined* when Spacing is not in
>> Positive_Count'Range.
>>
>>   New_Line(0)
>>
>> is a *legal* Ada program.
> 
> Legality has nothing to do with preconditions or postconditions.

=> It is OK to violate a "contract" defined by these. Here you are.

> The only kind of correctness checks that *can* exist in general are dynamic. 
> Ada's entire reason to exist is to include checks like range checks and 
> overflow checks to programs. Without them you get the buffer overflows and 
> other errors that plague C code.

Yes, but irrelevant. These checks are not contract checks, because,
otherwise you are in contradiction. No words can change that.

But also there are important consequences for software engineering. Since
these checks have nothing to do with contracts, they must be considered as
a part of the program semantics and all possible outcomes must be
*handled*. The problem of buffer overflow is exactly in pretending that it
cannot overflow. So the program is broken when it does.
 
> I suppose you have a totally different definition of "correctness checks" 
> than I do; as usual, we can't have a useful discussion because you have your 
> own set of terminology.

Terminology is secondary to the semantics. The problem is with the meaning.

> SPARK is next to useless for real programs - at best it can be used only to 
> prove small parts of a program, and it takes a lot of effort to get there.

You don't need to prove every possible aspect of the program. The language
should allow the programmer to choose. Ada 83 had provable contracts stated
in terms of types. Nothing prevents us from having more detailed contracts
as well as other program correctness stuff. I simply don't understand where
is a problem with that.

> Instead of getting the benefits of building in Ada now, 
> and getting more and more static checks as compilers improve.

I don't see tracking down exceptions as a benefit. Neither would it be a
for the maintainer to discover that the program suddenly became illegal
because static checks has been "improved."

I prefer to rely on things known to work now. These I use and hope that
they will continue to work in the future.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote:
> ...
>> They are contracts when checked statically and implementations when 
>> checked dynamically.
> 
> No, they're always contracts. They certainly aren't "implementation", 
> because they do *not* belong to the subprogram; they're checked *before* the 
> subprogram is called.

Checked by whom? How does this make any difference to the caller or to the
program as a whole? Is there a way to determine whether an exception was
raised in the body or "before" the body? Maybe there is some special
before-the-body-exceptions, propagated in some special manner? It just does
not make sense. The contract should refer to all effect of calling the
program.

> Besides, I don't understand why it is such a disaster to have precondition 
> contracts be dynamically evaluated in some cases, while it is OK to have a 
> postcondition be dynamically evaluated in some cases -- it too is a contract 
> (one that is evaluated *after* the subprogram finishes).

It is *not* OK to evaluate precondition of a program by the program itself.
It is similar to how halting becomes a problem:

procedure P is
begin
   while not HALT (P) loop
      null;
   end loop;
end P;

All this boils down to self-referential stuff.

> (Don't use specific preconditions and 
> postconditions if you care about inheritance.)

Which is a telling advise, taking into about that [true]
pre-/post-conditions is all [true] interface is about. Inheritance at the
interface level is nothing but shuffling pre-/post-conditions.

>> Another necessary contract mechanism is composition. That is when you pass
>> a downward closure to an operation, that could say: I raise what the
>> argument does. Note that this will require proper procedural types to have
>> interfaces to carry the contract with. E.g. you would be able to limit the
>> closure operation to what it is allowed to raise.
> 
> I agree with the need for composition; we had that in the never-finished 
> "global in/out" contracts. But that doesn't require "procedural types" 
> per-se;

Propagation of target contracts trough access to the target looks much more
complicated.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 03.07.12 14:53, Dmitry A. Kazakov wrote:
> It is *not* OK to evaluate precondition of a program by the program itself.
> It is similar to how halting becomes a problem:

Three participants have already noted that starting from two
different assignments of meaning to words such as "contract"
and "program design", chances are that conclusions differ.

> procedure P is
> begin
>    while not HALT (P) loop
>       null;
>    end loop;
> end P;
> 
> All this boils down to self-referential stuff.


Yes. Normal program design can hope to get close to a primitive
recursive programming process.


procedure Design_Program is
  Result : Program;
  V      : Inputs_Iterator;
  Y,
  Expected : Outputs;

  Bug : exception;
begin
  loop
    Result := Design;
    V := Test_Suite;
    for X in V loop
      Expected := Knowledge (X);
      if STEP (Result, X) > THRESHOLD then
         raise Bug with "STEP";
      end if;
      if Y /= Expected then
         raise Bug with "FAIL";
      end if;
    end loop;
  end loop;
end Design_Program;

The programming process can strive for success in showing
that STEP <= THRESHOLD for all inputs. Bugs still leave
some risks. But reducing risk and still taking some risks
is normal engineering, isn't it?

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Tue, 03 Jul 2012 15:48:32 +0200, Georg Bauhaus wrote:

> Yes. Normal program design can hope to get close to a primitive
> recursive programming process.

If you look how iterative solutions of optimization problems work, you will
notice that the goal function is a *function*. Looking from this angle the
program P under design is a point in the space of possible programs. The
goal function g takes P as an argument. P cannot compute g, it is an
argument of. Design process needs g() upfront, which we all know as an
empiric rule: you better know what you are going to write. Even such
notably poor practices as TDD don't go that far as you would go by putting
g into P. TDD keeps g outside P as a set of external test programs.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 03.07.12 16:06, Dmitry A. Kazakov wrote:
> TDD keeps g outside P as a set of external test programs.

Actually, TDD assumes it is keeping g outside P. By the
self-referential nature of things, this is not decidable,
but is a helpful illusion.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 03.07.12 18:12, Georg Bauhaus wrote:
> this is not decidable,

Two rather mundane illustrations of what "not decidable" might
mean, in the end:

1. Given source text, you are supposed to predict what
happens. Choices given are: compilation fails; no output;
output X; output Y. Now suppose compilation must fail. Is it
correct, then, to say that "no output" is what happens, too?

2. In a TV show, the hosts ask candidates questions such
as this: name all countries in the same time zone as
ours, X. One candidate says X. His choice is rejected.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net...
> On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature 
>>> wrote:
>> ...
>>> They are contracts when checked statically and implementations when
>>> checked dynamically.
>>
>> No, they're always contracts. They certainly aren't "implementation",
>> because they do *not* belong to the subprogram; they're checked *before* 
>> the
>> subprogram is called.
>
> Checked by whom?

By the caller, not the called body.

> How does this make any difference to the caller or to the
> program as a whole? Is there a way to determine whether an exception was
> raised in the body or "before" the body?

Sure: you can handle an exception raised in the body in the body itself; you 
cannot handle an exception raised by the call in the body.

> Maybe there is some special
> before-the-body-exceptions, propagated in some special manner? It just 
> does
> not make sense.

It's been that way in Ada since at least Ada 80 -- exceptions raised by the 
call cannot be handled in the body, exceptions raised in the body can be 
handled in the body. Amazing to find out that the model "does not make 
sense" after 30+ years. ;-) It has never been the case that constraint 
failures are part of the effect of the subprogram; they're part of the 
effect of the call (and thus belong to the caller, not the callee).

> The contract should refer to all effect of calling the program.

It does. The call itself is not part of the effect of "calling the 
subprogram".

>> Besides, I don't understand why it is such a disaster to have 
>> precondition
>> contracts be dynamically evaluated in some cases, while it is OK to have 
>> a
>> postcondition be dynamically evaluated in some cases -- it too is a 
>> contract
>> (one that is evaluated *after* the subprogram finishes).
>
> It is *not* OK to evaluate precondition of a program by the program 
> itself.

Well, then the precondition would never be evaluated at all, because there 
is nothing else. In my world, at least, Ada is the only programming 
language -- we even used Ada as the language of the command line of our 
debugger. The notion of using some other language and some other program to 
describe program semantics is a non-starter.

                                        Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
...
>> Legality has nothing to do with preconditions or postconditions.
>
> => It is OK to violate a "contract" defined by these. Here you are.

No, it's not OK; that is the crux of our disagreement. You seem to think 
that the only kind of "contract" is some sort of static thing. But that's 
never, ever been true in Ada.

Exactly. You claim that there cannot be such a thing as a dynamically 
enforced contract. But that's simply bogus - Ada has had those since the 
beginning of time - they were called "constraints". Failing one of these 
checks means that your program is wrong. Ada of course defines what happens 
(raising an exception, etc.), but handling those does not make your program 
less wrong. The only reason that these aren't detected statically is the 
difficulty (and impossibility, in some cases) of detecting them statically.

Yes, of course, there are also exceptions raised for reasons outside of a 
contract (that is, those that don't appear in the profile of a subprogram), 
and handling those might make sense in a correct program.

But handling exceptions raised for contracts does not make the program any 
less wrong; indeed, the only legitimate reasons for handling those is to 
make debugging easier [and, in a few applications, to make the application 
"bullet-proof"].

>> The only kind of correctness checks that *can* exist in general are 
>> dynamic.
>> Ada's entire reason to exist is to include checks like range checks and
>> overflow checks to programs. Without them you get the buffer overflows 
>> and
>> other errors that plague C code.
>
> Yes, but irrelevant. These checks are not contract checks, because,
> otherwise you are in contradiction. No words can change that.

Certainly not if you insist on using an unnecessarily limiting definition of 
"contract".

> But also there are important consequences for software engineering. Since
> these checks have nothing to do with contracts, they must be considered as
> a part of the program semantics and all possible outcomes must be
> *handled*. The problem of buffer overflow is exactly in pretending that it
> cannot overflow. So the program is broken when it does.

That's certainly a fallacy in general. Most Ada programs are best off *not* 
handling exceptions caused by outright bugs, because the Ada runtime will do 
a better job of pinpointing the source of the error than any facility you 
could create yourself. Of course, some programs have to be bullet-proof, but 
that is the tiny minority.

In a sense, of course, it's the Ada runtime that's providing the "handling" 
of those bugs (runtime contract failures). And that means a programmer 
doesn't have to, unless they need bulletproof code that is resistent to 
bugs. A lot of programs are *not* in this category. The Janus/Ada compiler, 
for instance, makes no attempt to handle such bugs -- it's much better to 
abandon the compilation attempt immediately rather than producing a program 
based on guessing what was intended.

>> I suppose you have a totally different definition of "correctness checks"
>> than I do; as usual, we can't have a useful discussion because you have 
>> your
>> own set of terminology.
>
> Terminology is secondary to the semantics. The problem is with the 
> meaning.

Right. I recall in the past that you've been unwilling to grasp the idea of 
bugs being detected at runtime. Just because Ada defines what happens in 
those cases does not suddenly make it OK to introduce bugs into a program.

>> SPARK is next to useless for real programs - at best it can be used only 
>> to
>> prove small parts of a program, and it takes a lot of effort to get 
>> there.
>
> You don't need to prove every possible aspect of the program. The language
> should allow the programmer to choose. Ada 83 had provable contracts 
> stated
> in terms of types. Nothing prevents us from having more detailed contracts
> as well as other program correctness stuff. I simply don't understand 
> where
> is a problem with that.

That's what we're trying to do, and you *obviously* have a problem with 
that. Learning more languages and more tools to do what an Ada compiler 
ought to be able to do is silly.

>> Instead of getting the benefits of building in Ada now,
>> and getting more and more static checks as compilers improve.
>
> I don't see tracking down exceptions as a benefit. Neither would it be a
> for the maintainer to discover that the program suddenly became illegal
> because static checks has been "improved."

That's not a real problem, because any such program is already wrong (its 
depending on the failure of a dynamic contract). Sure, people can write such 
code, but it's just like overlaying objects using address clauses -- it 
might work, but its still wrong and there is no guarentee that a newer 
compiler version will not break such things.

[As an aside, this means you do not want real exception contracts, since 
they cannot usefully be done without having it be implementation-defined 
when an exception is raised by a predefined check. The canonical semantics 
of Ada would require assuming that every line raises Storage_Error, 
Program_Error, and usually Constraint_Error -- that would make it virtually 
impossible to eliminate those exceptions from contracts. OTOH, compilers can 
and do remove most of those canonical checks, and letting the contracts be 
enforced against whatever is actually raised by the generated code would be 
much more useful. But it is impractical to specify the checks that have to 
be removed (and not very helpful - it could only be a very small number), so 
what is raised has to be implementation-defined. Which means that just 
because a contract works on one compiler does not mean that it will work on 
another compiler (including a later version of the same compiler). I agree 
with you that runtime detection of exception contract failure makes no 
sense, so the only choices are implementation-defined or non-existent.]

                               Randy.

Re: about the new Ada 2012 pre/post conditions

[Shark8]

On Saturday, June 30, 2012 3:26:12 AM UTC-5, Dmitry A. Kazakov wrote:
> On Fri, 29 Jun 2012 14:03:27 -0700 (PDT), Shark8 wrote:
>> I'm really confused on why you seem to think the Pre- and Post-conditions
>> are bad things. 
> 
> That is because you didn't follow the discussion. Pre- and post-conditions
> are great things, but only when done correctly.

Ah, now you're equating 'following' with both 'understanding' and 'remembering the nuances' -- I don't agree with that definition, precisely because it excludes the request for clarification so one might understand it.

Also, I don't know where you got the idea that pre- and post-conditions must not implement anything. If that was the case then, strictly speaking JavaDoc's pre and postcondition annotating comments are superior to Ada's pre and post condition because they don't implement anything and are, in fact, just comments having no actual impact on the program text.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote:

> Also, I don't know where you got the idea that pre- and post-conditions
> must not implement anything.

Trivial:

IF pre-/post-condition is contract THEN they are not implementation

[POV #2]

(Historically, pre-/post-conditions were invented by Dijkstra for the
purpose of proving correctness. Later they were used for types to analyze
substitutability issues etc.)

ELSE ... [POV #1]

> If that was the case then, strictly speaking
> JavaDoc's pre and postcondition annotating comments are superior to Ada's
> pre and post condition because they don't implement anything and are, in
> fact, just comments having no actual impact on the program text.

Not if condition proof fault makes the program illegal.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Wed, 4 Jul 2012 20:45:20 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net...
>> On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>>> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>>>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature 
>>>> wrote:
>>> ...
>>>> They are contracts when checked statically and implementations when
>>>> checked dynamically.
>>>
>>> No, they're always contracts. They certainly aren't "implementation",
>>> because they do *not* belong to the subprogram; they're checked *before* 
>>> the subprogram is called.
>>
>> Checked by whom?
> 
> By the caller, not the called body.
>
>> How does this make any difference to the caller or to the
>> program as a whole? Is there a way to determine whether an exception was
>> raised in the body or "before" the body?
> 
> Sure: you can handle an exception raised in the body in the body itself; you 
> cannot handle an exception raised by the call in the body.

That is irrelevant to the question asked. It was about the CALLER. Whatever
happening on the other side is an implementation. You cannot avoid #1 or
#2.

>> Maybe there is some special
>> before-the-body-exceptions, propagated in some special manner? It just 
>> does not make sense.
> 
> It's been that way in Ada since at least Ada 80 -- exceptions raised by the 
> call cannot be handled in the body, exceptions raised in the body can be 
> handled in the body. Amazing to find out that the model "does not make 
> sense" after 30+ years. ;-) It has never been the case that constraint 
> failures are part of the effect of the subprogram; they're part of the 
> effect of the call (and thus belong to the caller, not the callee).

All effects always belong to the caller. Whatever the caller does is to
obtain these effects.

>> The contract should refer to all effect of calling the program.
> 
> It does. The call itself is not part of the effect of "calling the 
> subprogram".

Then the contract does not cover all effects of putting a call statement
into an Ada program.

The same question again: on the language level, what a sequence of
characters denoting call to the subprogram P is supposed to *mean*? The
effect of writing, compiling, running programs containing that refer to P
is what?

Putting it even simpler. What is the effect of:

   sqrt (-1.0)

No effect? Any effect?

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
> ...
>>> Legality has nothing to do with preconditions or postconditions.
>>
>> => It is OK to violate a "contract" defined by these. Here you are.
> 
> No, it's not OK; that is the crux of our disagreement. You seem to think 
> that the only kind of "contract" is some sort of static thing.

Exactly. Because the contract exists *before* any programs implementing it
and after them. The contract exists even when there is no such program.
Therefore it cannot depend on the program state.

Another way to understand this: a contract describes states of a program.
As such it cannot depend on them.

Yet another way: the language of contracts is not the object language:

http://en.wikipedia.org/wiki/Object_language

> But that's never, ever been true in Ada.

I already said that type constraints are not contracts. E.g. an actual
value of the discriminant does not create a new contract. The contract
covers *all* possible values of the discriminant.

> Exactly. You claim that there cannot be such a thing as a dynamically 
> enforced contract.

Absolutely. How could you enforce a contract which has been *already*
violated? If a program reaches an illegal state, it is in that state.
Period.

> But handling exceptions raised for contracts does not make the program any 
> less wrong;

Really? What is the purpose of the exercise? Raising exception, rolling the
stack, finalizing stuff, and so on only to resign that the program is as
wrong as it was before? (Maybe it is even *more* wrong than it was? (:-))

>>> The only kind of correctness checks that *can* exist in general are dynamic.
>>> Ada's entire reason to exist is to include checks like range checks and
>>> overflow checks to programs. Without them you get the buffer overflows 
>>> and other errors that plague C code.
>>
>> Yes, but irrelevant. These checks are not contract checks, because,
>> otherwise you are in contradiction. No words can change that.
> 
> Certainly not if you insist on using an unnecessarily limiting definition of 
> "contract".

Yes, the contract as opposed to the implementation limits the former not to
be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada
2012 "contracts" are implementations [POV #1]. Do you?

>> But also there are important consequences for software engineering. Since
>> these checks have nothing to do with contracts, they must be considered as
>> a part of the program semantics and all possible outcomes must be
>> *handled*. The problem of buffer overflow is exactly in pretending that it
>> cannot overflow. So the program is broken when it does.
> 
> That's certainly a fallacy in general. Most Ada programs are best off *not* 
> handling exceptions caused by outright bugs,

What about the statement: "Most Ada programs are best off not adding
integer numbers caused by outright bugs"?

The actual fallacy is in pretending that a bug can be handled. You can
handle/be in only anticipated states.

The proper statement should have been: "Ada is best to make the programmer
aware of the states he might overlooked."

>>> I suppose you have a totally different definition of "correctness checks"
>>> than I do; as usual, we can't have a useful discussion because you have 
>>> your own set of terminology.
>>
>> Terminology is secondary to the semantics. The problem is with the 
>> meaning.
> 
> Right. I recall in the past that you've been unwilling to grasp the idea of 
> bugs being detected at runtime.

Sure, because that is rubbish, and always was:

http://en.wikipedia.org/wiki/Liar_paradox

> [As an aside, this means you do not want real exception contracts, since 
> they cannot usefully be done without having it be implementation-defined 
> when an exception is raised by a predefined check. The canonical semantics 
> of Ada would require assuming that every line raises Storage_Error, 
> Program_Error, and usually Constraint_Error -- that would make it virtually 
> impossible to eliminate those exceptions from contracts.

I don't see it as a big problem. There is a difference between an
obligation to raise exception and a possibility that an exception could be
raised.

The contract language should deploy the intuitionistic logic. That is
necessary anyway because some things are not provable. In the
intuitionistic logic A or not A is not true (no law of excluded middle).
E.g.

   "raise E"   (I will raise E)

and

   not "not raise E"   (I may raise E. I don't promise not to rase E)

are not equivalent statements.

The vendors could gradually reduce the number of cases where E may be
raised without making clients relying on weaker contracts illegal. The
second cannot be misused to prove that E is raised. It just does not follow
from the second, and conversely.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 05.07.12 10:48, Dmitry A. Kazakov wrote:
> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:
> 
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
>> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
>>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
>> ...
>>>> Legality has nothing to do with preconditions or postconditions.
>>>
>>> => It is OK to violate a "contract" defined by these. Here you are.
>>
>> No, it's not OK; that is the crux of our disagreement. You seem to think 
>> that the only kind of "contract" is some sort of static thing.
> 
> Exactly. Because the contract exists *before* any programs implementing it
> and after them. The contract exists even when there is no such program.

OK

> Therefore it cannot depend on the program state.

The "therefore" does not follow, because "it" makes too far reaching
assumptions, from which, I think, no one suggests your logic does not
follow. "It", for a start, once it materializes in this or that form.

Contract checking built into a program is rather
a design tool than some oracular inference engine.
Correctness need not be assumed at this stage.

If the checks are severely flawed bacause some programmer
inserts viral side effects in checked expressions,
or just wishes to start from the proof of the absence of
666 consecutive digits of e in π on the way,
then so be it.  He or she is violating the goals of
designing with the help of assertions. The goal is *not*
unrolling proven assumptions into source text, but arriving
at proven systems. So that turning off assertion checking
can be considered safe. Safe because checking will not
affect the desired effect of the program in any way that
is covered by the contract-as-agreed as being essential.

So IMHO Pre/Post/Inv are really improvements of pragma Assert.

> Another way to understand this: a contract describes states of a program.

That's not a contract. There are no parties. There is
no obligation to make predicates true on either side.
A program could define states, in the contract's space.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 05.07.12 14:07, Georg Bauhaus wrote:

> The "therefore" does not follow, because "it" makes too far reaching
> assumptions, from which, I think, no one suggests your logic does not
> follow. "It", for a start, once it materializes in this or that form.
                     & is plural &

> A program could define states, in the contract's space.
  s/program/contract/

Sorry. Thunderstorms about to arrive here.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Thu, 05 Jul 2012 14:07:02 +0200, Georg Bauhaus wrote:

> On 05.07.12 10:48, Dmitry A. Kazakov wrote:
>> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:
>> 
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
>>> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
>>>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
>>> ...
>>>>> Legality has nothing to do with preconditions or postconditions.
>>>>
>>>> => It is OK to violate a "contract" defined by these. Here you are.
>>>
>>> No, it's not OK; that is the crux of our disagreement. You seem to think 
>>> that the only kind of "contract" is some sort of static thing.
>> 
>> Exactly. Because the contract exists *before* any programs implementing it
>> and after them. The contract exists even when there is no such program.
> 
> OK

>> Therefore it cannot depend on the program state.
> 
> The "therefore" does not follow,

It does. States of P do not exist before P, which does not exist before its
contract. ["exists before" is a transitive relation]

> because "it" makes too far reaching
> assumptions, from which, I think, no one suggests your logic does not
> follow.

Can you point these assumptions out?

>> Another way to understand this: a contract describes states of a program.
> 
> That's not a contract.

Not any such thing is a contract. But any contract is such thing.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 05.07.12 14:31, Dmitry A. Kazakov wrote:
>> too far reaching
>> > assumptions, from which, I think, no one suggests your logic does not
>> > follow.
> Can you point these assumptions out?
> 

moment, please ...

Re: about the new Ada 2012 pre/post conditions

[Adam Beneschan]

On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:

> Putting it even simpler. What is the effect of:
> 
>    sqrt (-1.0)
> 
> No effect? Any effect?

This looks like an imaginary problem to me, not a real one.

                            -- Adam

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:

> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
> 
>> Putting it even simpler. What is the effect of:
>> 
>>    sqrt (-1.0)
>> 
>> No effect? Any effect?
> 
> This looks like an imaginary problem to me, not a real one.

What problem? It was a simple question illustrating absurdity of the idea.

Since the effect is evidently Constraint_Error, then raising it is a
required part of the implementation.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Thu, 05 Jul 2012 20:16:42 +0200, Georg Bauhaus wrote:

> On 05.07.12 14:31, Dmitry A. Kazakov wrote:
>>> too far reaching
>>> > assumptions, from which, I think, no one suggests your logic does not
>>> > follow.
>> Can you point these assumptions out?
>> 
> 
> moment, please ...

(infinite recursion into self-referential propositions (:-))

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

Re: about the new Ada 2012 pre/post conditions

[Shark8]

On Thursday, July 5, 2012 1:24:57 AM UTC-6, Dmitry A. Kazakov wrote:
> On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote:
> 
> > Also, I don't know where you got the idea that pre- and post-conditions
> > must not implement anything.
> 
> Trivial:
> 
> IF pre-/post-condition is contract THEN they are not implementation
> [POV #2]
> ELSE ... [POV #1]

Now you're just restating what you said. If you mean something like "I take that to be axiomaatic" or "by definition [...]" there'd be something to discuss.

As is though you're just throwing out the assertion that pre- and post-conditions must not have an implementation. {Otherwise they're not *real*, *contracted* pre- post-conditions.} this strikes me as a bit... off, considering things from the other direction: how to implement [for lack of a better word] pre- and post-conditions most of the method you seem to be advocating is impossible (just like any user-input cannot be guaranteed correct w/o either having all user-input as permissible, or otherwise validating it) or difficult on the compile-time/static-analysis level.

> (Historically, pre-/post-conditions were invented by Dijkstra for the
> purpose of proving correctness. Later they were used for types to analyze
> substitutability issues etc.)

And isn't the idea with Ada's constructs to at least aid proving the correctness of a program? Furthermore, wouldn't it be preferable to throw an exception when the condition is violated? That seems to fit perfectly with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no?
 
> > If that was the case then, strictly speaking
> > JavaDoc's pre and postcondition annotating comments are superior to Ada's
> > pre and post condition because they don't implement anything and are, in
> > fact, just comments having no actual impact on the program text.
> 
> Not if condition proof fault makes the program illegal.

It does nothing, insofar as I know, regarding nprogram correctness. http://en.wikipedia.org/wiki/Java_annotation has as an example the "override" annotation which when violated only provides a warning.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 05.07.12 21:57, Dmitry A. Kazakov wrote:
> On Thu, 05 Jul 2012 20:16:42 +0200, Georg Bauhaus wrote:
>
>> On 05.07.12 14:31, Dmitry A. Kazakov wrote:
>>>> too far reaching
>>>>> assumptions, from which, I think, no one suggests your logic does not
>>>>> follow.
>>> Can you point these assumptions out?
>>>
>>
>> moment, please ...
>
> (infinite recursion into self-referential propositions (:-))

Working against what appears to be from an rhetoric arsenal,
even when only accidentally, and collecting all references
correctlyisn't that easy.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 05.07.12 21:55, Dmitry A. Kazakov wrote:
> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>
>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>
>>> Putting it even simpler. What is the effect of:
>>>
>>>     sqrt (-1.0)
>>>
>>> No effect? Any effect?
>>
>> This looks like an imaginary problem to me, not a real one.
>
> What problem? It was a simple question illustrating absurdity of the idea.

Actually, a negative argument passed to sqrt is illustrating proper DbC
well. One famous example is Ariane 4, (4), that's the number four.
Another example is muffins, or meat balls.

sqrt(r), r < 0 would corresponds to ariane-4-f(v), where not v'valid:
since the engineers did well for Ariane 4, not v'valid would not happen,
is always true. So they could make the software module efficient.


> Since the effect is evidently Constraint_Error, then raising it is a
> required part of the implementation.

The proponents of DbC see the sqrt case differently, OOSC2 � 11.6(*):

+---
|   Non-Redundancy principle
|
| Under no circumstances shall the body of a routine ever test
| for the routine's precondition.
+---

where

   function sqrt (x: REAL) return REAL
      with   Pre => x >= 0.0;


That is, in a properly written system the author of the call
of sqrt needs to ensure that x >= 0.0 because of his or her
contractual obligation to do exactly this. The author of
sqrt is right when he or she starts from the precondition
as agreed between the two in contract: x >= 0.0 = True.

For making muffins (or meat balls), when stirring is required,
use a tool. The precondition for using the tool is that
the dough be for muffins (or made of equally light ingredients
for meat balls). Don't use the same tool with sour dough starter
and rye flour. That's part of the contract.

I'll not be surprised to learn the makers of kitchen machines
have added corresponding preconditions in their manuals.

__
(*) � 11.6. Coincidence? ;-) ;-)

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 06.07.12 09:41, Georg Bauhaus wrote:
> Don't use the same tool with sour dough starter
> and rye flour. That's part of the contract.

For those not familiar with making rye bread, lighter tools
will break or bend if moved in this kind of dough.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Thu, 5 Jul 2012 23:23:20 -0700 (PDT), Shark8 wrote:

> On Thursday, July 5, 2012 1:24:57 AM UTC-6, Dmitry A. Kazakov wrote:
>> On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote:
>> 
>>> Also, I don't know where you got the idea that pre- and post-conditions
>>> must not implement anything.
>> 
>> Trivial:
>> 
>> IF pre-/post-condition is contract THEN they are not implementation
>> [POV #2]
>> ELSE ... [POV #1]
> 
> Now you're just restating what you said.

No. The propositions are different:

P1: The contract may implement [some behavior]
P2: Pre-/post-conditions may implement [some behavior]

The statement I made was:

Pre-/post-condition is contract AND not P1 => not P2

Nobody, so far, take an assault on not P1. Would you?

> If you mean something like "I
> take that to be axiomaatic" or "by definition [...]" there'd be something
> to discuss.

Nope. Then, there will nothing to discuss, because a usual trick then, is
to refer to the RM claiming that anything you said is irrelevant to Ada.

Instead I offered a bait: two options to choose #1 and #2. These two are
complete and independent. It cannot be both, it cannot be none.

> pre- and post-conditions most of the method you
> seem to be advocating is impossible

1. SPARK
2. Proving correctness of all program >>> proving correctness of contracts

But the argument is bogus. If something is wrong it is wrong no matter how
implementable it be.

In fact, easily implementable wrong things are much more wrong than just
wrong ones. (:-))

> (just like any user-input cannot be
> guaranteed correct w/o either having all user-input as permissible, or
> otherwise validating it) or difficult on the compile-time/static-analysis
> level.

Bingo! If you CANNOT impose precondition on it, then it is NOT a
precondition.

There is no contract violated when End_Error is raised by file Read. It is
not the contract of Read to be supplied with infinite files!

Since, the discussion is perpetually repeating itself, I will tell you your
next turn: Ada I/O libraries are lousy, should have never used any
exceptions.

>> (Historically, pre-/post-conditions were invented by Dijkstra for the
>> purpose of proving correctness. Later they were used for types to analyze
>> substitutability issues etc.)
> 
> And isn't the idea with Ada's constructs to at least aid proving the
> correctness of a program?

I heard different opinions on that. But since False => True, you could said
so. Unfortunately it is also so that False => False...

> Furthermore, wouldn't it be preferable to throw
> an exception when the condition is violated?

It would be a bug.

The rule is simple: bug is when you cannot continue. Whatever you do having
a bug is another bug.

> That seems to fit perfectly
> with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no?

No, these are not contract violations. When they are pretended to be, they
incur incredible harm.

>>> If that was the case then, strictly speaking
>>> JavaDoc's pre and postcondition annotating comments are superior to Ada's
>>> pre and post condition because they don't implement anything and are, in
>>> fact, just comments having no actual impact on the program text.
>> 
>> Not if condition proof fault makes the program illegal.
> 
> It does nothing, insofar as I know, regarding nprogram correctness.
> http://en.wikipedia.org/wiki/Java_annotation has as an example the
> "override" annotation which when violated only provides a warning.

and?

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:

> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>
>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>
>>>> Putting it even simpler. What is the effect of:
>>>>
>>>>     sqrt (-1.0)
>>>>
>>>> No effect? Any effect?
>>>
>>> This looks like an imaginary problem to me, not a real one.
>>
>> What problem? It was a simple question illustrating absurdity of the idea.
> 
> Actually, a negative argument passed to sqrt is illustrating proper DbC
> well. One famous example is Ariane 4, (4), that's the number four.

If sqrt (-1.0) has no effect, what made Ariane to explode? Exploding is not
an effect, right?

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 06.07.12 10:05, Dmitry A. Kazakov wrote:
> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>
>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>
>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>
>>>>> Putting it even simpler. What is the effect of:
>>>>>
>>>>>      sqrt (-1.0)
>>>>>
>>>>> No effect? Any effect?
>>>>
>>>> This looks like an imaginary problem to me, not a real one.
>>>
>>> What problem? It was a simple question illustrating absurdity of the idea.
>>
>> Actually, a negative argument passed to sqrt is illustrating proper DbC
>> well. One famous example is Ariane 4, (4), that's the number four.
>
> If sqrt (-1.0) has no effect,

First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.

> what made Ariane to explode?

The engineers though the didn't have to re-read the contract
for Ariane 4 when moving the software to Ariane 5.

> Exploding is not an effect, right?

Wrong.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote:

> On 06.07.12 10:05, Dmitry A. Kazakov wrote:
>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>>
>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>>
>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>>
>>>>>> Putting it even simpler. What is the effect of:
>>>>>>
>>>>>>      sqrt (-1.0)
>>>>>>
>>>>>> No effect? Any effect?
>>>>>
>>>>> This looks like an imaginary problem to me, not a real one.
>>>>
>>>> What problem? It was a simple question illustrating absurdity of the idea.
>>>
>>> Actually, a negative argument passed to sqrt is illustrating proper DbC
>>> well. One famous example is Ariane 4, (4), that's the number four.
>>
>> If sqrt (-1.0) has no effect,
> 
> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.

1. That no correct program may have it requires a proof.

2. That no program at all may have it, requires yet another proof.

3. While you are busy proving 1 and 2, I'd rather stay on the safe side
considering sqrt (-1.0) happen. So, what about the effect?

>> what made Ariane to explode?
> 
> The engineers though the didn't have to re-read the contract
> for Ariane 4 when moving the software to Ariane 5.

But that has no effect or else does not occur... thus it never exploded.

>> Exploding is not an effect, right?
>
> Wrong.

Yet explosion occurred. Something must be wrong with the logic again?

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

Re: about the new Ada 2012 pre/post conditions

[Simon Wright]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote:
>
>> On 06.07.12 10:05, Dmitry A. Kazakov wrote:
>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>>>
>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>>>
>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>>>
>>>>>>> Putting it even simpler. What is the effect of:
>>>>>>>
>>>>>>>      sqrt (-1.0)
>>>>>>>
>>>>>>> No effect? Any effect?
>>>>>>
>>>>>> This looks like an imaginary problem to me, not a real one.
>>>>>
>>>>> What problem? It was a simple question illustrating absurdity of
>>>>> the idea.
>>>>
>>>> Actually, a negative argument passed to sqrt is illustrating proper
>>>> DbC well. One famous example is Ariane 4, (4), that's the number
>>>> four.
>>>
>>> If sqrt (-1.0) has no effect,
>> 
>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.
>
> 1. That no correct program may have it requires a proof.

If a DbC program passes a negative argument to sqrt(), then it isn't
correct.

To prove that a DbC program never passes a negative argument to sqrt()
requires a proof (tautology).

No proof is required of the statement that a correct program must not
pass a negative argument to sqrt() - the contract must be regarded as
axiomatic from the caller's pov.

> 2. That no program at all may have it, requires yet another proof.

I can't make sense of this statement.

> 3. While you are busy proving 1 and 2, I'd rather stay on the safe side
> considering sqrt (-1.0) happen. So, what about the effect?

There will be an exception. What's the problem with that?

In my last project, unhandled exceptions caused the system to be
rebooted (and missiles in flight to be aborted). If the system throws an
unhandled exception it's operating outside its design envelope and
safety considerations come in to play.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 06.07.12 11:01, Dmitry A. Kazakov wrote:
> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote:
> 
>> On 06.07.12 10:05, Dmitry A. Kazakov wrote:
>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>>>
>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>>>
>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>>>
>>>>>>> Putting it even simpler. What is the effect of:
>>>>>>>
>>>>>>>      sqrt (-1.0)
>>>>>>>
>>>>>>> No effect? Any effect?
>>>>>>
>>>>>> This looks like an imaginary problem to me, not a real one.
>>>>>
>>>>> What problem? It was a simple question illustrating absurdity of the idea.
>>>>
>>>> Actually, a negative argument passed to sqrt is illustrating proper DbC
>>>> well. One famous example is Ariane 4, (4), that's the number four.
>>>
>>> If sqrt (-1.0) has no effect,
>>
>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.
> 
> 1. That no correct program may have it requires a proof.

Yes, this is why DbC is associated with a proof obligation.

> 2. That no program at all may have it, requires yet another proof.

Who cares? I mean, really, who cares?

Assertion checking is *not* the same as showing that there exists
a class of programs written in a suitably restricted language
that is free of a number of possible errors. It is about
programmers expressing things not expressible in Ada's type
system.

And DbC is about two parties, not just one.

> I'd rather stay on the safe side
> considering sqrt (-1.0) happen. So, what about the effect?

If you know that you might be running an incorrect program,
the effect is similar to that of using Unchecked_Conversion.


>>> what made Ariane to explode?
>>
>> The engineers though the didn't have to re-read the contract
>> for Ariane 4 when moving the software to Ariane 5.
> 
> But that has no effect or else does not occur... thus it never exploded.

"That" = the contract?

If a program is correct, then checking contract clauses does
not have adverse effects. If a program is incorrectly calling
sqrt with a negative argument, there are two practical cases

1) [wrong -1.0 and checks on] detects violation, restarts if possible

2) [wrong -1.0 and checks off] whatever sqrt's body does

Both situations can make the system crash, because it might
not be possible to retry using another, fresh value for r
in case 1). Some have expressed a preference for detection (1) over
erratic performance (2).

I'll note in passing that a check is *not* testing I/O values.
By the Ariane analogy, the original *system* was assumed, correctly,
to guarantee that r >= 0.0. But another, different assembly of
a new system rendered the guarantee void, introducing an explosive bug.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 06 Jul 2012 12:33:33 +0100, Simon Wright wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote:
>>
>>> On 06.07.12 10:05, Dmitry A. Kazakov wrote:
>>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>>>>
>>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>>>>
>>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>>>>
>>>>>>>> Putting it even simpler. What is the effect of:
>>>>>>>>
>>>>>>>>      sqrt (-1.0)
>>>>>>>>
>>>>>>>> No effect? Any effect?
>>>>>>>
>>>>>>> This looks like an imaginary problem to me, not a real one.
>>>>>>
>>>>>> What problem? It was a simple question illustrating absurdity of
>>>>>> the idea.
>>>>>
>>>>> Actually, a negative argument passed to sqrt is illustrating proper
>>>>> DbC well. One famous example is Ariane 4, (4), that's the number
>>>>> four.
>>>>
>>>> If sqrt (-1.0) has no effect,
>>> 
>>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.
>>
>> 1. That no correct program may have it requires a proof.
> 
> If a DbC program passes a negative argument to sqrt(), then it isn't
> correct.

(I don't know want a "DbC program" is)

A correct implementation of a scientific calculator would certainly do that
thing.

>> 2. That no program at all may have it, requires yet another proof.
> 
> I can't make sense of this statement.

This was to prevent an escape into saying that no program were bug-free.
 
>> 3. While you are busy proving 1 and 2, I'd rather stay on the safe side
>> considering sqrt (-1.0) happen. So, what about the effect?
> 
> There will be an exception.

I.e. the effect of it is exception propagation in this case.

> What's the problem with that?

None to me. But for them, the problem is that if they admitted that sqrt
were contracted to raise exception, then that would become a part of sqrt
implementation, and the whole house of cards would collapse.

My point is that the *true* precondition of sqrt is:

   X in Float

And that the true postcondition contains:

   X < 0.0 and Constraint_Error raised

And that there is no any contract violation in calling sqrt(-1.0). The
point is also that any case where contracts are checked dynamically in the
same code can be killed exactly this way.

Contracts of P are not a part of P's behavior.

> In my last project, unhandled exceptions caused the system to be
> rebooted (and missiles in flight to be aborted). If the system throws an
> unhandled exception it's operating outside its design envelope and
> safety considerations come in to play.

Which is why contracted exceptions are so important. You would do in some
client:

   ... sqrt (X) ...

and then add to the postcondition that no Constraint_Error propagates. That
would require you either to prove that X >= 0.0 or else to handle
Constraint_Error.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 06 Jul 2012 14:07:52 +0200, Georg Bauhaus wrote:

> On 06.07.12 11:01, Dmitry A. Kazakov wrote:
>> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote:
>> 
>>> On 06.07.12 10:05, Dmitry A. Kazakov wrote:
>>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote:
>>>>
>>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote:
>>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote:
>>>>>>
>>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote:
>>>>>>>
>>>>>>>> Putting it even simpler. What is the effect of:
>>>>>>>>
>>>>>>>>      sqrt (-1.0)
>>>>>>>>
>>>>>>>> No effect? Any effect?
>>>>>>>
>>>>>>> This looks like an imaginary problem to me, not a real one.
>>>>>>
>>>>>> What problem? It was a simple question illustrating absurdity of the idea.
>>>>>
>>>>> Actually, a negative argument passed to sqrt is illustrating proper DbC
>>>>> well. One famous example is Ariane 4, (4), that's the number four.
>>>>
>>>> If sqrt (-1.0) has no effect,
>>>
>>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur.
>> 
>> 1. That no correct program may have it requires a proof.
> 
> Yes, this is why DbC is associated with a proof obligation.

Yes, yes. Where is the proof?

> And DbC is about two parties, not just one.

And both parties belong to the same program.
 
>> I'd rather stay on the safe side
>> considering sqrt (-1.0) happen. So, what about the effect?
> 
> If you know that you might be running an incorrect program,
> the effect is similar to that of using Unchecked_Conversion.

Maybe for Ada 202X, but in contemporary Ada it is Constraint_Error
propagation.

But wait a minute and re-read what you wrote. You say that the behaviour of
sqrt(-1.0) is basically unspecified. This is where dynamic checks have led
you into.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 06.07.12 15:37, Dmitry A. Kazakov wrote:
> You say that the behaviour of
> sqrt(-1.0) is basically unspecified. This is where dynamic checks have led
> you into.

I said that the behavior of sqrt(-1.0) is basically unspecified
IFF the programmer

(a) violates the contract
(b) turns off contract checking

If the programmer doesn't do this, then the behavior of a program
calling sqrt(-1.0) is specified.

SPARK prevents the foolishness of (a) + (b) in a technical way,
for SPARK programs. General programs require tests at run-time
and programmer intervention. Like pragma Assert does, too.

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 06.07.12 15:37, Dmitry A. Kazakov wrote:
>>> I'd rather stay on the safe side
>>> >> considering sqrt (-1.0) happen. So, what about the effect?
>> > 
>> > If you know that you might be running an incorrect program,
>> > the effect is similar to that of using Unchecked_Conversion.
> Maybe for Ada 202X, but in contemporary Ada it is Constraint_Error
> propagation.

Could you leave clauses of an explicitly state contract in the
text where there was one?

   function sqrt (x : REAL) return REAL
     with   Pre => x >= 0.0;

Ada's sqrt, as opposed to the sqrt above, adds a run-time check,
fully dynamic. The programmer can throw anything at Ada's sqrt,
quite carelessly. Its contract isn't specified in source text,
but requires that the programmer study the language manual in
order to learn about his obligations, and possible consequences.
When not, the program needs to handle Constraint_Error all over
the place because he or she *never* knows what precondition
to establish, other than by reading through more or less formal
comments.

Triply bad. If we had

   function sqrt (x : REAL) return REAL
     with   Pre => True
          Post  => sqrt'result * sqrt'result = x � eps or else *@$!;

instead, then (1) we not only have to handle exceptions, but (2) we cannot
really see from sqrt's specification what to do in order to avoid them,
and (3) we cannot have an efficient sqrt because Ada's sqrt forces
a test on us that is quite unnecessary once we know, i.e. have shown,
that x >= 0.0 is always true before calling sqrt.

So Ada's sqrt is programmed defensively, whereas the line of defence
in a program designed by contract is to feel obliged by the contract
and then either demonstrate correctness, or leave the checks in!

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 06 Jul 2012 18:34:37 +0200, Georg Bauhaus wrote:

> On 06.07.12 15:37, Dmitry A. Kazakov wrote:
> 
>    function sqrt (x : REAL) return REAL
>      with   Pre => True
>           Post  => sqrt'result * sqrt'result = x � eps or else *@$!;

Post =>
   (  X'Valid
   and then
      X >= 0.0
   and then
      (  sqrt'Result * sqrt'Result = X
     or else
         (  sqrt'Result * sqrt'Result > X
        and then
            sqrt'Result * sqrt'Result = X'Succ
         )
     or else
         (  sqrt'Result * sqrt'Result < X
        and then
            sqrt'Result * sqrt'Result = X'Pred
   )  )  )
or else
   (  (not X'Valid or else X < 0.0)
   and then
      Constraint_Error raised
   );

> instead, then (1) we not only have to handle exceptions,

1. Wrong. An exception is still there.

> but (2) we cannot really see from sqrt's specification what to do in order to avoid them,

2. Wrong, it is clearly seen from the post-condition

> and (3) we cannot have an efficient sqrt because Ada's sqrt forces
> a test on us that is quite unnecessary once we know, i.e. have shown,
> that x >= 0.0 is always true before calling sqrt.

3. Wrong. There is no whatsoever difference to dynamic check in that
respect. The implementation is same. That is BTW why there is no such thing
as "dynamic check." And surely the second part of the postcondition can be
ignored if proven that X > 0.0, which would let the optimizing compiler to
deploy a modified body without check.

See, doing things properly is always safer and no less efficient.

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

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net...
> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net...
>>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote:
>> ...
>>>> Legality has nothing to do with preconditions or postconditions.
>>>
>>> => It is OK to violate a "contract" defined by these. Here you are.
>>
>> No, it's not OK; that is the crux of our disagreement. You seem to think
>> that the only kind of "contract" is some sort of static thing.
>
> Exactly. Because the contract exists *before* any programs implementing it
> and after them. The contract exists even when there is no such program.
> Therefore it cannot depend on the program state.
>
> Another way to understand this: a contract describes states of a program.
> As such it cannot depend on them.

That's not my meaning of "contract". It doesn't have anything specific with 
"program states" (whatever the heck you mean by that -- I can't assume any 
reasonable interpretation because you make up terminology all the time).

> Yet another way: the language of contracts is not the object language:

We're not interested in other languages here (this is an Ada forum, after 
all); Ada is the *only* language worth talking about. So by your definition, 
nothing you are talking about is even relevant. Why do you bother? (Why do 
*I* bother? ;-)

...
>> But that's never, ever been true in Ada.
>
> I already said that type constraints are not contracts. E.g. an actual
> value of the discriminant does not create a new contract. The contract
> covers *all* possible values of the discriminant.
>
>> Exactly. You claim that there cannot be such a thing as a dynamically
>> enforced contract.
>
> Absolutely. How could you enforce a contract which has been *already*
> violated? If a program reaches an illegal state, it is in that state.
> Period.

Illegal /= Wrong. An illegal state cannot be reached because you can't 
compile the program. An incorrect state can be reached simply by violating a 
check or contract.

>> But handling exceptions raised for contracts does not make the program 
>> any
>> less wrong;
>
> Really? What is the purpose of the exercise? Raising exception, rolling 
> the
> stack, finalizing stuff, and so on only to resign that the program is as
> wrong as it was before? (Maybe it is even *more* wrong than it was? (:-))

Practicality -- it's not possible to find all program errors before a 
program is fielded. And a lot of programs cannot fail - so that they have to 
have a failback position even when they self-detect that they are internally 
incorrect. It doesn't make the program any less wrong, but it keeps the 
system up so the plane still can land or you can still retrive files for 
www.ada-auth.org.

But if you *could* have detected the "wrong" program earlier, you surely 
would have wanted to, so you could have eliminated the incorrect state.

A whole lot about programming language design is about practicality and not 
about ivory tower exercises. Languages which are purely ivory tower 
exercises rarely have been used off of a college campus.

>>>> The only kind of correctness checks that *can* exist in general are 
>>>> dynamic.
>>>> Ada's entire reason to exist is to include checks like range checks and
>>>> overflow checks to programs. Without them you get the buffer overflows
>>>> and other errors that plague C code.
>>>
>>> Yes, but irrelevant. These checks are not contract checks, because,
>>> otherwise you are in contradiction. No words can change that.
>>
>> Certainly not if you insist on using an unnecessarily limiting definition 
>> of
>> "contract".
>
> Yes, the contract as opposed to the implementation limits the former not 
> to
> be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada
> 2012 "contracts" are implementations [POV #1]. Do you?

No, because I use a very different definition of these terms.

Contract is roughly equivalent to (Ada) specification. Implementation is 
roughly equivalent to (Ada) body.

No caller should *ever* depend in any way on "implementation". (Ada screws 
this up for exceptions and tasking behaviors like blocking and abort.) The 
only things a caller can depend upon is that which is given in the 
specification. And that includes both dynamic and static parts.

Tools which depend in any way on the contents of Ada bodies (other than the 
one they are processing) are limiting and violate the philosophy of Ada. 
Thus we have to get more machine-processable information into the Ada 
specification, so tools can process calls without having to violate 
separation by looking at the implementation (that is, the body).

...
> The actual fallacy is in pretending that a bug can be handled. You can
> handle/be in only anticipated states.

Really? That's certainly not true of my web server or many other programs.

   exception
        when Err:others =>
              Log_Error (Err);
              Reset_to_Known_Good_State;

The above is that the bottom of most of my tasks. I have no idea what state 
the task is in when it gets to this handler; it certainly represents an 
"unanticipated state" in that any state that I actually anticipated has its 
own handlers and recovery mechanisms. But this handler works to recover the 
processing in 99% of the cases (good enough for this application); whatever 
caused the problem is abandoned, and it resets to handle another command.

I suppose you'll twist the terminology around in some bizarre way to claim 
that an unanticipated state - which is the only way to reach this handler - 
is somehow anticipated simply because I can write a handler for it. That's 
of course nonsense - whatever I (or any other programmer) thought of is what 
I anticipated, and there is no way for an outside observer to know anything 
about those. So you cannot reason about those in any useful way - it's an 
irrelevant qualifier.

>> Right. I recall in the past that you've been unwilling to grasp the idea 
>> of
>> bugs being detected at runtime.
>
> Sure, because that is rubbish, and always was:
>
> http://en.wikipedia.org/wiki/Liar_paradox

I don't get it. Just because you cannot detect *all* bugs -- that is, that 
you can't ever make a statement that a program is bug-free -- does not mean 
that you cannot detect *some* bugs. Indeed, this misguided focus on 
absolutes has prevented most practical progress in this area. And you're 
trying hard to prevent progress as well.

I'm obviously wasting my time discussing this with you, so I'm done. (If I 
can resist, I'm surely going to try.)

                                  Randy.

...
>> [As an aside, this means you do not want real exception contracts, since
>> they cannot usefully be done without having it be implementation-defined
>> when an exception is raised by a predefined check. The canonical 
>> semantics
>> of Ada would require assuming that every line raises Storage_Error,
>> Program_Error, and usually Constraint_Error -- that would make it 
>> virtually
>> impossible to eliminate those exceptions from contracts.
>
> I don't see it as a big problem. There is a difference between an
> obligation to raise exception and a possibility that an exception could be
> raised.

No one cares about an "obligation to raise an exception"; I can't imagine 
including those in exception contracts. (Indeed, any such "obligations" 
should be in the precondition or subtype predicates, so they never even 
reach the body of the subprogram.)

The only contracts of interest are the "possibility that an exception could 
be raised", as those probably depend on outside effects (user input, file 
system results, etc.)

...
> The vendors could gradually reduce the number of cases where E may be
> raised without making clients relying on weaker contracts illegal. The
> second cannot be misused to prove that E is raised. It just does not 
> follow
> from the second, and conversely.

I don't see this at all. Once you call a routine that has a contract that 
says "E might be raised", you have to include "E might be raised" in your 
contract as well. This "poisoning" is the major objection to exception 
contracts in practice.

Moreover, if you have a language-defined check that raises E in a subprogram 
S, then you have to include the "E might be raised" contract if you have any 
exception contract at all. That's where the legality comes in. If you allow 
that contract to be omitted if the compiler can prove that the 
language-defined check will not fail (and this is common), then you have an 
implementation-defined legality check. If you *don't* allow that contract to 
be omitted, then you will have to include such a host of "E might be raised" 
contracts on every subprogram that no one would ever use the feature. (There 
are at least 8 common exceptions that could occur in large chunks of my 
code; and almost no code could be without Constraint_Error, Program_Error, 
and Storage_Error.)

I'm pretty certain that the only useful exception contract would have to 
allow check elimination to affect legality -- and that's definitely a 
problem for some. (And they might even be right.) But my feeling is that it 
would be very valuable to specify that a routine does *not* raise 
Constraint_Error, and have the compiler verify (or refute) that fact.

                                                Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:l2v5ycmyjzk.11k6wbda0san5.dlg@40tude.net...
...
> Instead I offered a bait: two options to choose #1 and #2. These two are
> complete and independent. It cannot be both, it cannot be none.

They're only "complete and independent" if and only if "contract" includes 
dynamic contracts. Otherwise, there have to be three things (call the third 
one "specification", if you like). Because there are lots of things that 
don't belong to "implementation" (runtime checking of any sort, for 
instance), and there has to be somewhere to put them.

But I suppose only your worthless terminology can be argued. In which case, 
the answer does not matter, because it is irrelevant to using Ada (or any 
other practical programming language, for that matter).

>> pre- and post-conditions most of the method you
>> seem to be advocating is impossible
>
> 1. SPARK
> 2. Proving correctness of all program >>> proving correctness of contracts

Proving complete correctness of a program is a pointless, impossible 
exercise. Real SPARK programs exclude such a large portion of the code, it's 
unlikely that they've actually proved anything of value.

The only real hope is combining static and dynamic checks to improve the 
correctness of programs. (Absolutely nothing will cause programs to be 100% 
correct in practice -- why even try?)

...
> There is no contract violated when End_Error is raised by file Read. It is
> not the contract of Read to be supplied with infinite files!

Certainly not. End_Error is clearly not part of the precondition of Read. 
Mode_Error, OTOH, might be.

It doesn't help to take up straw men, you know.

It's not possible to write contracts why all exceptions, for every possible 
exit condition of a subprogram. In *any* language. Nothing about this is 
about ALL. It's all about MOST. You continue to insist on arguing about ALL. 
No one cares about ALL, because it is impractical if not impossible.

> Since, the discussion is perpetually repeating itself, I will tell you 
> your
> next turn: Ada I/O libraries are lousy, should have never used any
> exceptions.

Huh? The problem is your insistence on straw men. The only contract that 
makes sense for Read is "might raise End_Error". There is no possible 
description of why. And no one anywhere ever said that End_Error should be 
in a precondition, and certainly not that all exceptions should be in a 
precondition. I've only said that SOME exceptions should be in a 
precondition, because violating them is a bug. And only the programmer can 
determine which makes sense for a particular subprogram -- there cannot be a 
hard rule about that.

End_Error being raised by Read is perfectly normal. Mode_Error being raised 
by Read is a serious bug. So what?

You seem to want hard rules, but that is not how anything works in the real 
world. After all, "everything is legal so long as you don't get caught" 
(Traveling Wilburys).

...
>> That seems to fit perfectly
>> with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no?
>
> No, these are not contract violations. When they are pretended to be, they
> incur incredible harm.

What harm? The program is wrong when these happen. It should be fixed if 
practical. If it cannot be fixed, Ada lets you handle them to recover - but 
this is not something that should be relied on.

If there is a harm, it's that you can't tell between these used as a 
contract and these used as an implementation artifact (say, handling an 
overflow error). It would have been nice to differentiate, but that was not 
done in Ada 83 and it is way too late now. You could of course get that 
effect by eliminating all of the constraints from your program and using 
Preconditions and Predicates instead -- that would get all contract failures 
raising Assertion_Error.

                                      Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:7xnkuta2d94n$.1815f9iev4s7r$.dlg@40tude.net...
...
> But wait a minute and re-read what you wrote. You say that the behaviour 
> of
> sqrt(-1.0) is basically unspecified. This is where dynamic checks have led
> you into.

If you suppress checks, basically the behavior of all programs are 
unspecified. Thus, I highly recommend that you don't do that. (Consider 
Suppress similar to Unchecked_Conversion -- OK when used in the right hands, 
dangerous otherwise.)

If you *don't* suppress checks, the behavior is well-defined. So what?

                                    Randy.

Re: about the new Ada 2012 pre/post conditions

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net...
...
> 1. Wrong. An exception is still there.

Sure, but the compiler can prove that it will not be raised (at least part 
of the time). The Sqrt in the LRM has not such possibility; a caller would 
always have to assume that it is raised.

>> but (2) we cannot really see from sqrt's specification what to do in 
>> order to avoid them,
>
> 2. Wrong, it is clearly seen from the post-condition

It was clear as mud to me.

         Pre => (if A < 0.0 then raise Constraint_Error);

is a *lot* clearer to me.

>> and (3) we cannot have an efficient sqrt because Ada's sqrt forces
>> a test on us that is quite unnecessary once we know, i.e. have shown,
>> that x >= 0.0 is always true before calling sqrt.
>
> 3. Wrong. There is no whatsoever difference to dynamic check in that
> respect. The implementation is same. That is BTW why there is no such 
> thing
> as "dynamic check." And surely the second part of the postcondition can be
> ignored if proven that X > 0.0, which would let the optimizing compiler to
> deploy a modified body without check.

Definitely wrong. Any decent compiler will completely eliminate the dynamic 
check on the precondition given above (presuming the actual value allows 
that). (Preconditions are checked at the call site, not inside the body.) No 
compiler can eliminate a dynamic check written in a body. So the generated 
code will be very different.

                                         Randy.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 6 Jul 2012 19:43:08 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net...
>> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:

>>> Exactly. You claim that there cannot be such a thing as a dynamically
>>> enforced contract.
>>
>> Absolutely. How could you enforce a contract which has been *already*
>> violated? If a program reaches an illegal state, it is in that state.
>> Period.
> 
> Illegal /= Wrong. An illegal state cannot be reached because you can't 
> compile the program. An incorrect state can be reached simply by violating a 
> check or contract.

"violating the contract enforced by the contract check", you should have
said.

>>> But handling exceptions raised for contracts does not make the program 
>>> any less wrong;
>>
>> Really? What is the purpose of the exercise? Raising exception, rolling the
>> stack, finalizing stuff, and so on only to resign that the program is as
>> wrong as it was before? (Maybe it is even *more* wrong than it was? (:-))
> 
> Practicality -- it's not possible to find all program errors before a 
> program is fielded.

No practical reasons may do wrong right. I see no practical gain in calling
implementations contracts.

>>>>> The only kind of correctness checks that *can* exist in general are dynamic.
>>>>> Ada's entire reason to exist is to include checks like range checks and
>>>>> overflow checks to programs. Without them you get the buffer overflows
>>>>> and other errors that plague C code.
>>>>
>>>> Yes, but irrelevant. These checks are not contract checks, because,
>>>> otherwise you are in contradiction. No words can change that.
>>>
>>> Certainly not if you insist on using an unnecessarily limiting definition of
>>> "contract".
>>
>> Yes, the contract as opposed to the implementation limits the former not to
>> be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada
>> 2012 "contracts" are implementations [POV #1]. Do you?
> 
> No, because I use a very different definition of these terms.
> 
> Contract is roughly equivalent to (Ada) specification. Implementation is 
> roughly equivalent to (Ada) body.

That does not change anything. There are two kind entities involved A and
B. The check may be attributed to either A or B. It is not a question of
terminology.

>> The actual fallacy is in pretending that a bug can be handled. You can
>> handle/be in only anticipated states.
> 
> Really? That's certainly not true of my web server or many other programs.
> 
>    exception
>         when Err:others =>
>               Log_Error (Err);
>               Reset_to_Known_Good_State;
>
> The above is that the bottom of most of my tasks. I have no idea what state 
> the task is in when it gets to this handler;

But you have some ideas about the state of the log, about the meaning of
the object Err, about the overall state of your program, such that
Reset_to_Known_Good_State might work.

> I suppose you'll twist the terminology around in some bizarre way to claim 
> that an unanticipated state - which is the only way to reach this handler - 
> is somehow anticipated simply because I can write a handler for it.

Yes. Merely by the fact that the program continues.

Think about it from the angle of preconditions. In ANY state of the program
the preconditions of this state are met. You are going to do

   Log_Error (Err);
   Reset_to_Known_Good_State;

BECAUSE the precondition "some unhandled exception is propagating" is TRUE.
(Would you claim that precondition FALSE?)

>>> [As an aside, this means you do not want real exception contracts, since
>>> they cannot usefully be done without having it be implementation-defined
>>> when an exception is raised by a predefined check. The canonical semantics
>>> of Ada would require assuming that every line raises Storage_Error,
>>> Program_Error, and usually Constraint_Error -- that would make it virtually
>>> impossible to eliminate those exceptions from contracts.
>>
>> I don't see it as a big problem. There is a difference between an
>> obligation to raise exception and a possibility that an exception could be
>> raised.
> 
> No one cares about an "obligation to raise an exception";

Numeric errors, e.g. overflow and zero-divide must raise.

Another important example is when a constructing operation is implemented
like:

  function Create (...) return Boo is
  begin
      raise Use_Error; 
      return Boo;
  end Create;

>> The vendors could gradually reduce the number of cases where E may be
>> raised without making clients relying on weaker contracts illegal. The
>> second cannot be misused to prove that E is raised. It just does not 
>> follow from the second, and conversely.
> 
> I don't see this at all. Once you call a routine that has a contract that 
> says "E might be raised", you have to include "E might be raised" in your 
> contract as well.

No.

1. It is always "E might be raised AND Condition." It might be possible to
prove not Condition. E.g. x + y might raise Constraint_Error if sum is out
of range (or else yield the mathematically correct result). If you can
prove x + y in the range, you don't have Constraint_Error.

2. It you cannot prove not Condition, you still can handle E.

The main practical purpose of exception contracts is to ensure them
handled, rather than attempting to prevent exceptions from being raised.

> This "poisoning" is the major objection to exception 
> contracts in practice.

It cannot be otherwise. Any uncertainty about the condition when an
exception may appear is necessarily propagates to all clients. This cannot
be changed otherwise than by reducing uncertainty:

- at the client side, e.g. through 1 or 2.
- at the callee's side, e.g. strengthening the condition.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 6 Jul 2012 20:09:32 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:l2v5ycmyjzk.11k6wbda0san5.dlg@40tude.net...
> ...
>> Instead I offered a bait: two options to choose #1 and #2. These two are
>> complete and independent. It cannot be both, it cannot be none.
> 
> They're only "complete and independent" if and only if "contract" includes 
> dynamic contracts. Otherwise, there have to be three things (call the third 
> one "specification", if you like).

#3 specification.

So, dynamic checks belong to specifications? It gets better every day...

>> There is no contract violated when End_Error is raised by file Read. It is
>> not the contract of Read to be supplied with infinite files!
> 
> Certainly not. End_Error is clearly not part of the precondition of Read. 

I.e. you agree that exceptions are not necessarily errors. I am glad to
hear that, because others claimed that all exceptions are errors.

Now, Constraint_Error is an error and End_Error is not so error? Right?

> End_Error being raised by Read is perfectly normal. Mode_Error being raised 
> by Read is a serious bug. So what?

I would like to know why Mode_Error is a "serious  bug," while End_Error is
no bug at all. What in the *language* makes them different?

> You seem to want hard rules, but that is not how anything works in the real 
> world. After all, "everything is legal so long as you don't get caught" 
> (Traveling Wilburys).

No, I want *clear* terms without false excuses about practicality. Now, it
is utterly IMPRACTICAL to draw lines between End_Error, Mode_Error,
Constraint_Error. They all belong to the implementation. All cases when
raised must be contracted formally or informally.

>>> That seems to fit perfectly
>>> with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no?
>>
>> No, these are not contract violations. When they are pretended to be, they
>> incur incredible harm.
> 
> What harm? The program is wrong when these happen.

See above. You are trying to prescribe semantics of a program you never
saw.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 6 Jul 2012 20:24:39 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net...
> ...
>>> but (2) we cannot really see from sqrt's specification what to do in 
>>> order to avoid them,
>>
>> 2. Wrong, it is clearly seen from the post-condition
> 
> It was clear as mud to me.
> 
>          Pre => (if A < 0.0 then raise Constraint_Error);
> 
> is a *lot* clearer to me.

Precondition is a predicate. Predicate is a Boolean valued function per
definition.

http://en.wikipedia.org/wiki/Predicate_%28mathematical_logic%29

It cannot raise anything. The formula above is meaningless, shows how
damaging if-operator stuff could become. The proper precondition of sqrt
that does not raise [we hope that it would not, but for "practical reasons"
take that it does not] is:

   Pre => A >= 0.0    (and A'Valid)

The precondition of sqrt that does raise is:

   Pre => True

The postcondiion is also a predicate, which could only state that
Constraint_Error is underway, e.g.:

   Post => ... (A < 0.0 and Constraint_Error RAISED) ...;

If exception will ever be contracted, you would never see them in
preconditions.

From the proof POV, there is no difference. Both are equivalently difficult
or simple to prove, because it is essentially A < 0.0.

>>> and (3) we cannot have an efficient sqrt because Ada's sqrt forces
>>> a test on us that is quite unnecessary once we know, i.e. have shown,
>>> that x >= 0.0 is always true before calling sqrt.
>>
>> 3. Wrong. There is no whatsoever difference to dynamic check in that
>> respect. The implementation is same. That is BTW why there is no such thing
>> as "dynamic check." And surely the second part of the postcondition can be
>> ignored if proven that X > 0.0, which would let the optimizing compiler to
>> deploy a modified body without check.
> 
> Definitely wrong. Any decent compiler will completely eliminate the dynamic 
> check on the precondition given above (presuming the actual value allows 
> that).

This is what I wrote.

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Fri, 6 Jul 2012 20:18:31 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:7xnkuta2d94n$.1815f9iev4s7r$.dlg@40tude.net...
> ...
>> But wait a minute and re-read what you wrote. You say that the behaviour of
>> sqrt(-1.0) is basically unspecified. This is where dynamic checks have led
>> you into.
> 
> If you suppress checks, basically the behavior of all programs are 
> unspecified.

There was no *IF*.

> If you *don't* suppress checks, the behavior is well-defined. So what?

That the same function's behavior might be both defined and undefined.
There must be something wrong with that function, the definition of
"behavior", dynamic checks, Georg's statements. The choice is up to the
reader.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 07.07.12 10:06, Dmitry A. Kazakov wrote:
>> Contract is roughly equivalent to (Ada) specification. Implementation is
>> roughly equivalent to (Ada) body.

> There are two kind entities involved A and
> B. The check may be attributed to either A or B.

There is no need for such attribution. Indeed, assertion monitoring
(note the word) ideally works like in the following illustration.

Monitoring here uses a monitoring processor (not an Ada thing,
but a conceptual thing to which an Ada compiler can supply suitable code).
Let there be a procedure that adds 42 to its argument (in out) unless
adding 42 makes the result too large. Let the argument be passed in r1.

add_42:
         load    $2A, r2           # 42 in r2
         add     r2, r1            # X := X + 42;
         *return

call_add_42:
         load    $0, r1            # X := 0;
         *call   add_42            # Add_42 (X);
         store   r1, (#output)     # print X
         *return

The monitor can be turned on or off. The special instructions [X]call
and [X]return can be monitored.  When monitoring is on, then an
auxiliary processor is hooked up to *call and/or *return. It can
read all data that the program can read, too.

When monitoring, any *call or *return will make the monitor evaluate
the corresponding assertions. If they are true, the system continues
executing the program. If they are false, the system prints a diagnostic
message and stops.

If "r1 is too large" means "r1 > 968", then this is the assertion associated
with calling add_42.  The monitor will test the assertion when "*call add_42"
is the next instruction to be performed, and monitoring of calls has
been  turned on.

The point is that the "program proper", i.e. the list of instructions,
is the very same irrespective of monitoring assertions.

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sat, 07 Jul 2012 13:17:52 +0200, Georg Bauhaus wrote:

> On 07.07.12 10:06, Dmitry A. Kazakov wrote:
>>> Contract is roughly equivalent to (Ada) specification. Implementation is
>>> roughly equivalent to (Ada) body.
> 
>> There are two kind entities involved A and
>> B. The check may be attributed to either A or B.
> 
> There is no need for such attribution.

Still, it is either A or B.

> The point is that the "program proper", i.e. the list of instructions,
> is the very same irrespective of monitoring assertions.

The program is not a list of instructions. The latter is called "code" of
the program. But the error is *very* telling.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 07.07.12 11:14, Dmitry A. Kazakov wrote:
> That the same function's behavior might be both defined and undefined.

The function's behavior is not affected by assertion checking:

A DbC function computes as if it its pre condition were true.

Whatever the caller is going to pass to sqrt, the function sqrt corresponds
to a sequence of instructions that compute a value from a float argument
that is taken to be >= 0.0.  Reason: it was stated in the contract.

"shocking at first to many, it is among the method's main contributions
to software reliability and deserves emphasis." (OOSC2, � 11.6)

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 07.07.12 13:31, Dmitry A. Kazakov wrote:

>>> There are two kind entities involved A and
>>> B. The check may be attributed to either A or B.
>>
>> There is no need for such attribution.
>
> Still, it is either A or B.

You did notice that monitoring behavior is outside the behavior
that the program given  will contribute?

> The program is not a list of instructions. The latter is called "code" of
> the program.

The list of instruction is the program that the compiler produces from
an Ada program. The program given, the list of instructions, is one in
the set of the only programs that can have any effect.

> But the error is *very* telling.

It's again the dogma versus dogma thing. Still takes time
to nail down ...

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sat, 07 Jul 2012 14:06:46 +0200, Georg Bauhaus wrote:

> On 07.07.12 11:14, Dmitry A. Kazakov wrote:
>> That the same function's behavior might be both defined and undefined.
> 
> The function's behavior is not affected by assertion checking:

Whatever it be. You wrote about the effect of sqrt exactly this:

"the effect is similar to that of using Unchecked_Conversion."

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

Re: about the new Ada 2012 pre/post conditions

[Dmitry A. Kazakov]

On Sat, 07 Jul 2012 14:21:45 +0200, Georg Bauhaus wrote:

> On 07.07.12 13:31, Dmitry A. Kazakov wrote:
> 
>>>> There are two kind entities involved A and
>>>> B. The check may be attributed to either A or B.
>>>
>>> There is no need for such attribution.
>>
>> Still, it is either A or B.
> 
> You did notice that monitoring behavior is outside the behavior
> that the program given  will contribute?

How exception propagation could be outside the behavior? I gather there is
behavior and misbehavior? Dynamic checks must be the second. Now we are on
the same page!

>> The program is not a list of instructions. The latter is called "code" of
>> the program.
> 
> The list of instruction is the program that the compiler produces from
> an Ada program. The program given, the list of instructions, is one in
> the set of the only programs that can have any effect.
> 
>> But the error is *very* telling.
> 
> It's again the dogma versus dogma thing.

It is confusion of program and the semantics thereof. Just like with
contracts and implementations.

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

Re: about the new Ada 2012 pre/post conditions

[Georg Bauhaus]

On 07.07.12 14:54, Dmitry A. Kazakov wrote:
> On Sat, 07 Jul 2012 14:06:46 +0200, Georg Bauhaus wrote:
>
>> On 07.07.12 11:14, Dmitry A. Kazakov wrote:
>>> That the same function's behavior might be both defined and undefined.
>>
>> The function's behavior is not affected by assertion checking:
>
> Whatever it be. You wrote about the effect of sqrt exactly this:
>
> "the effect is similar to that of using Unchecked_Conversion."

Yes, the function's behavior is according to both sides of the
stated contract.

Continuing the Unchecked_Conversion analogy,
there are safe uses of Unchecked_Conversion. Improving Ada 2005,
a full DbC method allows formalizing these safe use cases to the extent
possible in each case. For example, it is safe to call sqrt if the caller
ensures the conditions stated in the explicit contract of my_sqrt.