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

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

[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

[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

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

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

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

[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

[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

[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;

[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

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

[Robert A Duff]

"Jeffrey R. Carter" <gg...@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

[Georg Bauhaus]

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?

[Randy Brukardt]

"Nasser M. Abbasi" <n...@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.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@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.

[Randy Brukardt]

"Jeffrey R. Carter" <gg...@pragmada.co.cc> wrote in message
news:4f0d55a9-83e1-44fe...@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.

[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 ne...@netfront.net ---

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mai...@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.

[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

[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;

[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/

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

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

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

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

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

[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! (:-))

[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?

[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 :-)

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

[Randy Brukardt]

"Jeffrey Carter" <spam.jrc...@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.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@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" <mai...@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.

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mai...@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" <mai...@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.

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

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

[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)?

[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?

[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?

[Dmitry A. Kazakov]

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?

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

[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

[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

[Georg Bauhaus]

That's what true exceptions always are.

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

[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?

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

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

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

[stefan...@see-the.signature]

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

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 16:08:01 +0200, stefan...@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?

[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

[stefan...@see-the.signature]

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.

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

[Dmitry A. Kazakov]

On Mon, 25 Jun 2012 18:26:18 +0200, stefan...@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).

[stefan...@see-the.signature]

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.

[Dmitry A. Kazakov]

On Tue, 26 Jun 2012 13:50:28 +0200, stefan...@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.

[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?

[stefan...@see-the.signature]

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

> On Tue, 26 Jun 2012 13:50:28 +0200, stefan...@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!

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

[Dmitry A. Kazakov]

On Tue, 26 Jun 2012 16:54:45 +0200, stefan...@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.

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

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

[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

[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!

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

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

[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

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

[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;

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

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

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

[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" <mai...@dmitry-kazakov.de> wrote in message
news:1oih2rok18dmt.a...@40tude.net...
> On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mai...@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" <mai...@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.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:bdpvyb9h7rvt.z...@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.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...

> On Tue, 26 Jun 2012 13:50:28 +0200, stefan...@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.

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message

> news:1oih2rok18dmt.a...@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.

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mai...@dmitry-kazakov.de> wrote in message
> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan...@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.

[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?

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

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

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

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@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" <mai...@dmitry-kazakov.de> wrote in message
>> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan...@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.

[Randy Brukardt]

"Dmitry A. Kazakov" <mai...@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.

[Shark8]

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.

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

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mai...@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" <mai...@dmitry-kazakov.de> wrote in message
>>> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net...
>>>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan...@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?

[Dmitry A. Kazakov]

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

> "Dmitry A. Kazakov" <mai...@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.

[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" <mai...@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.

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

[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" <mai...@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.

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

[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

[Dmitry A. Kazakov]

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.

[Dmitry A. Kazakov]

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

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

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

[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? ;-) ;-)

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

[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?