* about the new Ada 2012 pre/post conditions @ 2012-06-20 13:39 Nasser M. Abbasi 2012-06-20 14:02 ` Georg Bauhaus ` (4 more replies) 0 siblings, 5 replies; 125+ messages in thread From: Nasser M. Abbasi @ 2012-06-20 13:39 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi @ 2012-06-20 14:02 ` Georg Bauhaus 2012-06-20 14:13 ` Dmitry A. Kazakov ` (3 subsequent siblings) 4 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-20 14:02 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi 2012-06-20 14:02 ` Georg Bauhaus @ 2012-06-20 14:13 ` Dmitry A. Kazakov 2012-06-20 14:24 ` Nasser M. Abbasi 2012-06-20 19:18 ` Anh Vo ` (2 subsequent siblings) 4 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-20 14:13 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 14:13 ` Dmitry A. Kazakov @ 2012-06-20 14:24 ` Nasser M. Abbasi 2012-06-20 14:37 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Nasser M. Abbasi @ 2012-06-20 14:24 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 14:24 ` Nasser M. Abbasi @ 2012-06-20 14:37 ` Dmitry A. Kazakov 2012-06-20 17:02 ` Georg Bauhaus 2012-06-21 20:32 ` Randy Brukardt 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-20 14:37 UTC (permalink / raw) On Wed, 20 Jun 2012 09:24:48 -0500, Nasser M. Abbasi wrote: > On 6/20/2012 9:13 AM, Dmitry A. Kazakov wrote: >> On Wed, 20 Jun 2012 08:39:50 -0500, Nasser M. Abbasi wrote: >> >> [...] >>> But, and here is the problem, when I turn off assertions, I am >>> now left with the push() function with no check at all for >>> the case of the stack is full. >>> >>> So, what is one to do? use pre/post AND also add >>> an extra check for full stack in the code as before? >>> does not make sense. >> >> This is what constitutes the core inconsistency about dynamic >> pre-/post-conditions. If they #1 implement behavior (e.g the stack contract >> to raise something when full), then they cannot be suppressed and do not >> describe the contract. If they do describe the contract #2, they may not >> implement it and thus shall have no run-time effect. > > That is what I was thinking. So, I guess I am not alone. Two of us, to be precise. >>> They seem to definitely be something good to have. >> >> Not everything is what it seems... > > Since I myself have no experience in contract programming, > I have to wait and see how they work out. I assume they > must be good thing to have, to make the program more > robust,but if used correctly. No, it is impossible to use correctly what is incorrect. Choose #1 or #2, the rest will follow automatically. > When exceptions were new thing, many started using them in > place of the old fashioned if/then to check for > error in logic and just return an error code. Many are still confused about it. Independently on exceptions, it is inconsistent for a program to check the consistency, correctness, logic etc of its own by whatever means. Correctness to be checked statically or dynamically by an *independent* program. > Will have to wait for gnat Ada 2012 to come out and start > using them to find out. No. If you want #2, use SPARK (because contracts *shall* be checked statically). If you want #1, use if- and case-statements (because the program *shall* implement what it was contract for). Period. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 14:37 ` Dmitry A. Kazakov @ 2012-06-20 17:02 ` Georg Bauhaus 2012-06-20 18:28 ` Dmitry A. Kazakov 2012-06-21 20:32 ` Randy Brukardt 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-20 17:02 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 17:02 ` Georg Bauhaus @ 2012-06-20 18:28 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-20 18:28 UTC (permalink / raw) On Wed, 20 Jun 2012 19:02:37 +0200, Georg Bauhaus wrote: > On 20.06.12 16:37, Dmitry A. Kazakov wrote: > >> Correctness to be checked statically or dynamically by an *independent* >> program. > > Yes, the independent program that checks the assertions is us, > fixing bugs (a.k.a. correcting partial proofs). Yes, of course. This process is called "code review." > Nevertheless, if conditions/assumptions/assertions are > formally expressible, and *determinable* for the checker being considered. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 14:37 ` Dmitry A. Kazakov 2012-06-20 17:02 ` Georg Bauhaus @ 2012-06-21 20:32 ` Randy Brukardt 2012-06-22 7:23 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-06-21 20:32 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net... ... > This is what constitutes the core inconsistency about dynamic > pre-/post-conditions. If they #1 implement behavior (e.g the stack > contract > to raise something when full), then they cannot be suppressed and do not > describe the contract. If they do describe the contract #2, they may not > implement it and thus shall have no run-time effect. You're right, but I don't see any inconsistency. They are clearly #1, and that includes all of the existing Ada checks as well. And you are right, it *never* makes logical sense in Ada to suppress or ignore anything. They *are* part of the contract. The old saw about wearing seatbelts in the garage and taking them off when you leave is totally in operation here. The *only* reason to suppress or ignore checks is for performance reasons, and those are clearly outside of any program logic. Moreover, this should be very rare, since this should only happen in the very narrow band when the program is too slow with the checks on and fast enough with them off (most programs will be fast enough always, and most of the rest will be too slow always). I know Bob and some others disagree with this, and they're just outright wrong. (In part because I don't believe in requiring any checks as part of the contract that are too expensive to leave on always. The sorts of assertions that you might want to suppress because they are too expensive should *never* be part of the contract and I think they should be categorized differently from those that are part of the contract. But I found no traction for that idea, unfortunately.) Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-21 20:32 ` Randy Brukardt @ 2012-06-22 7:23 ` Dmitry A. Kazakov 2012-06-22 11:54 ` Georg Bauhaus 2012-06-22 19:41 ` Randy Brukardt 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-22 7:23 UTC (permalink / raw) On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net... > ... >> This is what constitutes the core inconsistency about dynamic >> pre-/post-conditions. If they #1 implement behavior (e.g the stack contract >> to raise something when full), then they cannot be suppressed and do not >> describe the contract. If they do describe the contract #2, they may not >> implement it and thus shall have no run-time effect. > > You're right, but I don't see any inconsistency. They are clearly #1, and > that includes all of the existing Ada checks as well. If you take a stance on #1, then checking stack full is no more evaluation of the precondition, which does not depend on the stack state anymore, as it of course should be. So the "true" precondition is just: True. Then why on earth anybody would denote it as: Pre => not Is_Full (S) And implementations leaking into declarations is certainly a very bad idea. An even worse idea is to slice implementations into parts of unclear purpose. Instead of one package body, the maintainer will have to inspect the body, and so-.called pre-/post-conditions slices. Neither #1 nor #2 is defendable. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 7:23 ` Dmitry A. Kazakov @ 2012-06-22 11:54 ` Georg Bauhaus 2012-06-22 12:39 ` Georg Bauhaus 2012-06-22 12:43 ` Dmitry A. Kazakov 2012-06-22 19:41 ` Randy Brukardt 1 sibling, 2 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 11:54 UTC (permalink / raw) 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; ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 11:54 ` Georg Bauhaus @ 2012-06-22 12:39 ` Georg Bauhaus 2012-06-22 12:43 ` Dmitry A. Kazakov 1 sibling, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 12:39 UTC (permalink / raw) 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/ ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 11:54 ` Georg Bauhaus 2012-06-22 12:39 ` Georg Bauhaus @ 2012-06-22 12:43 ` Dmitry A. Kazakov 2012-06-22 14:30 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-22 12:43 UTC (permalink / raw) On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote: > On 22.06.12 09:23, Dmitry A. Kazakov wrote: >> Neither #1 nor #2 is defendable. > > Maybe dynamic checking is not defendable when the attack is > based on some biased, and, frankly, narrow set of assumptions. Sure, the most effective defence is just not to take any position. You might get exposed otherwise. BTW, narrower the set of assumptions is, wider is the context where the conclusion stays true. I would not be so proud about liberally sweeping assumptions, they may occasionally include flat earth or the Moon composed of cheese... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 12:43 ` Dmitry A. Kazakov @ 2012-06-22 14:30 ` Georg Bauhaus 2012-06-22 14:36 ` Georg Bauhaus 2012-06-22 15:05 ` Dmitry A. Kazakov 0 siblings, 2 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 14:30 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 14:30 ` Georg Bauhaus @ 2012-06-22 14:36 ` Georg Bauhaus 2012-06-22 15:05 ` Dmitry A. Kazakov 1 sibling, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 14:36 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 14:30 ` Georg Bauhaus 2012-06-22 14:36 ` Georg Bauhaus @ 2012-06-22 15:05 ` Dmitry A. Kazakov 2012-06-22 15:52 ` Georg Bauhaus 2012-06-22 16:45 ` Georg Bauhaus 1 sibling, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-22 15:05 UTC (permalink / raw) On Fri, 22 Jun 2012 16:30:52 +0200, Georg Bauhaus wrote: > On 22.06.12 14:43, Dmitry A. Kazakov wrote: >> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote: >> >>> On 22.06.12 09:23, Dmitry A. Kazakov wrote: >>>> Neither #1 nor #2 is defendable. >>> >>> Maybe dynamic checking is not defendable when the attack is >>> based on some biased, and, frankly, narrow set of assumptions. >> >> Sure, the most effective defence is just not to take any position. You >> might get exposed otherwise. > > Who isn't taking a position? You. On the contrary, Randy was unambiguously clear that he supports #1. You might also be surprised by Robert Dewar's opinion on and around the subject, see recent discussion in LinkedIn, group: "Ada Programming Language", thread: "Imaginary proposal for the next Ada standard: Ada compilers will automatically generate Package Specification from Package Body" (He was ready to debunk use of exceptions, to dismiss design of Ada I/O. People could do anything in order to save dynamic checks! (:-)) >> BTW, narrower the set of assumptions is, wider is the context where the >> conclusion stays true. > > As context is widened, the set of assumptions being narrowed, > the more specific and less informative the full text. > Context widening forces a general concept such as pre/post > to be specific, which it isn't. No, you cannot narrow any context so that laws of logic would not apply. If you wanted to make an inherently inconsistent concept working, you would have to rather widen the context to include alogical things and false inherence. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 15:05 ` Dmitry A. Kazakov @ 2012-06-22 15:52 ` Georg Bauhaus 2012-06-22 16:35 ` Dmitry A. Kazakov 2012-06-22 16:45 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 15:52 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 15:52 ` Georg Bauhaus @ 2012-06-22 16:35 ` Dmitry A. Kazakov 2012-06-22 16:53 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-22 16:35 UTC (permalink / raw) On Fri, 22 Jun 2012 17:52:53 +0200, Georg Bauhaus wrote: > The world happens, including computers, and the laws of logic are > far too insufficient to capture it. Great, now we are in cordial agreement that dynamic checks of Ada 2012 are in breach with laws of logic! (:-)) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 16:35 ` Dmitry A. Kazakov @ 2012-06-22 16:53 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 16:53 UTC (permalink / raw) 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 :-) ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 15:05 ` Dmitry A. Kazakov 2012-06-22 15:52 ` Georg Bauhaus @ 2012-06-22 16:45 ` Georg Bauhaus 2012-06-22 17:24 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-22 16:45 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 16:45 ` Georg Bauhaus @ 2012-06-22 17:24 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-22 17:24 UTC (permalink / raw) On Fri, 22 Jun 2012 18:45:16 +0200, Georg Bauhaus wrote: > On 22.06.12 17:05, Dmitry A. Kazakov wrote: >> On Fri, 22 Jun 2012 16:30:52 +0200, Georg Bauhaus wrote: >> >>> On 22.06.12 14:43, Dmitry A. Kazakov wrote: >>>> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote: >>>> >>>>> On 22.06.12 09:23, Dmitry A. Kazakov wrote: >>>>>> Neither #1 nor #2 is defendable. >>>>> >>>>> Maybe dynamic checking is not defendable when the attack is >>>>> based on some biased, and, frankly, narrow set of assumptions. >>>> >>>> Sure, the most effective defence is just not to take any position. You >>>> might get exposed otherwise. >>> >>> Who isn't taking a position? >> >> You. > > I don't think that #1 xor #2 can be the basis of a meaningful > discussion of DbC, because of the frames of reference. #1 and #2 are mutually exclusive and complete. The rest is hand waving. >> (He was ready to debunk use of exceptions, to dismiss design of Ada I/O. > > A similar comment on omitting exceptions might be circulated with Parasail, > I think. The same Robert Dewar, lecturing at MIT, praises exceptions, > comparing them to C's solution (checking return values all along). > > Could this conviction and readiness to debunk exceptions be > a consequence of running a particular business, the small and > profitable niche of immensely well funded high tech? Robert Dewar seem to consider exceptions as manifestations of contract violations. That immediately leads to rejection of exceptions, on the obvious basis that the contracts must be respected. The next step is, of course, that any program raising exceptions is illegal. This is the point where the proponents of #2 providently disconnect, because legality is to be checked statically. >> People could do anything in order to save dynamic checks! (:-)) > > Can you report the gist of the argument? I cannot honestly summarize his argument, because as I said, there is no way to make it. It is inconsistent. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 7:23 ` Dmitry A. Kazakov 2012-06-22 11:54 ` Georg Bauhaus @ 2012-06-22 19:41 ` Randy Brukardt 2012-06-22 23:08 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-06-22 19:41 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net... > On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net... >> ... >>> This is what constitutes the core inconsistency about dynamic >>> pre-/post-conditions. If they #1 implement behavior (e.g the stack >>> contract >>> to raise something when full), then they cannot be suppressed and do not >>> describe the contract. If they do describe the contract #2, they may not >>> implement it and thus shall have no run-time effect. >> >> You're right, but I don't see any inconsistency. They are clearly #1, and >> that includes all of the existing Ada checks as well. > > If you take a stance on #1, then checking stack full is no more evaluation > of the precondition, which does not depend on the stack state anymore, as > it of course should be. So the "true" precondition is just: True. Huh? This makes no sense whatsoever. We can't require static detection of precondition failures any more than we can demand static detection of range violations. And Ada *always* has had dynamic preconditions: procedure New_Line (Spacing : in Positive_Count := 1); Here, the precondition is "Spacing in Positive_Count". Your contention that a dynamic expression cannot be a precondition is the same as saying that no parameter can include a range (and thus ought be written as Count'Base above). ... > And implementations leaking into declarations is certainly a very bad > idea. This is NOT implementation; it's part of the contract. For the vast majority of subprograms, callers aren't supposed to call routines such that an exception is raised; it represents a bug. The only question is to whether those conditions are expressed in executable terms or in comments. For instance, the containers have operations like: procedure Insert_Space (Container : in out Vector; Before : in Extended_Index; Count : in Count_Type := 1); If Before is not in the range First_Index (Container) .. Last_Index (Container) + 1, then Constraint_Error is propagated. If Count is 0, then Insert_Space does nothing. Otherwise, it computes the new length NL as the sum of the current length and Count; if the value of Last appropriate for length NL would be greater than Index_Type'Last, then Constraint_Error is propagated. {more text here} It would have much better if this was written as: procedure Insert_Space (Container : in out Vector; Before : in Extended_Index; Count : in Count_Type := 1) with Pre => (if Before not in First_Index (Container) .. Last_Index (Container) + 1 or else Container.Length > Index_Type'Last - Count then raise Constraint_Error); The latter is less likely to be misinterpreted, it still can be checked at run-time, the compiler can use it to completely eliminate redundant checks (which cannot be done for checks in the body absent of inlining -- which is usually a bad idea), and static analysis tools (and compilers, for that matter) can detect and complain about cases where the checks are known to fail (that is, where the program has bugs). And you get all of this without peeking into the body of the subprogram. We can't require the latter: it's beyond the state of the art to do that in most cases, but by doing this at runtime now, we get people writing these conditions so that as the state of the art improves more can be done for static detection. There never will be any static detection of conditions written as comments! Also note that in the above, this precondition is NOT part of the body (implementation) of the subprogram. This is required of all implementations -- it's part of the contract, not the part that varies between implementations. As such, it makes the most sense to write it as part of the contract. ... > Neither #1 nor #2 is defendable. Nothing you say on this topic makes any sense, at least from an Ada perspective. Here you are saying that Ada's entire design and reason for existing is "not defendable" (that's the separation of specification from implementation). How your ideal language might work is irrelevevant in this forum. Please talk about Ada, not impossible theory. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 19:41 ` Randy Brukardt @ 2012-06-22 23:08 ` Dmitry A. Kazakov 2012-06-23 10:46 ` Georg Bauhaus 2012-07-03 4:51 ` Randy Brukardt 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-22 23:08 UTC (permalink / raw) On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net... >> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote: >> >>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net... >>> ... >>>> This is what constitutes the core inconsistency about dynamic >>>> pre-/post-conditions. If they #1 implement behavior (e.g the stack >>>> contract >>>> to raise something when full), then they cannot be suppressed and do not >>>> describe the contract. If they do describe the contract #2, they may not >>>> implement it and thus shall have no run-time effect. >>> >>> You're right, but I don't see any inconsistency. They are clearly #1, and >>> that includes all of the existing Ada checks as well. >> >> If you take a stance on #1, then checking stack full is no more evaluation >> of the precondition, which does not depend on the stack state anymore, as >> it of course should be. So the "true" precondition is just: True. > > Huh? This makes no sense whatsoever. > > We can't require static detection of precondition failures any more than we > can demand static detection of range violations. You seem to imply that value in the range is a precondition of the operation constrained to that range. This is wrong. If S is a subtype of T then the precondition is X in T The postcondition is (X in S and <something>) or (X not in S and Constraint_Error propagated) > And Ada *always* has had dynamic preconditions: > > procedure New_Line (Spacing : in Positive_Count := 1); The precondition here is Spacing in Positive_Count'Base because the behavior of New_Line is *defined* when Spacing is not in Positive_Count'Range. New_Line(0) is a *legal* Ada program. >> And implementations leaking into declarations is certainly a very bad >> idea. > > This is NOT implementation; it's part of the contract. OK, you switched from #1 to #2. >> Neither #1 nor #2 is defendable. > > Nothing you say on this topic makes any sense, at least from an Ada > perspective. Here you are saying that Ada's entire design and reason for > existing is "not defendable" Why entire? Dynamic correctness checks are not defendable, as demonstrated on numerous examples. > (that's the separation of specification from implementation). On the contrary, it is #1 which breaks that separation. #2 it is just flat wrong. > How your ideal language might work is irrelevevant in this forum. It is not mine language. It is a methodology of defining and proving program correctness as introduced by Dijkstra. It applies to all languages without exemption. > Please talk about Ada, not impossible theory. The only impossible theory here is about meaning of dynamically checked preconditions, e.g. #1 or #2? That is indeed impossible, because inconsistent. Otherwise Dijkstra's approach works pretty well with any language, e.g. SPARK does for Ada. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 23:08 ` Dmitry A. Kazakov @ 2012-06-23 10:46 ` Georg Bauhaus 2012-06-23 11:01 ` Dmitry A. Kazakov 2012-07-03 4:51 ` Randy Brukardt 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-23 10:46 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-23 10:46 ` Georg Bauhaus @ 2012-06-23 11:01 ` Dmitry A. Kazakov 2012-06-23 17:46 ` AdaMagica 2012-06-24 14:59 ` Georg Bauhaus 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-23 11:01 UTC (permalink / raw) On Sat, 23 Jun 2012 12:46:56 +0200, Georg Bauhaus wrote: > On 23.06.12 01:08, Dmitry A. Kazakov wrote: >>> And Ada*always* has had dynamic preconditions: >>> > >>> > procedure New_Line (Spacing : in Positive_Count := 1); >> The precondition here is Spacing in Positive_Count'Base because the >> behavior of New_Line is*defined* when Spacing is not in >> Positive_Count'Range. >> >> New_Line(0) >> >> is a*legal* Ada program. > > The behavior of New_Line is not relevant, It is OK if New_Line(0) would reboot the computer? New_Line(0) is not straight legal, it not an error in the classification of errors (RM 1.1.5). Compare: a contract violation is an *unbounded ERROR*. Aside. If you could estimate the effect of a contract violation, in order to make the case for a bounded error, that would not save the idea of checking either. Because, of course, in that case you also could detect the violation itself, which is a much simpler task than tracking all possible consequences down. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-23 11:01 ` Dmitry A. Kazakov @ 2012-06-23 17:46 ` AdaMagica 2012-06-23 19:23 ` Dmitry A. Kazakov 2012-06-24 14:59 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: AdaMagica @ 2012-06-23 17:46 UTC (permalink / raw) Cc: mailbox On Saturday, June 23, 2012 1:01:17 PM UTC+2, Dmitry A. Kazakov wrote: > It is OK if New_Line(0) would reboot the computer? Really, I do not understand your argument. If the argument of New_Line is 0, the procedure is not even called, so its body is irrelevant. The evaluation of the argument raises Constraint_Error as defined in the RM. How could it reboot the computer? The consequences of CE are well-defined. So what? I think I'm not the only one who is often lost in following your arguments. > New_Line(0) is not straight legal, it not an error in the classification of > errors (RM 1.1.5). What? You surely have read 1.1.5(5)? > > Compare: a contract violation is an *unbounded ERROR*. > > Aside. If you could estimate the effect of a contract violation, in order > to make the case for a bounded error, that would not save the idea of > checking either. Because, of course, in that case you also could detect the > violation itself, which is a much simpler task than tracking all possible > consequences down. > > -- > Regards, > Dmitry A. Kazakov > http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-23 17:46 ` AdaMagica @ 2012-06-23 19:23 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-23 19:23 UTC (permalink / raw) On Sat, 23 Jun 2012 10:46:35 -0700 (PDT), AdaMagica wrote: > On Saturday, June 23, 2012 1:01:17 PM UTC+2, Dmitry A. Kazakov wrote: >> It is OK if New_Line(0) would reboot the computer? > > Really, I do not understand your argument. It was Georg's argument. I only asked a simple question. Is the behavior of New_Line defined for the case when the argument is 0, or not? Possible answer is either "yes" or "no." > If the argument of New_Line is 0, the procedure is not even called, so its > body is irrelevant. If New_Line is not called, why this construct is named "procedure call"? Let New_Line(1) were inlined would you also argue that its body is not called? Would be an implementation checking the constraint within the body illegal? How do you know if the given piece of code raising an exception does or does not belong to the body? How all this could be relevant to the semantics of New_Line and its contract describing this semantics? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-23 11:01 ` Dmitry A. Kazakov 2012-06-23 17:46 ` AdaMagica @ 2012-06-24 14:59 ` Georg Bauhaus 2012-06-24 16:06 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-24 14:59 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-24 14:59 ` Georg Bauhaus @ 2012-06-24 16:06 ` Dmitry A. Kazakov 2012-06-24 19:51 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-24 16:06 UTC (permalink / raw) On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote: > On 23.06.12 13:01, Dmitry A. Kazakov wrote: >> Compare: a contract violation is an *unbounded ERROR*. > > Do you mean, I should imagine a contract violation that, > when checks are turned off, result in erroneous execution? The effect of contract violation is unbounded because not contracted. When you say that something behaves in a certain way under specified conditions, e.g. raises exception when out of range, that is the contract. 1. violation => nothing guaranteed 2. effect is bounded => these bounds are in the contract 1+2 = contract violation is necessarily *equivalent* to undefined behavior. What is so difficult about this? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-24 16:06 ` Dmitry A. Kazakov @ 2012-06-24 19:51 ` Georg Bauhaus 2012-06-25 7:48 ` Dmitry A. Kazakov 2012-06-25 8:08 ` Dmitry A. Kazakov 0 siblings, 2 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-24 19:51 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-24 19:51 ` Georg Bauhaus @ 2012-06-25 7:48 ` Dmitry A. Kazakov 2012-06-25 10:10 ` Georg Bauhaus 2012-06-25 8:08 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 7:48 UTC (permalink / raw) On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote: > On 24.06.12 18:06, Dmitry A. Kazakov wrote: >> On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote: >> >>> On 23.06.12 13:01, Dmitry A. Kazakov wrote: >>>> Compare: a contract violation is an *unbounded ERROR*. >>> >>> Do you mean, I should imagine a contract violation that, >>> when checks are turned off, result in erroneous execution? >> >> The effect of contract violation is unbounded because not contracted. > > The effect of a contract violation is part of the contract between > client and supplier, Like the actual effect of violation of the expected effect of violation of the contract. Credo quia absurdum -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 7:48 ` Dmitry A. Kazakov @ 2012-06-25 10:10 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-25 10:10 UTC (permalink / raw) On 25.06.12 09:48, Dmitry A. Kazakov wrote: > On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote: > >> On 24.06.12 18:06, Dmitry A. Kazakov wrote: >>> On Sun, 24 Jun 2012 16:59:55 +0200, Georg Bauhaus wrote: >>> >>>> On 23.06.12 13:01, Dmitry A. Kazakov wrote: >>>>> Compare: a contract violation is an *unbounded ERROR*. >>>> >>>> Do you mean, I should imagine a contract violation that, >>>> when checks are turned off, result in erroneous execution? >>> >>> The effect of contract violation is unbounded because not contracted. >> >> The effect of a contract violation is part of the contract between >> client and supplier, > > Like the actual effect of violation of the expected effect of violation of > the contract. > > Credo quia absurdum That's what true exceptions always are. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-24 19:51 ` Georg Bauhaus 2012-06-25 7:48 ` Dmitry A. Kazakov @ 2012-06-25 8:08 ` Dmitry A. Kazakov 2012-06-25 10:17 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 8:08 UTC (permalink / raw) On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote: > It is a theory in a different universe of notions. http://en.wikipedia.org/wiki/Paradox_of_the_Court As Littlewood once said, self-referential jokes are fun. Further reading on the subject of your universe: http://www.cut-the-knot.org/selfreference/index.shtml -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 8:08 ` Dmitry A. Kazakov @ 2012-06-25 10:17 ` Georg Bauhaus 2012-06-25 11:54 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-25 10:17 UTC (permalink / raw) On 25.06.12 10:08, Dmitry A. Kazakov wrote: > On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote: > >> It is a theory in a different universe of notions. > > http://en.wikipedia.org/wiki/Paradox_of_the_Court Indeed, it helps to remember that logicians and mathematicians have learned that logic and mathematics cannot justify themselves. We have to do something. DbC is something. Better than nothing. So logic and mathematics become tools that happen to exist, tools in the hands of designers whose goals transcend both mathematics and logics into the realm of the physical world of computer based systems. DbC is a best effort thing like every system building effort. > As Littlewood once said, self-referential jokes are fun. Further reading on > the subject of your universe: > > http://www.cut-the-knot.org/selfreference/index.shtml ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 10:17 ` Georg Bauhaus @ 2012-06-25 11:54 ` Dmitry A. Kazakov 2012-06-25 12:39 ` Georg Bauhaus 2012-06-25 14:08 ` stefan-lucks 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 11:54 UTC (permalink / raw) On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote: > On 25.06.12 10:08, Dmitry A. Kazakov wrote: >> On Sun, 24 Jun 2012 21:51:08 +0200, Georg Bauhaus wrote: >> >>> It is a theory in a different universe of notions. >> >> http://en.wikipedia.org/wiki/Paradox_of_the_Court > > Indeed, it helps to remember that logicians and mathematicians > have learned that logic and mathematics cannot justify themselves. No, they never ever did that. From very beginning mathematicians used axiomatic approach instead. What they did, was constructing frameworks within which one could not deduce both A and not A. > We have to do something. DbC is something. Better than nothing. Is SPARK nothing? Is strong typing nothing? But you seemingly did not read what I wrote earlier. There is either #1 or #2. #2 is inconsistent and thus is out. Left is #1: so-called Ada 2012 preconditions simply are misplaced implementations. This is flawed and misleading, but not because of some cosmogonic problems like your Promethean trampling laws of logic. Just a much more humble ignoring principles of good language design. Nothing really new. > DbC is a best effort thing like every system building effort. How are you going to prove this, if "DbC" contradicts logic itself? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 11:54 ` Dmitry A. Kazakov @ 2012-06-25 12:39 ` Georg Bauhaus 2012-06-25 12:51 ` Georg Bauhaus 2012-06-25 13:19 ` Dmitry A. Kazakov 2012-06-25 14:08 ` stefan-lucks 1 sibling, 2 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-25 12:39 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 12:39 ` Georg Bauhaus @ 2012-06-25 12:51 ` Georg Bauhaus 2012-06-25 13:19 ` Dmitry A. Kazakov 1 sibling, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-25 12:51 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 12:39 ` Georg Bauhaus 2012-06-25 12:51 ` Georg Bauhaus @ 2012-06-25 13:19 ` Dmitry A. Kazakov 2012-06-25 16:43 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 13:19 UTC (permalink / raw) On Mon, 25 Jun 2012 14:39:06 +0200, Georg Bauhaus wrote: > On 25.06.12 13:54, Dmitry A. Kazakov wrote: > >>> Indeed, it helps to remember that logicians and mathematicians >>> have learned that logic and mathematics cannot justify themselves. >> >> No, they never ever did that. > > They tried, though. I didn't even say that they did. > > Frege thought, for some time, that he had done. > Russel sent a correction. Hilbert did not give up, though: Not at all. All three used axiomatic approach. None of them would ever seek to justify logic by means of logic. >>> We have to do something. DbC is something. Better than nothing. >> >> Is SPARK nothing? > > Try > > new Data'(Size => More_than_4k); How does this make SPARK null and void? >> Is strong typing nothing? > > Until Ada 2012, there was nothing in addition to the strong type > system of Ada 2005. And the point is? Some hidden Ada version between 2005 and 2012? >> But you seemingly did not read what I wrote earlier. There is either #1 or >> #2. > > I have tried to explain that neither #1 nor #2 are applicable > because they assume applicability of exhaustive formal analysis > to general program design (not programs). So #2 does not apply, I missed where you agreed with me on that. Ergo, Ada 2012 preconditions are not contract (not #2). Please confirm this, and we will proceed to #1 and whether (not #2 is equivalent to #1). >>> DbC is a best effort thing like every system building effort. >> >> How are you going to prove this, if "DbC" contradicts logic itself? > > A program that is known to be covered entirely by logic > is really an exception. Please, show this without logic. > Proving things in a DbC framework is similar to proving things > with the help of more than Ada, as is done when using SPARK. No. You claimed that what you call DbC does not obey laws of logic. I am eager to learn how are you going to "prove things" without these laws. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 13:19 ` Dmitry A. Kazakov @ 2012-06-25 16:43 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-25 16:43 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 11:54 ` Dmitry A. Kazakov 2012-06-25 12:39 ` Georg Bauhaus @ 2012-06-25 14:08 ` stefan-lucks 2012-06-25 14:36 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: stefan-lucks @ 2012-06-25 14:08 UTC (permalink / raw) 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! ------ ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 14:08 ` stefan-lucks @ 2012-06-25 14:36 ` Dmitry A. Kazakov 2012-06-25 14:37 ` Dmitry A. Kazakov 2012-06-25 16:26 ` stefan-lucks 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 14:36 UTC (permalink / raw) On Mon, 25 Jun 2012 16:08:01 +0200, stefan-lucks@see-the.signature wrote: > I am not sure if I can cool down this heated discussion, but I'll give it > a try. > > On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > >> On Mon, 25 Jun 2012 12:17:14 +0200, Georg Bauhaus wrote: >> >>> Indeed, it helps to remember that logicians and mathematicians >>> have learned that logic and mathematics cannot justify themselves. >> >> No, they never ever did that. From very beginning mathematicians used >> axiomatic approach instead. What they did, was constructing frameworks >> within which one could not deduce both A and not A. > > A bit off topic -- but this is not quite true. > > Firstly, the axiomatic approach has become mathematical mainstream only > since about the times of David Hilbert. The "very beginning" of > Mathematics and Logic are quite a bit earlier. ;-) Euclid > Secondly, Hilbert's program was to construct frameworks being both > complete (all correct conclusions should be deducible) and one should not > be able to deduce both A and not A. Kurt Goedel eventually showed that > this is *logically* impossible. Hilbert's program by no means was intended to justify logic or mathematics themselves. This is outright wrong. >> Is SPARK nothing? Is strong typing nothing? >> >> But you seemingly did not read what I wrote earlier. There is either #1 or >> #2. > > This the axiom that *you* choose to start with. Starting from there, your > reasoning may be logically correct. If Ada precondition is neither implementation (#1) nor specification/contract (#2) then what is it? Since nobody ever came with #3, I considered only #1 and #2. > *Firstly*, you don't seem to separate between syntax and semantic. I said nothing about the syntax. It could be better, but syntax is always the most difficult part. > *Secondly*, you seem to overlook that there are three semantical options, > rather than the two you mention: > > 1 ignore the conditions > > 2 check them dynamically at run time > > 3 prove them statically at compile time I didn't: Assuming #1, only no.2 is possible. #1 <=> no.2 Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or no.2. One *cannot* mix no.1/3 with no.2, that is what upsets me. > Even SPARK may soon support the Ada 2012 syntax for its annotations. That is OK to me, however, considering syntax I wished a clearer separation of pre-/post-conditions from other declarations. But since GPS rules, I suppose it would not be much difficult to have a view cutting pre-/post-conditions off and displaying them in a side-by-side window scrolled upon mouse hovering etc. > *Thirdly*, you seem to assume that a tool that can be used in a > destructive way cannot also be used properly. In this particular case (#2 + no.3) we wave a very strong evidence: accessibility checks. It was a disaster. > The support for the second option is such a tool. I agree with you, any > program that claims some preconditions, postconditions and invariants > should stop and must be fixed when any such check fails. Silently handling > the exception and then continuing is > > - a logical contradiction in itself, and also > > - the result from some lousy programming practice. > > There is no justification for handling the exception instead of fixing the > flaw! > > But the same tool can properly be used for debugging and testing -- if any > assertion fails, and you detect this at run time, write all relevant > details into a log file, stop the program, and fix the bug. No objection whatsoever. I covered this case earlier. It is OK to check dynamically under the condition that the checker is an *independent* program. A debugger, checker, reasonably protected Ada run-time verifying preconditions and *handling* failed checks is perfectly consistent and advisable. That clearly precludes no.2: handling is within the checker, checker is outside the testee. And, very importantly, we want to contract exceptions some day, don't we? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 14:36 ` Dmitry A. Kazakov @ 2012-06-25 14:37 ` Dmitry A. Kazakov 2012-06-25 16:26 ` stefan-lucks 1 sibling, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 14:37 UTC (permalink / raw) On Mon, 25 Jun 2012 16:36:09 +0200, Dmitry A. Kazakov wrote: > Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or > no.2. typo error: no.1 or 3 -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 14:36 ` Dmitry A. Kazakov 2012-06-25 14:37 ` Dmitry A. Kazakov @ 2012-06-25 16:26 ` stefan-lucks 2012-06-25 19:42 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: stefan-lucks @ 2012-06-25 16:26 UTC (permalink / raw) On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > Hilbert's program by no means was intended to justify logic or mathematics > themselves. This is outright wrong. Hilbert's program was an attempt to re-build the very foundations of Mathematics. No more, no less. See <http://en.wikipedia.org/wiki/Hilbert%27s_program>. > If Ada precondition is neither implementation (#1) nor > specification/contract (#2) then what is it? A syntax for specifications. > I said nothing about the syntax. It could be better, but syntax is always > the most difficult part. OK. > > *Secondly*, you seem to overlook that there are three semantical options, > > rather than the two you mention: > > > > 1 ignore the conditions > > > > 2 check them dynamically at run time > > > > 3 prove them statically at compile time > > I didn't: > > Assuming #1, only no.2 is possible. #1 <=> no.2 > > Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or > no.2. > > One *cannot* mix no.1/3 with no.2, that is what upsets me. But you are not locked into either option 1, 2, or 3, you can choose, without having to change the language, or to rewrite a single character of your program source. > > Even SPARK may soon support the Ada 2012 syntax for its annotations. > > That is OK to me, however, considering syntax I wished a clearer separation > of pre-/post-conditions from other declarations. But since GPS rules, I > suppose it would not be much difficult to have a view cutting > pre-/post-conditions off and displaying them in a side-by-side window > scrolled upon mouse hovering etc. That is a matter of taste. In any case, emacs rules. ;-) > > *Thirdly*, you seem to assume that a tool that can be used in a > > destructive way cannot also be used properly. > > In this particular case (#2 + no.3) we wave a very strong evidence: > accessibility checks. It was a disaster. I agree that dynamic accessibility checks have failed to become a good tool for reliable program development. But the standard requires no compiler switch to allow them turning on and off on demand -- in contrast to assertions and Ada 2012 conditions.I.e., the accessibility checks are really part of the language, the checks are a tool that you have the freedom to use or not to use! > No objection whatsoever. I covered this case earlier. It is OK to check > dynamically under the condition that the checker is an *independent* > program. A debugger, checker, reasonably protected Ada run-time verifying > preconditions and *handling* failed checks is perfectly consistent and > advisable. Agreed. > That clearly precludes no.2: handling is within the checker, checker is > outside the testee. Well, this separation is ideal. But most of the time, a testee that discovers itself being in a faulty state (and that is, what a failed dynamic check actually reveals), the testee is still able to write some information to a log file. Sure, you can construct or find the odd counterexample -- but in practice almost all the time this approach works. (OK, I am assuming your system allows to write some log output at all.) > And, very importantly, we want to contract exceptions some day, don't we? Sure! So what? Ada.Assertions.Assertion_Error is one exception like Constraint_Error or the like. Either, you prove that this or that exception will not be raised. Or you claim that such an exception is not raised. If it is actually raised this is a violation of the contract. Which is a big deal for, say, Constraint_Error, but not for Ada.Assertions.Assertion_Error ... the exception that indicates the violation of a contract, anyway. (Assuming that Ada.Assertions.Assertion_Error is not raised manually -- but no sane programmer would do that.) Actually, there is one exception that is difficult to specify. It is our old fellow Storage_Error. On the level of source code analysis, you actually cannot prove that this exception will not be raised. -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html> ------ I love the taste of Cryptanalysis in the morning! ------ ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 16:26 ` stefan-lucks @ 2012-06-25 19:42 ` Dmitry A. Kazakov 2012-06-26 11:50 ` stefan-lucks 2012-07-03 5:10 ` Randy Brukardt 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-25 19:42 UTC (permalink / raw) On Mon, 25 Jun 2012 18:26:18 +0200, stefan-lucks@see-the.signature wrote: > On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > >> Hilbert's program by no means was intended to justify logic or mathematics >> themselves. This is outright wrong. > > Hilbert's program was an attempt to re-build the very foundations of > Mathematics. No more, no less. See > <http://en.wikipedia.org/wiki/Hilbert%27s_program>. Right, and this had nothing to do with justification either logic or mathematics by means of themselves. Such an epic task would rather be a job for baron Muenchausen. Just scroll through the Hilbert's program list of problems: http://en.wikipedia.org/wiki/Hilbert_problems >> If Ada precondition is neither implementation (#1) nor >> specification/contract (#2) then what is it? > > A syntax for specifications. Syntax only? >>> *Secondly*, you seem to overlook that there are three semantical options, >>> rather than the two you mention: >>> >>> 1 ignore the conditions >>> >>> 2 check them dynamically at run time >>> >>> 3 prove them statically at compile time >> >> I didn't: >> >> Assuming #1, only no.2 is possible. #1 <=> no.2 >> >> Assuming #2, you have only choice between no.1 and no.3. #2 <=> no.1 or >> no.2. >> >> One *cannot* mix no.1/3 with no.2, that is what upsets me. > > But you are not locked into either option 1, 2, or 3, you can choose, > without having to change the language, or to rewrite a single character > of your program source. Same syntax for things which are far more apart than just semantically different. What a bizzare idea! You would be switching between contract specification and implementation per compiler switch! Is this C preprocessor or Ada? >> That clearly precludes no.2: handling is within the checker, checker is >> outside the testee. > > Well, this separation is ideal. But most of the time, a testee that > discovers itself being in a faulty state (and that is, what a failed > dynamic check actually reveals), the testee is still able to write some > information to a log file. Sure, you can construct or find the odd > counterexample -- but in practice almost all the time this approach works. > (OK, I am assuming your system allows to write some log output at all.) Tracing is OK, but what happens afterwards? If continuation is possible, that requires some cleanup, rollback, retry etc, which has the goal of putting the system into some definite state. This is not over before over. >> And, very importantly, we want to contract exceptions some day, don't we? > > Sure! So what? How are going to marry exceptions propagating from contracts with contracts on exceptions? Some exceptions are more exceptional than others? Aren't we fed up with Program_Error? > Ada.Assertions.Assertion_Error is one exception like Constraint_Error or > the like. Either, you prove that this or that exception will not be > raised. Or you claim that such an exception is not raised. If it is > actually raised this is a violation of the contract. Which is a big deal > for, say, Constraint_Error, but not for Ada.Assertions.Assertion_Error ... > the exception that indicates the violation of a contract, anyway. (Assuming > that Ada.Assertions.Assertion_Error is not raised manually -- but no sane > programmer would do that.) > > Actually, there is one exception that is difficult to specify. It is our > old fellow > > Storage_Error. > > On the level of source code analysis, you > actually cannot prove that this exception will not be raised. Firstly, you if you don't want to prove anything about a certain exception, you would add this exception to all contracts involved and take care about exceptions of interest. Secondly, you would rather prove conditionals, like: Storage_Error is not propagated when given amount of memory is available in the specified pools. This is good enough for most cases, which are not about any exact bound, but about existence of such bound, i.e. about memory leak detection. Thirdly, you would be able to provide axioms. E.g. for some complex recursive operation, you could just specify the upper memory consumption bound known to you from other sources, and let the prover to go with that (the oracle). I think conservative Storage_Errror proof is pretty doable. If you move the upper bound a pair Kbytes upward it would eliminate most of problems. We certainly could learn from Java mistakes rather than repeating them (e.g. interfaces). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 19:42 ` Dmitry A. Kazakov @ 2012-06-26 11:50 ` stefan-lucks 2012-06-26 13:07 ` Dmitry A. Kazakov 2012-07-03 5:10 ` Randy Brukardt 1 sibling, 1 reply; 125+ messages in thread From: stefan-lucks @ 2012-06-26 11:50 UTC (permalink / raw) On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > > Hilbert's program was an attempt to re-build the very foundations of > > Mathematics. No more, no less. See > > <http://en.wikipedia.org/wiki/Hilbert%27s_program>. > > Right, and this had nothing to do with justification either logic or > mathematics by means of themselves. Hilbert was very explicit that he wanted to formalize *all* of mathematics axiomatically, and prove the whole formalization consistent. There is an interesting article <http://plato.stanford.edu/entries/hilbert-program/>. > Such an epic task would rather be a job for baron Muenchausen. Here we are in violent agreement. ;-) The program was quite successful in making mathematicans re-think the foundations of their field. BUT it turned out that the required formalization of *all* of mathematics could not work, for the same reason Muenchhausen's famous trick would not work. So Hilbert's program was an epic failure! In any case, this is quite off topic, and we need not discuss Hilbert's program in c.l.a. > Same syntax for things which are far more apart than just semantically > different. What a bizzare idea! You would be switching between contract > specification and implementation per compiler switch! Is this C > preprocessor or Ada? There is a well-defined syntax for contracts, and you can choose between different ways to use them. But contracts are still contracts. No relationship to the C preprocessor. > >> That clearly precludes no.2: handling is within the checker, checker is > >> outside the testee. > > > > Well, this separation is ideal. But most of the time, a testee that > > discovers itself being in a faulty state (and that is, what a failed > > dynamic check actually reveals), the testee is still able to write some > > information to a log file. Sure, you can construct or find the odd > > counterexample -- but in practice almost all the time this approach works. > > (OK, I am assuming your system allows to write some log output at all.) > > Tracing is OK, but what happens afterwards? If continuation is possible, > that requires some cleanup, rollback, retry etc, which has the goal of > putting the system into some definite state. This is not over before over. Don't do that! Emit your messages to to the log file and then terminate! Or try to continue -- but you should never forget that any failed condition indicates a bug that must be fixed soon! This feature may be misused by handling an Assertion_Error and then not fixing the bug. And this feature will be misused by some program authors. But then, what is more important: - Provide tools that support good software engineering practice? or - Prohibit any tools that can be misused? Dynamically checked contracts are such a tool. > How are going to marry exceptions propagating from contracts with contracts > on exceptions? The contract must always state "Assertion error is not raised!" Anything else violates some contract, anyway. (But note that if contracts are not proven, they can be lies.) > Some exceptions are more exceptional than others? Aren't we > fed up with Program_Error? What are your issues with Program_Error? I don't have any. > > Actually, there is one exception that is difficult to specify. It is our > > old fellow > > > > Storage_Error. > > > > On the level of source code analysis, you > > actually cannot prove that this exception will not be raised. > > Firstly, you if you don't want to prove anything about a certain exception, > you would add this exception to all contracts involved and take care about > exceptions of interest. So you just add "can raise Storage_Error" to any contract? (Maybe implicitly.) > Secondly, you would rather prove conditionals, like: Storage_Error is not > propagated when given amount of memory is available in the specified pools. > This is good enough for most cases, which are not about any exact bound, > but about existence of such bound, i.e. about memory leak detection. You are so violately against dynamically checked conditions ... and then you propose some heuristic that you just claim to be "good enough for most cases"? > Thirdly, you would be able to provide axioms. E.g. for some complex > recursive operation, you could just specify the upper memory consumption > bound known to you from other sources, and let the prover to go with that > (the oracle). > > I think conservative Storage_Error proof is pretty doable. If you move the > upper bound a pair Kbytes upward it would eliminate most of problems. Good luck with any recursive program. And (I am sure you know this) any approach to really prove upper bounds on the storage requirements would imply to solve the Halting Problem. > We certainly could learn from Java mistakes rather than repeating them > (e.g. interfaces). Which is probably why Ada so far has no contracted exceptions. Not that they cannot be done -- but nobody knows how to write such contracts that they really become useful. -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html> ------ I love the taste of Cryptanalysis in the morning! ------ ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 11:50 ` stefan-lucks @ 2012-06-26 13:07 ` Dmitry A. Kazakov 2012-06-26 13:49 ` Georg Bauhaus ` (2 more replies) 0 siblings, 3 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-26 13:07 UTC (permalink / raw) On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote: > On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > >> Same syntax for things which are far more apart than just semantically >> different. What a bizzare idea! You would be switching between contract >> specification and implementation per compiler switch! Is this C >> preprocessor or Ada? > > There is a well-defined syntax for contracts, and you can choose between > different ways to use them. But contracts are still contracts. No > relationship to the C preprocessor. They are contracts when checked statically and implementations when checked dynamically. It is like #define is := >>>> That clearly precludes no.2: handling is within the checker, checker is >>>> outside the testee. >>> >>> Well, this separation is ideal. But most of the time, a testee that >>> discovers itself being in a faulty state (and that is, what a failed >>> dynamic check actually reveals), the testee is still able to write some >>> information to a log file. Sure, you can construct or find the odd >>> counterexample -- but in practice almost all the time this approach works. >>> (OK, I am assuming your system allows to write some log output at all.) >> >> Tracing is OK, but what happens afterwards? If continuation is possible, >> that requires some cleanup, rollback, retry etc, which has the goal of >> putting the system into some definite state. This is not over before over. > > Don't do that! Emit your messages to to the log file and then terminate! Contract violation => terminate. Exceptional state => recover. > But then, what is more important: > > - Provide tools that support good software engineering practice? > > or > > - Prohibit any tools that can be misused? > > Dynamically checked contracts are such a tool. A wrench sold as shoe polish. >>> Actually, there is one exception that is difficult to specify. It is our >>> old fellow >>> >>> Storage_Error. >>> >>> On the level of source code analysis, you >>> actually cannot prove that this exception will not be raised. >> >> Firstly, you if you don't want to prove anything about a certain exception, >> you would add this exception to all contracts involved and take care about >> exceptions of interest. > > So you just add "can raise Storage_Error" to any contract? (Maybe > implicitly.) Contracts will be inheritable. I don't know how it goes with aspects, never understood what they are good for, but true contracts are inherited while possibly weakening pre- and strengthening post-conditions (LSP). Another necessary contract mechanism is composition. That is when you pass a downward closure to an operation, that could say: I raise what the argument does. Note that this will require proper procedural types to have interfaces to carry the contract with. E.g. you would be able to limit the closure operation to what it is allowed to raise. >> Secondly, you would rather prove conditionals, like: Storage_Error is not >> propagated when given amount of memory is available in the specified pools. >> This is good enough for most cases, which are not about any exact bound, >> but about existence of such bound, i.e. about memory leak detection. > > You are so violately against dynamically checked conditions ... and then > you propose some heuristic that you just claim to be "good enough for most > cases"? Why does this surprise you? No contract can describe all semantics. It only vaguely describes it. You may have all sorts of possible contracts with the same implementation and conversely. It is free choice how much of the semantics a contract to mandate: from few in a trow away program to much for a mission critical one. >> Thirdly, you would be able to provide axioms. E.g. for some complex >> recursive operation, you could just specify the upper memory consumption >> bound known to you from other sources, and let the prover to go with that >> (the oracle). >> >> I think conservative Storage_Error proof is pretty doable. If you move the >> upper bound a pair Kbytes upward it would eliminate most of problems. > > Good luck with any recursive program. > > And (I am sure you know this) any approach to really prove upper bounds > on the storage requirements would imply to solve the Halting Problem. No problem. If you cannot prove it, that is compile error. It is a conservative estimation, estimations have no halting problem issue, Boolean values are bounded. The real problem lies elsewhere. Prover to tell program legality is thin ice. Depending on the technique used the same program could be legal (good prover) or illegal (poor prover). I don't know how to address this, though nobody cares anyway... >> We certainly could learn from Java mistakes rather than repeating them >> (e.g. interfaces). > > Which is probably why Ada so far has no contracted exceptions. Not that > they cannot be done -- but nobody knows how to write such contracts that > they really become useful. Huh, they didn't much hesitate to borrow flawed Java interfaces, although the language already had abstract types. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 13:07 ` Dmitry A. Kazakov @ 2012-06-26 13:49 ` Georg Bauhaus 2012-06-26 14:45 ` Dmitry A. Kazakov 2012-06-26 14:54 ` stefan-lucks 2012-07-03 5:28 ` Randy Brukardt 2 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-26 13:49 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 13:49 ` Georg Bauhaus @ 2012-06-26 14:45 ` Dmitry A. Kazakov 2012-06-26 16:48 ` Georg Bauhaus 2012-06-29 21:03 ` Shark8 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-26 14:45 UTC (permalink / raw) On Tue, 26 Jun 2012 15:49:24 +0200, Georg Bauhaus wrote: > On 26.06.12 15:07, Dmitry A. Kazakov wrote: > >> They are contracts when checked statically and implementations when checked >> dynamically. > > What do pre/post implement, if so, in your view? if Pre(...) then <body> if Post(...) then null; else raise Constraint_Error; end if; else raise Constraint_Error; end if; >> Contract violation => terminate. Exceptional state => recover. > > How does a client do make the program recover if an exception > stands for "unforeseen"? How does a client recover if X contains 3 rather than 1? Answer: it recovers by continuing its program further. > Or is an exception just a special value of a type, a value > with an "exception" label that is nothing special, but allows > an elaborate goto? Yes, exception an "ideal" value. It is used to fix contracts, when otherwise no outcome existed. E.g. Constraint_Error is the value of x/0. With Constraint_Error "+", "-", "*", "/" become defined for all possible values of the arguments. Compare to IEEE NaN, +Inf, -Inf. With exceptions you can continue execution when you otherwise could not, because exceptions add new computational states for which no value otherwise existed. Continuation goes to these states, which are called exceptional. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 14:45 ` Dmitry A. Kazakov @ 2012-06-26 16:48 ` Georg Bauhaus 2012-06-26 19:43 ` Dmitry A. Kazakov 2012-06-29 21:03 ` Shark8 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-26 16:48 UTC (permalink / raw) 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). ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 16:48 ` Georg Bauhaus @ 2012-06-26 19:43 ` Dmitry A. Kazakov 2012-06-27 8:23 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-26 19:43 UTC (permalink / raw) On Tue, 26 Jun 2012 18:48:05 +0200, Georg Bauhaus wrote: > On 26.06.12 16:45, Dmitry A. Kazakov wrote: >> On Tue, 26 Jun 2012 15:49:24 +0200, Georg Bauhaus wrote: >> >>> On 26.06.12 15:07, Dmitry A. Kazakov wrote: >>> >>>> They are contracts when checked statically and implementations when checked >>>> dynamically. >>> >>> What do pre/post implement, if so, in your view? >> >> if Pre(...) then >> <body> >> if Post(...) then >> null; >> else >> raise Constraint_Error; >> end if; >> else >> raise Constraint_Error; >> end if; > > There is a different understanding of "implement". Pre/Post > do not implement anything essential. They implement raising exceptions. > <body> is supposed to > implement something that essentially agrees with Pre/Post. Sure. Anything that follows "then" in any if-statement implements something in agreement with the condition tested by the statement. That is the nature of if-statements. >>>> Contract violation => terminate. Exceptional state => recover. >>> >>> How does a client do make the program recover if an exception >>> stands for "unforeseen"? >> >> How does a client recover if X contains 3 rather than 1? >> >> Answer: it recovers by continuing its program further. > > In a truly exceptional situation, as opposed to when there is > a catch-all "special value", there is no contract that could have > been violated, because the contract does not in any way cover the > situation There is no known good value contained in X, for example, > because there is no (practically) meaningful state. If program continues, it does to some state. > For this truly exceptional situation, which is necessarily > unforeseen (otherwise it could have been covered by the contract), An unforeseen situation cannot be tested for. You cannot evaluate a predicate P you don't know. Even a test for "others" is foreseen. Others is merely: Others = not (P1 or P2 or ... or Pn) "Go there, do not know where. Bring that, do not know what" -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 19:43 ` Dmitry A. Kazakov @ 2012-06-27 8:23 ` Georg Bauhaus 2012-06-27 8:52 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-27 8:23 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-27 8:23 ` Georg Bauhaus @ 2012-06-27 8:52 ` Dmitry A. Kazakov 2012-06-27 10:30 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-27 8:52 UTC (permalink / raw) On Wed, 27 Jun 2012 10:23:47 +0200, Georg Bauhaus wrote: > On 26.06.12 21:43, Dmitry A. Kazakov wrote: > >>> <body> is supposed to >>> implement something that essentially agrees with Pre/Post. >> >> Sure. Anything that follows "then" in any if-statement implements something >> in agreement with the condition tested by the statement. That is the nature >> of if-statements. > > That's not what agreement of <body> with Pre/Post should mean, If that is not, change the code. Bugs not to be tolerated. > actually. > In a DbC-correct program, the following two bodies shall have essentially > the same effect: > > A: begin > if Pre (...) then > Stmts; > else > raise Assertion_Failure; > end; > ... > > B: begin > Stmts; > ... They evidently do not have same effect. Prove that they do! -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-27 8:52 ` Dmitry A. Kazakov @ 2012-06-27 10:30 ` Georg Bauhaus 2012-06-27 12:19 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-06-27 10:30 UTC (permalink / raw) 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". ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-27 10:30 ` Georg Bauhaus @ 2012-06-27 12:19 ` Dmitry A. Kazakov 2012-06-27 13:41 ` Nasser M. Abbasi 2012-06-27 15:08 ` Georg Bauhaus 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-27 12:19 UTC (permalink / raw) On Wed, 27 Jun 2012 12:30:41 +0200, Georg Bauhaus wrote: > On 27.06.12 10:52, Dmitry A. Kazakov wrote: >> On Wed, 27 Jun 2012 10:23:47 +0200, Georg Bauhaus wrote: >> >>> On 26.06.12 21:43, Dmitry A. Kazakov wrote: >>> >>>>> <body> is supposed to >>>>> implement something that essentially agrees with Pre/Post. >>>> >>>> Sure. Anything that follows "then" in any if-statement implements something >>>> in agreement with the condition tested by the statement. That is the nature >>>> of if-statements. >>> >>> That's not what agreement of<body> with Pre/Post should mean, >> >> If that is not, change the code. Bugs not to be tolerated. > > What bug? That the code is in disagreement with your objective. > A: > if Pre (...) then > A (X) := 1; > else > raise Assertion_Failure; > end if; > > B: > A (X) := 1; > > A and B can be shown to both be implementations of the behavior > that some contract stipulates. This is wrong on multiple accounts: 1. It cannot be shown: if Pre (HALT (p)) then ... else ... end if; 2. For any program there exist an infinite set of contracts satisfied by; 3. It is irrelevant to whether both pieces are equivalent. If they are, one can be replaced by another. DO IT, where is the check? If they cannot be swapped, they are not equivalent. (Your previous position was more consistent. The point can only be made by getting rid of logic first.) >> They evidently do not have same effect. Prove that they do! > > A and B have *essentially* the same effect once the program > is correct. I don't know what "essentially same effect" is, but whatever formal definition of essential you took you would have to prove that two programs are equivalent according to the definition. That will require proving that the exception is not propagated or else handled to an "essentially" same result. Good luck with that. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-27 12:19 ` Dmitry A. Kazakov @ 2012-06-27 13:41 ` Nasser M. Abbasi 2012-06-28 7:00 ` Georg Bauhaus 2012-06-27 15:08 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Nasser M. Abbasi @ 2012-06-27 13:41 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-27 13:41 ` Nasser M. Abbasi @ 2012-06-28 7:00 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-28 7:00 UTC (permalink / raw) 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; ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-27 12:19 ` Dmitry A. Kazakov 2012-06-27 13:41 ` Nasser M. Abbasi @ 2012-06-27 15:08 ` Georg Bauhaus 1 sibling, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-27 15:08 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 14:45 ` Dmitry A. Kazakov 2012-06-26 16:48 ` Georg Bauhaus @ 2012-06-29 21:03 ` Shark8 2012-06-30 8:26 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Shark8 @ 2012-06-29 21:03 UTC (permalink / raw) Cc: mailbox > > 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-29 21:03 ` Shark8 @ 2012-06-30 8:26 ` Dmitry A. Kazakov 2012-06-30 12:54 ` Niklas Holsti 2012-07-05 2:58 ` Shark8 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-30 8:26 UTC (permalink / raw) On Fri, 29 Jun 2012 14:03:27 -0700 (PDT), Shark8 wrote: >>> What do pre/post implement, if so, in your view? >> >> if Pre(...) then >> <body> >> if Post(...) then >> null; >> else >> raise Constraint_Error; >> end if; >> else >> raise Constraint_Error; >> end if; > > Ok, but this is just what preconditions [and post] are supposed to do. [That is POV #1] No they are not. True pre-/post-conditions are not supposed to implement anything. Formally speaking, pre-/post-conditions are statements of another language L. The language Ada is what you use to program some P. P operates bits and bytes. The language L is used to operate P itself. In L you can say Correct (P) or Incorrect (P). > After all, we had a way to specify some preconditions before (in Ada 2005): > Type Some_Type is ...; > Type Access_Some is Access Some_Type; > Subtype NN_Access_Some is Not Null Access_Some; It is important to understand that constraint is not a precondition. > How does pulling that out into the Pre clause in Ada 2012 change things? Ignoring the fact that the name is misguiding, it is bad because ad-hoc. It hugely extends the number of places where anonymous subtypes may appear. Effectively a constraint on the argument defines a subtype for the purpose of this only subprogram and this only argument. I am not against extending algebra of subtypes, but it should be done with great care. > I'm really confused on why you seem to think the Pre- and Post-conditions > are bad things. That is because you didn't follow the discussion. Pre- and post-conditions are great things, but only when done correctly. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-30 8:26 ` Dmitry A. Kazakov @ 2012-06-30 12:54 ` Niklas Holsti 2012-07-05 2:58 ` Shark8 1 sibling, 0 replies; 125+ messages in thread From: Niklas Holsti @ 2012-06-30 12:54 UTC (permalink / raw) 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 . @ . ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-30 8:26 ` Dmitry A. Kazakov 2012-06-30 12:54 ` Niklas Holsti @ 2012-07-05 2:58 ` Shark8 2012-07-05 7:24 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Shark8 @ 2012-07-05 2:58 UTC (permalink / raw) Cc: mailbox On Saturday, June 30, 2012 3:26:12 AM UTC-5, Dmitry A. Kazakov wrote: > On Fri, 29 Jun 2012 14:03:27 -0700 (PDT), Shark8 wrote: >> I'm really confused on why you seem to think the Pre- and Post-conditions >> are bad things. > > That is because you didn't follow the discussion. Pre- and post-conditions > are great things, but only when done correctly. Ah, now you're equating 'following' with both 'understanding' and 'remembering the nuances' -- I don't agree with that definition, precisely because it excludes the request for clarification so one might understand it. Also, I don't know where you got the idea that pre- and post-conditions must not implement anything. If that was the case then, strictly speaking JavaDoc's pre and postcondition annotating comments are superior to Ada's pre and post condition because they don't implement anything and are, in fact, just comments having no actual impact on the program text. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 2:58 ` Shark8 @ 2012-07-05 7:24 ` Dmitry A. Kazakov 2012-07-06 6:23 ` Shark8 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-05 7:24 UTC (permalink / raw) On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote: > Also, I don't know where you got the idea that pre- and post-conditions > must not implement anything. Trivial: IF pre-/post-condition is contract THEN they are not implementation [POV #2] (Historically, pre-/post-conditions were invented by Dijkstra for the purpose of proving correctness. Later they were used for types to analyze substitutability issues etc.) ELSE ... [POV #1] > If that was the case then, strictly speaking > JavaDoc's pre and postcondition annotating comments are superior to Ada's > pre and post condition because they don't implement anything and are, in > fact, just comments having no actual impact on the program text. Not if condition proof fault makes the program illegal. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 7:24 ` Dmitry A. Kazakov @ 2012-07-06 6:23 ` Shark8 2012-07-06 7:57 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Shark8 @ 2012-07-06 6:23 UTC (permalink / raw) Cc: mailbox 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 6:23 ` Shark8 @ 2012-07-06 7:57 ` Dmitry A. Kazakov 2012-07-07 1:09 ` Randy Brukardt 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-06 7:57 UTC (permalink / raw) On Thu, 5 Jul 2012 23:23:20 -0700 (PDT), Shark8 wrote: > On Thursday, July 5, 2012 1:24:57 AM UTC-6, Dmitry A. Kazakov wrote: >> On Wed, 4 Jul 2012 19:58:31 -0700 (PDT), Shark8 wrote: >> >>> Also, I don't know where you got the idea that pre- and post-conditions >>> must not implement anything. >> >> Trivial: >> >> IF pre-/post-condition is contract THEN they are not implementation >> [POV #2] >> ELSE ... [POV #1] > > Now you're just restating what you said. No. The propositions are different: P1: The contract may implement [some behavior] P2: Pre-/post-conditions may implement [some behavior] The statement I made was: Pre-/post-condition is contract AND not P1 => not P2 Nobody, so far, take an assault on not P1. Would you? > If you mean something like "I > take that to be axiomaatic" or "by definition [...]" there'd be something > to discuss. Nope. Then, there will nothing to discuss, because a usual trick then, is to refer to the RM claiming that anything you said is irrelevant to Ada. Instead I offered a bait: two options to choose #1 and #2. These two are complete and independent. It cannot be both, it cannot be none. > pre- and post-conditions most of the method you > seem to be advocating is impossible 1. SPARK 2. Proving correctness of all program >>> proving correctness of contracts But the argument is bogus. If something is wrong it is wrong no matter how implementable it be. In fact, easily implementable wrong things are much more wrong than just wrong ones. (:-)) > (just like any user-input cannot be > guaranteed correct w/o either having all user-input as permissible, or > otherwise validating it) or difficult on the compile-time/static-analysis > level. Bingo! If you CANNOT impose precondition on it, then it is NOT a precondition. There is no contract violated when End_Error is raised by file Read. It is not the contract of Read to be supplied with infinite files! Since, the discussion is perpetually repeating itself, I will tell you your next turn: Ada I/O libraries are lousy, should have never used any exceptions. >> (Historically, pre-/post-conditions were invented by Dijkstra for the >> purpose of proving correctness. Later they were used for types to analyze >> substitutability issues etc.) > > And isn't the idea with Ada's constructs to at least aid proving the > correctness of a program? I heard different opinions on that. But since False => True, you could said so. Unfortunately it is also so that False => False... > Furthermore, wouldn't it be preferable to throw > an exception when the condition is violated? It would be a bug. The rule is simple: bug is when you cannot continue. Whatever you do having a bug is another bug. > That seems to fit perfectly > with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no? No, these are not contract violations. When they are pretended to be, they incur incredible harm. >>> If that was the case then, strictly speaking >>> JavaDoc's pre and postcondition annotating comments are superior to Ada's >>> pre and post condition because they don't implement anything and are, in >>> fact, just comments having no actual impact on the program text. >> >> Not if condition proof fault makes the program illegal. > > It does nothing, insofar as I know, regarding nprogram correctness. > http://en.wikipedia.org/wiki/Java_annotation has as an example the > "override" annotation which when violated only provides a warning. and? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 7:57 ` Dmitry A. Kazakov @ 2012-07-07 1:09 ` Randy Brukardt 2012-07-07 8:44 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-07 1:09 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:l2v5ycmyjzk.11k6wbda0san5.dlg@40tude.net... ... > Instead I offered a bait: two options to choose #1 and #2. These two are > complete and independent. It cannot be both, it cannot be none. They're only "complete and independent" if and only if "contract" includes dynamic contracts. Otherwise, there have to be three things (call the third one "specification", if you like). Because there are lots of things that don't belong to "implementation" (runtime checking of any sort, for instance), and there has to be somewhere to put them. But I suppose only your worthless terminology can be argued. In which case, the answer does not matter, because it is irrelevant to using Ada (or any other practical programming language, for that matter). >> pre- and post-conditions most of the method you >> seem to be advocating is impossible > > 1. SPARK > 2. Proving correctness of all program >>> proving correctness of contracts Proving complete correctness of a program is a pointless, impossible exercise. Real SPARK programs exclude such a large portion of the code, it's unlikely that they've actually proved anything of value. The only real hope is combining static and dynamic checks to improve the correctness of programs. (Absolutely nothing will cause programs to be 100% correct in practice -- why even try?) ... > There is no contract violated when End_Error is raised by file Read. It is > not the contract of Read to be supplied with infinite files! Certainly not. End_Error is clearly not part of the precondition of Read. Mode_Error, OTOH, might be. It doesn't help to take up straw men, you know. It's not possible to write contracts why all exceptions, for every possible exit condition of a subprogram. In *any* language. Nothing about this is about ALL. It's all about MOST. You continue to insist on arguing about ALL. No one cares about ALL, because it is impractical if not impossible. > Since, the discussion is perpetually repeating itself, I will tell you > your > next turn: Ada I/O libraries are lousy, should have never used any > exceptions. Huh? The problem is your insistence on straw men. The only contract that makes sense for Read is "might raise End_Error". There is no possible description of why. And no one anywhere ever said that End_Error should be in a precondition, and certainly not that all exceptions should be in a precondition. I've only said that SOME exceptions should be in a precondition, because violating them is a bug. And only the programmer can determine which makes sense for a particular subprogram -- there cannot be a hard rule about that. End_Error being raised by Read is perfectly normal. Mode_Error being raised by Read is a serious bug. So what? You seem to want hard rules, but that is not how anything works in the real world. After all, "everything is legal so long as you don't get caught" (Traveling Wilburys). ... >> That seems to fit perfectly >> with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no? > > No, these are not contract violations. When they are pretended to be, they > incur incredible harm. What harm? The program is wrong when these happen. It should be fixed if practical. If it cannot be fixed, Ada lets you handle them to recover - but this is not something that should be relied on. If there is a harm, it's that you can't tell between these used as a contract and these used as an implementation artifact (say, handling an overflow error). It would have been nice to differentiate, but that was not done in Ada 83 and it is way too late now. You could of course get that effect by eliminating all of the constraints from your program and using Preconditions and Predicates instead -- that would get all contract failures raising Assertion_Error. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 1:09 ` Randy Brukardt @ 2012-07-07 8:44 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 8:44 UTC (permalink / raw) On Fri, 6 Jul 2012 20:09:32 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:l2v5ycmyjzk.11k6wbda0san5.dlg@40tude.net... > ... >> Instead I offered a bait: two options to choose #1 and #2. These two are >> complete and independent. It cannot be both, it cannot be none. > > They're only "complete and independent" if and only if "contract" includes > dynamic contracts. Otherwise, there have to be three things (call the third > one "specification", if you like). #3 specification. So, dynamic checks belong to specifications? It gets better every day... >> There is no contract violated when End_Error is raised by file Read. It is >> not the contract of Read to be supplied with infinite files! > > Certainly not. End_Error is clearly not part of the precondition of Read. I.e. you agree that exceptions are not necessarily errors. I am glad to hear that, because others claimed that all exceptions are errors. Now, Constraint_Error is an error and End_Error is not so error? Right? > End_Error being raised by Read is perfectly normal. Mode_Error being raised > by Read is a serious bug. So what? I would like to know why Mode_Error is a "serious bug," while End_Error is no bug at all. What in the *language* makes them different? > You seem to want hard rules, but that is not how anything works in the real > world. After all, "everything is legal so long as you don't get caught" > (Traveling Wilburys). No, I want *clear* terms without false excuses about practicality. Now, it is utterly IMPRACTICAL to draw lines between End_Error, Mode_Error, Constraint_Error. They all belong to the implementation. All cases when raised must be contracted formally or informally. >>> That seems to fit perfectly >>> with such as CONSTRAINT_ERROR or PROGRAM_ERROR, no? >> >> No, these are not contract violations. When they are pretended to be, they >> incur incredible harm. > > What harm? The program is wrong when these happen. See above. You are trying to prescribe semantics of a program you never saw. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 13:07 ` Dmitry A. Kazakov 2012-06-26 13:49 ` Georg Bauhaus @ 2012-06-26 14:54 ` stefan-lucks 2012-06-26 15:14 ` Dmitry A. Kazakov 2012-07-03 5:28 ` Randy Brukardt 2 siblings, 1 reply; 125+ messages in thread From: stefan-lucks @ 2012-06-26 14:54 UTC (permalink / raw) On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote: > On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote: > > Don't do that! Emit your messages to to the log file and then terminate! > > Contract violation => terminate. Exceptional state => recover. Yes, exactly! > > But then, what is more important: > > > > - Provide tools that support good software engineering practice? > > > > or > > > > - Prohibit any tools that can be misused? > > > > Dynamically checked contracts are such a tool. > > A wrench sold as shoe polish. This is my point! A wrench is good when used as a wrench, also quite good as a tool for cryptanalysis <http://xkcd.com/538/>, but bad when misused as a shoe polish. > > And (I am sure you know this) any approach to really prove upper bounds > > on the storage requirements would imply to solve the Halting Problem. > > No problem. If you cannot prove it, that is compile error. It is a > conservative estimation, estimations have no halting problem issue, Boolean > values are bounded. > > The real problem lies elsewhere. Prover to tell program legality is thin > ice. Depending on the technique used the same program could be legal (good > prover) or illegal (poor prover). I don't know how to address this, though > nobody cares anyway... It is even worse! An Ada program is either legal or not. It would be a fatal mistake to make legality depend on the theorem prover one is using. That is precisely the reason for checked contracts: Within the language, we cannot prove them. With additional tools, we may be able to prove at least some of them. The tools will improve over time -- hopefully faster than new Ada standards arrive. In the mean time, we can do our best to figure out contract violations by testing. That means, dynamic checks in the test cases. > >> We certainly could learn from Java mistakes rather than repeating them > >> (e.g. interfaces). > > > > Which is probably why Ada so far has no contracted exceptions. Not that > > they cannot be done -- but nobody knows how to write such contracts that > > they really become useful. > > Huh, they didn't much hesitate to borrow flawed Java interfaces, although > the language already had abstract types. Yes, indeed. With respect to borrowing ideas from Java, the ARG has learned! -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html> ------ I love the taste of Cryptanalysis in the morning! ------ ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 14:54 ` stefan-lucks @ 2012-06-26 15:14 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-26 15:14 UTC (permalink / raw) On Tue, 26 Jun 2012 16:54:45 +0200, stefan-lucks@see-the.signature wrote: > On Tue, 26 Jun 2012, Dmitry A. Kazakov wrote: > >> The real problem lies elsewhere. Prover to tell program legality is thin >> ice. Depending on the technique used the same program could be legal (good >> prover) or illegal (poor prover). I don't know how to address this, though >> nobody cares anyway... > > It is even worse! An Ada program is either legal or not. It is an old problem. Not every legal program is compilable: X : constant := 2**(2**<compiler-dependent>); > It would be a > fatal mistake to make legality depend on the theorem prover one is using. You cannot avoid this. The problem is to find right balance by moving most variations out of the sensitive area. > That is precisely the reason for checked contracts: Within the language, > we cannot prove them. With additional tools, we may be able to prove at > least some of them. The tools will improve over time -- hopefully faster > than new Ada standards arrive. In the mean time, we can do our best to > figure out contract violations by testing. That means, dynamic checks in > the test cases. I don't believe in tools. A full integration of the prover would open a completely new level of engineering, when amount of static checks could be adjusted by the programmer incrementally as the project matures by adding or removing goals to prove. >>>> We certainly could learn from Java mistakes rather than repeating them >>>> (e.g. interfaces). >>> >>> Which is probably why Ada so far has no contracted exceptions. Not that >>> they cannot be done -- but nobody knows how to write such contracts that >>> they really become useful. >> >> Huh, they didn't much hesitate to borrow flawed Java interfaces, although >> the language already had abstract types. > > Yes, indeed. With respect to borrowing ideas from Java, the ARG has > learned! Nope, they just switched to Eiffel. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-26 13:07 ` Dmitry A. Kazakov 2012-06-26 13:49 ` Georg Bauhaus 2012-06-26 14:54 ` stefan-lucks @ 2012-07-03 5:28 ` Randy Brukardt 2012-07-03 12:53 ` Dmitry A. Kazakov 2 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-03 5:28 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net... > On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote: ... > They are contracts when checked statically and implementations when > checked > dynamically. No, they're always contracts. They certainly aren't "implementation", because they do *not* belong to the subprogram; they're checked *before* the subprogram is called. (The check, if any, belongs to caller, not the callee.) Besides, I don't understand why it is such a disaster to have precondition contracts be dynamically evaluated in some cases, while it is OK to have a postcondition be dynamically evaluated in some cases -- it too is a contract (one that is evaluated *after* the subprogram finishes). In any case, you want to prevent the any mechanism for specifying these things in code rather than in comments are currently. It should never be necessary for anyone to look into the body ("implementation") of a routine to see the contract (static or dynamic); tools that have to see within bodies (that is, only operate on all of the source) are close to useless (since they can only be used at the end of the development cycle when fixing bugs is at its most expensive). ... >> So you just add "can raise Storage_Error" to any contract? (Maybe >> implicitly.) > > Contracts will be inheritable. I don't know how it goes with aspects, > never > understood what they are good for, but true contracts are inherited while > possibly weakening pre- and strengthening post-conditions (LSP). Yes, of course. Class-wide preconditions are inherited (potentially with weakening, although that's almost never useful), as are class-wide postconditions (with strengthening). (Don't use specific preconditions and postconditions if you care about inheritance.) > Another necessary contract mechanism is composition. That is when you pass > a downward closure to an operation, that could say: I raise what the > argument does. Note that this will require proper procedural types to have > interfaces to carry the contract with. E.g. you would be able to limit the > closure operation to what it is allowed to raise. I agree with the need for composition; we had that in the never-finished "global in/out" contracts. But that doesn't require "procedural types" per-se; it can be done quite easily with the existing facilities. (Whether the result really would be any good, I can't say, but I'm pretty sure that the existence of "procedural types" would make no difference in how useful is is.) ... > The real problem lies elsewhere. Prover to tell program legality is thin > ice. Depending on the technique used the same program could be legal (good > prover) or illegal (poor prover). I don't know how to address this, though > nobody cares anyway... I think some of us care, the problem is assuming that the prover can prove everything important (that will never, ever happen). For me, the biggest impediment is coming up with rules that would allow proving what they can without (a) requiring too much of all compilers and (b) bounding what an implementation can do. There's clearly a portability problem here -- it's quite possible that that problem will prevent ever implementing exception contracts in the Ada language (as opposed to specific implementations). Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 5:28 ` Randy Brukardt @ 2012-07-03 12:53 ` Dmitry A. Kazakov 2012-07-03 13:48 ` Georg Bauhaus 2012-07-05 1:45 ` Randy Brukardt 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-03 12:53 UTC (permalink / raw) On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net... >> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature wrote: > ... >> They are contracts when checked statically and implementations when >> checked dynamically. > > No, they're always contracts. They certainly aren't "implementation", > because they do *not* belong to the subprogram; they're checked *before* the > subprogram is called. Checked by whom? How does this make any difference to the caller or to the program as a whole? Is there a way to determine whether an exception was raised in the body or "before" the body? Maybe there is some special before-the-body-exceptions, propagated in some special manner? It just does not make sense. The contract should refer to all effect of calling the program. > Besides, I don't understand why it is such a disaster to have precondition > contracts be dynamically evaluated in some cases, while it is OK to have a > postcondition be dynamically evaluated in some cases -- it too is a contract > (one that is evaluated *after* the subprogram finishes). It is *not* OK to evaluate precondition of a program by the program itself. It is similar to how halting becomes a problem: procedure P is begin while not HALT (P) loop null; end loop; end P; All this boils down to self-referential stuff. > (Don't use specific preconditions and > postconditions if you care about inheritance.) Which is a telling advise, taking into about that [true] pre-/post-conditions is all [true] interface is about. Inheritance at the interface level is nothing but shuffling pre-/post-conditions. >> Another necessary contract mechanism is composition. That is when you pass >> a downward closure to an operation, that could say: I raise what the >> argument does. Note that this will require proper procedural types to have >> interfaces to carry the contract with. E.g. you would be able to limit the >> closure operation to what it is allowed to raise. > > I agree with the need for composition; we had that in the never-finished > "global in/out" contracts. But that doesn't require "procedural types" > per-se; Propagation of target contracts trough access to the target looks much more complicated. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 12:53 ` Dmitry A. Kazakov @ 2012-07-03 13:48 ` Georg Bauhaus 2012-07-03 14:06 ` Dmitry A. Kazakov 2012-07-05 1:45 ` Randy Brukardt 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-03 13:48 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 13:48 ` Georg Bauhaus @ 2012-07-03 14:06 ` Dmitry A. Kazakov 2012-07-03 16:12 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-03 14:06 UTC (permalink / raw) On Tue, 03 Jul 2012 15:48:32 +0200, Georg Bauhaus wrote: > Yes. Normal program design can hope to get close to a primitive > recursive programming process. If you look how iterative solutions of optimization problems work, you will notice that the goal function is a *function*. Looking from this angle the program P under design is a point in the space of possible programs. The goal function g takes P as an argument. P cannot compute g, it is an argument of. Design process needs g() upfront, which we all know as an empiric rule: you better know what you are going to write. Even such notably poor practices as TDD don't go that far as you would go by putting g into P. TDD keeps g outside P as a set of external test programs. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 14:06 ` Dmitry A. Kazakov @ 2012-07-03 16:12 ` Georg Bauhaus 2012-07-03 16:45 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-03 16:12 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 16:12 ` Georg Bauhaus @ 2012-07-03 16:45 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-03 16:45 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 12:53 ` Dmitry A. Kazakov 2012-07-03 13:48 ` Georg Bauhaus @ 2012-07-05 1:45 ` Randy Brukardt 2012-07-05 7:48 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-05 1:45 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net... > On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net... >>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature >>> wrote: >> ... >>> They are contracts when checked statically and implementations when >>> checked dynamically. >> >> No, they're always contracts. They certainly aren't "implementation", >> because they do *not* belong to the subprogram; they're checked *before* >> the >> subprogram is called. > > Checked by whom? By the caller, not the called body. > How does this make any difference to the caller or to the > program as a whole? Is there a way to determine whether an exception was > raised in the body or "before" the body? Sure: you can handle an exception raised in the body in the body itself; you cannot handle an exception raised by the call in the body. > Maybe there is some special > before-the-body-exceptions, propagated in some special manner? It just > does > not make sense. It's been that way in Ada since at least Ada 80 -- exceptions raised by the call cannot be handled in the body, exceptions raised in the body can be handled in the body. Amazing to find out that the model "does not make sense" after 30+ years. ;-) It has never been the case that constraint failures are part of the effect of the subprogram; they're part of the effect of the call (and thus belong to the caller, not the callee). > The contract should refer to all effect of calling the program. It does. The call itself is not part of the effect of "calling the subprogram". >> Besides, I don't understand why it is such a disaster to have >> precondition >> contracts be dynamically evaluated in some cases, while it is OK to have >> a >> postcondition be dynamically evaluated in some cases -- it too is a >> contract >> (one that is evaluated *after* the subprogram finishes). > > It is *not* OK to evaluate precondition of a program by the program > itself. Well, then the precondition would never be evaluated at all, because there is nothing else. In my world, at least, Ada is the only programming language -- we even used Ada as the language of the command line of our debugger. The notion of using some other language and some other program to describe program semantics is a non-starter. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 1:45 ` Randy Brukardt @ 2012-07-05 7:48 ` Dmitry A. Kazakov 2012-07-05 19:11 ` Adam Beneschan 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-05 7:48 UTC (permalink / raw) On Wed, 4 Jul 2012 20:45:20 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:a555h2psfssb$.1be3awg0xbewa.dlg@40tude.net... >> On Tue, 3 Jul 2012 00:28:31 -0500, Randy Brukardt wrote: >> >>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >>> news:xmybo646240w$.13rwa9qwsliyp$.dlg@40tude.net... >>>> On Tue, 26 Jun 2012 13:50:28 +0200, stefan-lucks@see-the.signature >>>> wrote: >>> ... >>>> They are contracts when checked statically and implementations when >>>> checked dynamically. >>> >>> No, they're always contracts. They certainly aren't "implementation", >>> because they do *not* belong to the subprogram; they're checked *before* >>> the subprogram is called. >> >> Checked by whom? > > By the caller, not the called body. > >> How does this make any difference to the caller or to the >> program as a whole? Is there a way to determine whether an exception was >> raised in the body or "before" the body? > > Sure: you can handle an exception raised in the body in the body itself; you > cannot handle an exception raised by the call in the body. That is irrelevant to the question asked. It was about the CALLER. Whatever happening on the other side is an implementation. You cannot avoid #1 or #2. >> Maybe there is some special >> before-the-body-exceptions, propagated in some special manner? It just >> does not make sense. > > It's been that way in Ada since at least Ada 80 -- exceptions raised by the > call cannot be handled in the body, exceptions raised in the body can be > handled in the body. Amazing to find out that the model "does not make > sense" after 30+ years. ;-) It has never been the case that constraint > failures are part of the effect of the subprogram; they're part of the > effect of the call (and thus belong to the caller, not the callee). All effects always belong to the caller. Whatever the caller does is to obtain these effects. >> The contract should refer to all effect of calling the program. > > It does. The call itself is not part of the effect of "calling the > subprogram". Then the contract does not cover all effects of putting a call statement into an Ada program. The same question again: on the language level, what a sequence of characters denoting call to the subprogram P is supposed to *mean*? The effect of writing, compiling, running programs containing that refer to P is what? Putting it even simpler. What is the effect of: sqrt (-1.0) No effect? Any effect? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 7:48 ` Dmitry A. Kazakov @ 2012-07-05 19:11 ` Adam Beneschan 2012-07-05 19:55 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Adam Beneschan @ 2012-07-05 19:11 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 19:11 ` Adam Beneschan @ 2012-07-05 19:55 ` Dmitry A. Kazakov 2012-07-06 7:41 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-05 19:55 UTC (permalink / raw) On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: > On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: > >> Putting it even simpler. What is the effect of: >> >> sqrt (-1.0) >> >> No effect? Any effect? > > This looks like an imaginary problem to me, not a real one. What problem? It was a simple question illustrating absurdity of the idea. Since the effect is evidently Constraint_Error, then raising it is a required part of the implementation. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 19:55 ` Dmitry A. Kazakov @ 2012-07-06 7:41 ` Georg Bauhaus 2012-07-06 7:47 ` Georg Bauhaus 2012-07-06 8:05 ` Dmitry A. Kazakov 0 siblings, 2 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 7:41 UTC (permalink / raw) 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? ;-) ;-) ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 7:41 ` Georg Bauhaus @ 2012-07-06 7:47 ` Georg Bauhaus 2012-07-06 8:05 ` Dmitry A. Kazakov 1 sibling, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 7:47 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 7:41 ` Georg Bauhaus 2012-07-06 7:47 ` Georg Bauhaus @ 2012-07-06 8:05 ` Dmitry A. Kazakov 2012-07-06 8:30 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-06 8:05 UTC (permalink / raw) On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: > On 05.07.12 21:55, Dmitry A. Kazakov wrote: >> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >> >>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>> >>>> Putting it even simpler. What is the effect of: >>>> >>>> sqrt (-1.0) >>>> >>>> No effect? Any effect? >>> >>> This looks like an imaginary problem to me, not a real one. >> >> What problem? It was a simple question illustrating absurdity of the idea. > > Actually, a negative argument passed to sqrt is illustrating proper DbC > well. One famous example is Ariane 4, (4), that's the number four. If sqrt (-1.0) has no effect, what made Ariane to explode? Exploding is not an effect, right? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 8:05 ` Dmitry A. Kazakov @ 2012-07-06 8:30 ` Georg Bauhaus 2012-07-06 9:01 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 8:30 UTC (permalink / raw) On 06.07.12 10:05, Dmitry A. Kazakov wrote: > On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: > >> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>> >>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>> >>>>> Putting it even simpler. What is the effect of: >>>>> >>>>> sqrt (-1.0) >>>>> >>>>> No effect? Any effect? >>>> >>>> This looks like an imaginary problem to me, not a real one. >>> >>> What problem? It was a simple question illustrating absurdity of the idea. >> >> Actually, a negative argument passed to sqrt is illustrating proper DbC >> well. One famous example is Ariane 4, (4), that's the number four. > > If sqrt (-1.0) has no effect, First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. > what made Ariane to explode? The engineers though the didn't have to re-read the contract for Ariane 4 when moving the software to Ariane 5. > Exploding is not an effect, right? Wrong. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 8:30 ` Georg Bauhaus @ 2012-07-06 9:01 ` Dmitry A. Kazakov 2012-07-06 11:33 ` Simon Wright 2012-07-06 12:07 ` Georg Bauhaus 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-06 9:01 UTC (permalink / raw) On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote: > On 06.07.12 10:05, Dmitry A. Kazakov wrote: >> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: >> >>> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>>> >>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>>> >>>>>> Putting it even simpler. What is the effect of: >>>>>> >>>>>> sqrt (-1.0) >>>>>> >>>>>> No effect? Any effect? >>>>> >>>>> This looks like an imaginary problem to me, not a real one. >>>> >>>> What problem? It was a simple question illustrating absurdity of the idea. >>> >>> Actually, a negative argument passed to sqrt is illustrating proper DbC >>> well. One famous example is Ariane 4, (4), that's the number four. >> >> If sqrt (-1.0) has no effect, > > First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. 1. That no correct program may have it requires a proof. 2. That no program at all may have it, requires yet another proof. 3. While you are busy proving 1 and 2, I'd rather stay on the safe side considering sqrt (-1.0) happen. So, what about the effect? >> what made Ariane to explode? > > The engineers though the didn't have to re-read the contract > for Ariane 4 when moving the software to Ariane 5. But that has no effect or else does not occur... thus it never exploded. >> Exploding is not an effect, right? > > Wrong. Yet explosion occurred. Something must be wrong with the logic again? -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 9:01 ` Dmitry A. Kazakov @ 2012-07-06 11:33 ` Simon Wright 2012-07-06 13:25 ` Dmitry A. Kazakov 2012-07-06 12:07 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Simon Wright @ 2012-07-06 11:33 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes: > On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote: > >> On 06.07.12 10:05, Dmitry A. Kazakov wrote: >>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: >>> >>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>>>> >>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>>>> >>>>>>> Putting it even simpler. What is the effect of: >>>>>>> >>>>>>> sqrt (-1.0) >>>>>>> >>>>>>> No effect? Any effect? >>>>>> >>>>>> This looks like an imaginary problem to me, not a real one. >>>>> >>>>> What problem? It was a simple question illustrating absurdity of >>>>> the idea. >>>> >>>> Actually, a negative argument passed to sqrt is illustrating proper >>>> DbC well. One famous example is Ariane 4, (4), that's the number >>>> four. >>> >>> If sqrt (-1.0) has no effect, >> >> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. > > 1. That no correct program may have it requires a proof. If a DbC program passes a negative argument to sqrt(), then it isn't correct. To prove that a DbC program never passes a negative argument to sqrt() requires a proof (tautology). No proof is required of the statement that a correct program must not pass a negative argument to sqrt() - the contract must be regarded as axiomatic from the caller's pov. > 2. That no program at all may have it, requires yet another proof. I can't make sense of this statement. > 3. While you are busy proving 1 and 2, I'd rather stay on the safe side > considering sqrt (-1.0) happen. So, what about the effect? There will be an exception. What's the problem with that? In my last project, unhandled exceptions caused the system to be rebooted (and missiles in flight to be aborted). If the system throws an unhandled exception it's operating outside its design envelope and safety considerations come in to play. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 11:33 ` Simon Wright @ 2012-07-06 13:25 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-06 13:25 UTC (permalink / raw) On Fri, 06 Jul 2012 12:33:33 +0100, Simon Wright wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes: > >> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote: >> >>> On 06.07.12 10:05, Dmitry A. Kazakov wrote: >>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: >>>> >>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>>>>> >>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>>>>> >>>>>>>> Putting it even simpler. What is the effect of: >>>>>>>> >>>>>>>> sqrt (-1.0) >>>>>>>> >>>>>>>> No effect? Any effect? >>>>>>> >>>>>>> This looks like an imaginary problem to me, not a real one. >>>>>> >>>>>> What problem? It was a simple question illustrating absurdity of >>>>>> the idea. >>>>> >>>>> Actually, a negative argument passed to sqrt is illustrating proper >>>>> DbC well. One famous example is Ariane 4, (4), that's the number >>>>> four. >>>> >>>> If sqrt (-1.0) has no effect, >>> >>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. >> >> 1. That no correct program may have it requires a proof. > > If a DbC program passes a negative argument to sqrt(), then it isn't > correct. (I don't know want a "DbC program" is) A correct implementation of a scientific calculator would certainly do that thing. >> 2. That no program at all may have it, requires yet another proof. > > I can't make sense of this statement. This was to prevent an escape into saying that no program were bug-free. >> 3. While you are busy proving 1 and 2, I'd rather stay on the safe side >> considering sqrt (-1.0) happen. So, what about the effect? > > There will be an exception. I.e. the effect of it is exception propagation in this case. > What's the problem with that? None to me. But for them, the problem is that if they admitted that sqrt were contracted to raise exception, then that would become a part of sqrt implementation, and the whole house of cards would collapse. My point is that the *true* precondition of sqrt is: X in Float And that the true postcondition contains: X < 0.0 and Constraint_Error raised And that there is no any contract violation in calling sqrt(-1.0). The point is also that any case where contracts are checked dynamically in the same code can be killed exactly this way. Contracts of P are not a part of P's behavior. > In my last project, unhandled exceptions caused the system to be > rebooted (and missiles in flight to be aborted). If the system throws an > unhandled exception it's operating outside its design envelope and > safety considerations come in to play. Which is why contracted exceptions are so important. You would do in some client: ... sqrt (X) ... and then add to the postcondition that no Constraint_Error propagates. That would require you either to prove that X >= 0.0 or else to handle Constraint_Error. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 9:01 ` Dmitry A. Kazakov 2012-07-06 11:33 ` Simon Wright @ 2012-07-06 12:07 ` Georg Bauhaus 2012-07-06 13:37 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 12:07 UTC (permalink / raw) On 06.07.12 11:01, Dmitry A. Kazakov wrote: > On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote: > >> On 06.07.12 10:05, Dmitry A. Kazakov wrote: >>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: >>> >>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>>>> >>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>>>> >>>>>>> Putting it even simpler. What is the effect of: >>>>>>> >>>>>>> sqrt (-1.0) >>>>>>> >>>>>>> No effect? Any effect? >>>>>> >>>>>> This looks like an imaginary problem to me, not a real one. >>>>> >>>>> What problem? It was a simple question illustrating absurdity of the idea. >>>> >>>> Actually, a negative argument passed to sqrt is illustrating proper DbC >>>> well. One famous example is Ariane 4, (4), that's the number four. >>> >>> If sqrt (-1.0) has no effect, >> >> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. > > 1. That no correct program may have it requires a proof. Yes, this is why DbC is associated with a proof obligation. > 2. That no program at all may have it, requires yet another proof. Who cares? I mean, really, who cares? Assertion checking is *not* the same as showing that there exists a class of programs written in a suitably restricted language that is free of a number of possible errors. It is about programmers expressing things not expressible in Ada's type system. And DbC is about two parties, not just one. > I'd rather stay on the safe side > considering sqrt (-1.0) happen. So, what about the effect? If you know that you might be running an incorrect program, the effect is similar to that of using Unchecked_Conversion. >>> what made Ariane to explode? >> >> The engineers though the didn't have to re-read the contract >> for Ariane 4 when moving the software to Ariane 5. > > But that has no effect or else does not occur... thus it never exploded. "That" = the contract? If a program is correct, then checking contract clauses does not have adverse effects. If a program is incorrectly calling sqrt with a negative argument, there are two practical cases 1) [wrong -1.0 and checks on] detects violation, restarts if possible 2) [wrong -1.0 and checks off] whatever sqrt's body does Both situations can make the system crash, because it might not be possible to retry using another, fresh value for r in case 1). Some have expressed a preference for detection (1) over erratic performance (2). I'll note in passing that a check is *not* testing I/O values. By the Ariane analogy, the original *system* was assumed, correctly, to guarantee that r >= 0.0. But another, different assembly of a new system rendered the guarantee void, introducing an explosive bug. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 12:07 ` Georg Bauhaus @ 2012-07-06 13:37 ` Dmitry A. Kazakov 2012-07-06 16:17 ` Georg Bauhaus ` (2 more replies) 0 siblings, 3 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-06 13:37 UTC (permalink / raw) On Fri, 06 Jul 2012 14:07:52 +0200, Georg Bauhaus wrote: > On 06.07.12 11:01, Dmitry A. Kazakov wrote: >> On Fri, 06 Jul 2012 10:30:01 +0200, Georg Bauhaus wrote: >> >>> On 06.07.12 10:05, Dmitry A. Kazakov wrote: >>>> On Fri, 06 Jul 2012 09:41:18 +0200, Georg Bauhaus wrote: >>>> >>>>> On 05.07.12 21:55, Dmitry A. Kazakov wrote: >>>>>> On Thu, 5 Jul 2012 12:11:57 -0700 (PDT), Adam Beneschan wrote: >>>>>> >>>>>>> On Thursday, July 5, 2012 12:48:30 AM UTC-7, Dmitry A. Kazakov wrote: >>>>>>> >>>>>>>> Putting it even simpler. What is the effect of: >>>>>>>> >>>>>>>> sqrt (-1.0) >>>>>>>> >>>>>>>> No effect? Any effect? >>>>>>> >>>>>>> This looks like an imaginary problem to me, not a real one. >>>>>> >>>>>> What problem? It was a simple question illustrating absurdity of the idea. >>>>> >>>>> Actually, a negative argument passed to sqrt is illustrating proper DbC >>>>> well. One famous example is Ariane 4, (4), that's the number four. >>>> >>>> If sqrt (-1.0) has no effect, >>> >>> First, in a DbC correct program, sqrt(r) where r < 0.0 does not occur. >> >> 1. That no correct program may have it requires a proof. > > Yes, this is why DbC is associated with a proof obligation. Yes, yes. Where is the proof? > And DbC is about two parties, not just one. And both parties belong to the same program. >> I'd rather stay on the safe side >> considering sqrt (-1.0) happen. So, what about the effect? > > If you know that you might be running an incorrect program, > the effect is similar to that of using Unchecked_Conversion. Maybe for Ada 202X, but in contemporary Ada it is Constraint_Error propagation. But wait a minute and re-read what you wrote. You say that the behaviour of sqrt(-1.0) is basically unspecified. This is where dynamic checks have led you into. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 13:37 ` Dmitry A. Kazakov @ 2012-07-06 16:17 ` Georg Bauhaus 2012-07-06 16:34 ` Georg Bauhaus 2012-07-07 1:18 ` Randy Brukardt 2 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 16:17 UTC (permalink / raw) On 06.07.12 15:37, Dmitry A. Kazakov wrote: > You say that the behaviour of > sqrt(-1.0) is basically unspecified. This is where dynamic checks have led > you into. I said that the behavior of sqrt(-1.0) is basically unspecified IFF the programmer (a) violates the contract (b) turns off contract checking If the programmer doesn't do this, then the behavior of a program calling sqrt(-1.0) is specified. SPARK prevents the foolishness of (a) + (b) in a technical way, for SPARK programs. General programs require tests at run-time and programmer intervention. Like pragma Assert does, too. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 13:37 ` Dmitry A. Kazakov 2012-07-06 16:17 ` Georg Bauhaus @ 2012-07-06 16:34 ` Georg Bauhaus 2012-07-06 19:18 ` Dmitry A. Kazakov 2012-07-07 1:18 ` Randy Brukardt 2 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 16:34 UTC (permalink / raw) On 06.07.12 15:37, Dmitry A. Kazakov wrote: >>> I'd rather stay on the safe side >>> >> considering sqrt (-1.0) happen. So, what about the effect? >> > >> > If you know that you might be running an incorrect program, >> > the effect is similar to that of using Unchecked_Conversion. > Maybe for Ada 202X, but in contemporary Ada it is Constraint_Error > propagation. Could you leave clauses of an explicitly state contract in the text where there was one? function sqrt (x : REAL) return REAL with Pre => x >= 0.0; Ada's sqrt, as opposed to the sqrt above, adds a run-time check, fully dynamic. The programmer can throw anything at Ada's sqrt, quite carelessly. Its contract isn't specified in source text, but requires that the programmer study the language manual in order to learn about his obligations, and possible consequences. When not, the program needs to handle Constraint_Error all over the place because he or she *never* knows what precondition to establish, other than by reading through more or less formal comments. Triply bad. If we had function sqrt (x : REAL) return REAL with Pre => True Post => sqrt'result * sqrt'result = x � eps or else *@$!; instead, then (1) we not only have to handle exceptions, but (2) we cannot really see from sqrt's specification what to do in order to avoid them, and (3) we cannot have an efficient sqrt because Ada's sqrt forces a test on us that is quite unnecessary once we know, i.e. have shown, that x >= 0.0 is always true before calling sqrt. So Ada's sqrt is programmed defensively, whereas the line of defence in a program designed by contract is to feel obliged by the contract and then either demonstrate correctness, or leave the checks in! ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 16:34 ` Georg Bauhaus @ 2012-07-06 19:18 ` Dmitry A. Kazakov 2012-07-07 1:24 ` Randy Brukardt 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-06 19:18 UTC (permalink / raw) On Fri, 06 Jul 2012 18:34:37 +0200, Georg Bauhaus wrote: > On 06.07.12 15:37, Dmitry A. Kazakov wrote: > > function sqrt (x : REAL) return REAL > with Pre => True > Post => sqrt'result * sqrt'result = x � eps or else *@$!; Post => ( X'Valid and then X >= 0.0 and then ( sqrt'Result * sqrt'Result = X or else ( sqrt'Result * sqrt'Result > X and then sqrt'Result * sqrt'Result = X'Succ ) or else ( sqrt'Result * sqrt'Result < X and then sqrt'Result * sqrt'Result = X'Pred ) ) ) or else ( (not X'Valid or else X < 0.0) and then Constraint_Error raised ); > instead, then (1) we not only have to handle exceptions, 1. Wrong. An exception is still there. > but (2) we cannot really see from sqrt's specification what to do in order to avoid them, 2. Wrong, it is clearly seen from the post-condition > and (3) we cannot have an efficient sqrt because Ada's sqrt forces > a test on us that is quite unnecessary once we know, i.e. have shown, > that x >= 0.0 is always true before calling sqrt. 3. Wrong. There is no whatsoever difference to dynamic check in that respect. The implementation is same. That is BTW why there is no such thing as "dynamic check." And surely the second part of the postcondition can be ignored if proven that X > 0.0, which would let the optimizing compiler to deploy a modified body without check. See, doing things properly is always safer and no less efficient. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 19:18 ` Dmitry A. Kazakov @ 2012-07-07 1:24 ` Randy Brukardt 2012-07-07 9:09 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-07 1:24 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net... ... > 1. Wrong. An exception is still there. Sure, but the compiler can prove that it will not be raised (at least part of the time). The Sqrt in the LRM has not such possibility; a caller would always have to assume that it is raised. >> but (2) we cannot really see from sqrt's specification what to do in >> order to avoid them, > > 2. Wrong, it is clearly seen from the post-condition It was clear as mud to me. Pre => (if A < 0.0 then raise Constraint_Error); is a *lot* clearer to me. >> and (3) we cannot have an efficient sqrt because Ada's sqrt forces >> a test on us that is quite unnecessary once we know, i.e. have shown, >> that x >= 0.0 is always true before calling sqrt. > > 3. Wrong. There is no whatsoever difference to dynamic check in that > respect. The implementation is same. That is BTW why there is no such > thing > as "dynamic check." And surely the second part of the postcondition can be > ignored if proven that X > 0.0, which would let the optimizing compiler to > deploy a modified body without check. Definitely wrong. Any decent compiler will completely eliminate the dynamic check on the precondition given above (presuming the actual value allows that). (Preconditions are checked at the call site, not inside the body.) No compiler can eliminate a dynamic check written in a body. So the generated code will be very different. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 1:24 ` Randy Brukardt @ 2012-07-07 9:09 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 9:09 UTC (permalink / raw) On Fri, 6 Jul 2012 20:24:39 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:80rid9aui8jv$.wg3phwexxdfy$.dlg@40tude.net... > ... >>> but (2) we cannot really see from sqrt's specification what to do in >>> order to avoid them, >> >> 2. Wrong, it is clearly seen from the post-condition > > It was clear as mud to me. > > Pre => (if A < 0.0 then raise Constraint_Error); > > is a *lot* clearer to me. Precondition is a predicate. Predicate is a Boolean valued function per definition. http://en.wikipedia.org/wiki/Predicate_%28mathematical_logic%29 It cannot raise anything. The formula above is meaningless, shows how damaging if-operator stuff could become. The proper precondition of sqrt that does not raise [we hope that it would not, but for "practical reasons" take that it does not] is: Pre => A >= 0.0 (and A'Valid) The precondition of sqrt that does raise is: Pre => True The postcondiion is also a predicate, which could only state that Constraint_Error is underway, e.g.: Post => ... (A < 0.0 and Constraint_Error RAISED) ...; If exception will ever be contracted, you would never see them in preconditions. From the proof POV, there is no difference. Both are equivalently difficult or simple to prove, because it is essentially A < 0.0. >>> and (3) we cannot have an efficient sqrt because Ada's sqrt forces >>> a test on us that is quite unnecessary once we know, i.e. have shown, >>> that x >= 0.0 is always true before calling sqrt. >> >> 3. Wrong. There is no whatsoever difference to dynamic check in that >> respect. The implementation is same. That is BTW why there is no such thing >> as "dynamic check." And surely the second part of the postcondition can be >> ignored if proven that X > 0.0, which would let the optimizing compiler to >> deploy a modified body without check. > > Definitely wrong. Any decent compiler will completely eliminate the dynamic > check on the precondition given above (presuming the actual value allows > that). This is what I wrote. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-06 13:37 ` Dmitry A. Kazakov 2012-07-06 16:17 ` Georg Bauhaus 2012-07-06 16:34 ` Georg Bauhaus @ 2012-07-07 1:18 ` Randy Brukardt 2012-07-07 9:14 ` Dmitry A. Kazakov 2 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-07 1:18 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:7xnkuta2d94n$.1815f9iev4s7r$.dlg@40tude.net... ... > But wait a minute and re-read what you wrote. You say that the behaviour > of > sqrt(-1.0) is basically unspecified. This is where dynamic checks have led > you into. If you suppress checks, basically the behavior of all programs are unspecified. Thus, I highly recommend that you don't do that. (Consider Suppress similar to Unchecked_Conversion -- OK when used in the right hands, dangerous otherwise.) If you *don't* suppress checks, the behavior is well-defined. So what? Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 1:18 ` Randy Brukardt @ 2012-07-07 9:14 ` Dmitry A. Kazakov 2012-07-07 12:06 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 9:14 UTC (permalink / raw) On Fri, 6 Jul 2012 20:18:31 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:7xnkuta2d94n$.1815f9iev4s7r$.dlg@40tude.net... > ... >> But wait a minute and re-read what you wrote. You say that the behaviour of >> sqrt(-1.0) is basically unspecified. This is where dynamic checks have led >> you into. > > If you suppress checks, basically the behavior of all programs are > unspecified. There was no *IF*. > If you *don't* suppress checks, the behavior is well-defined. So what? That the same function's behavior might be both defined and undefined. There must be something wrong with that function, the definition of "behavior", dynamic checks, Georg's statements. The choice is up to the reader. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 9:14 ` Dmitry A. Kazakov @ 2012-07-07 12:06 ` Georg Bauhaus 2012-07-07 12:54 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-07 12:06 UTC (permalink / raw) On 07.07.12 11:14, Dmitry A. Kazakov wrote: > That the same function's behavior might be both defined and undefined. The function's behavior is not affected by assertion checking: A DbC function computes as if it its pre condition were true. Whatever the caller is going to pass to sqrt, the function sqrt corresponds to a sequence of instructions that compute a value from a float argument that is taken to be >= 0.0. Reason: it was stated in the contract. "shocking at first to many, it is among the method's main contributions to software reliability and deserves emphasis." (OOSC2, � 11.6) ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 12:06 ` Georg Bauhaus @ 2012-07-07 12:54 ` Dmitry A. Kazakov 2012-07-07 13:31 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 12:54 UTC (permalink / raw) On Sat, 07 Jul 2012 14:06:46 +0200, Georg Bauhaus wrote: > On 07.07.12 11:14, Dmitry A. Kazakov wrote: >> That the same function's behavior might be both defined and undefined. > > The function's behavior is not affected by assertion checking: Whatever it be. You wrote about the effect of sqrt exactly this: "the effect is similar to that of using Unchecked_Conversion." -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 12:54 ` Dmitry A. Kazakov @ 2012-07-07 13:31 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-07 13:31 UTC (permalink / raw) On 07.07.12 14:54, Dmitry A. Kazakov wrote: > On Sat, 07 Jul 2012 14:06:46 +0200, Georg Bauhaus wrote: > >> On 07.07.12 11:14, Dmitry A. Kazakov wrote: >>> That the same function's behavior might be both defined and undefined. >> >> The function's behavior is not affected by assertion checking: > > Whatever it be. You wrote about the effect of sqrt exactly this: > > "the effect is similar to that of using Unchecked_Conversion." Yes, the function's behavior is according to both sides of the stated contract. Continuing the Unchecked_Conversion analogy, there are safe uses of Unchecked_Conversion. Improving Ada 2005, a full DbC method allows formalizing these safe use cases to the extent possible in each case. For example, it is safe to call sqrt if the caller ensures the conditions stated in the explicit contract of my_sqrt. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-25 19:42 ` Dmitry A. Kazakov 2012-06-26 11:50 ` stefan-lucks @ 2012-07-03 5:10 ` Randy Brukardt 1 sibling, 0 replies; 125+ messages in thread From: Randy Brukardt @ 2012-07-03 5:10 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:bdpvyb9h7rvt.zbq0kbiq72wj.dlg@40tude.net... ... >> Sure! So what? > > How are going to marry exceptions propagating from contracts with > contracts > on exceptions? Some exceptions are more exceptional than others? Aren't we > fed up with Program_Error? That's trivial. Exceptions from contracts occur at the call site; they're not part of the subprogram. Of course they *are* part of the contract of the subprogram that made the call. It works just like propagation. You have far too narrow of a view of what a contract is. Open up your mind, and it will all make far more sense. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-22 23:08 ` Dmitry A. Kazakov 2012-06-23 10:46 ` Georg Bauhaus @ 2012-07-03 4:51 ` Randy Brukardt 2012-07-03 12:46 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-03 4:51 UTC (permalink / raw) (Note: I haven't yet read anyone else's response to this thread; but I thought I owed Dmitry a response. If this ground was previously covered, please feel free to ignore my response.) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net... > On Fri, 22 Jun 2012 14:41:55 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >> news:1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net... >>> On Thu, 21 Jun 2012 15:32:21 -0500, Randy Brukardt wrote: >>> >>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >>>> news:npdjip6ohqlt$.1x6bxc9jsaago$.dlg@40tude.net... >>>> ... >>>>> This is what constitutes the core inconsistency about dynamic >>>>> pre-/post-conditions. If they #1 implement behavior (e.g the stack >>>>> contract >>>>> to raise something when full), then they cannot be suppressed and do >>>>> not >>>>> describe the contract. If they do describe the contract #2, they may >>>>> not >>>>> implement it and thus shall have no run-time effect. >>>> >>>> You're right, but I don't see any inconsistency. They are clearly #1, >>>> and >>>> that includes all of the existing Ada checks as well. >>> >>> If you take a stance on #1, then checking stack full is no more >>> evaluation >>> of the precondition, which does not depend on the stack state anymore, >>> as >>> it of course should be. So the "true" precondition is just: True. >> >> Huh? This makes no sense whatsoever. >> >> We can't require static detection of precondition failures any more than >> we >> can demand static detection of range violations. > > You seem to imply that value in the range is a precondition of the > operation constrained to that range. This is wrong. It can't be "wrong", because the programmer of an abstraction decides what the preconditions and postconditions are. > If S is a subtype of T then the precondition is > > X in T > > The postcondition is > > (X in S and <something>) or (X not in S and Constraint_Error propagated) > >> And Ada *always* has had dynamic preconditions: >> >> procedure New_Line (Spacing : in Positive_Count := 1); > > The precondition here is Spacing in Positive_Count'Base because the > behavior of New_Line is *defined* when Spacing is not in > Positive_Count'Range. > > New_Line(0) > > is a *legal* Ada program. Legality has nothing to do with preconditions or postconditions. Preconditions and postconditions are two sides of the same coin. They're checks made on the way into and the way out of a subprogram. There is absolutely no justification for saying that these are different in some way. You are saying that only a postcondition can have dynamic components, which is nonsense. You seem to want to associate the actions of the precondition with the subprogram itself, but that is also wrong. Preconditions are checked *before* a subprogram is called, so those actions occur *before* anything in the subprogram (and thus anything in the postcondition to the subprogram). You're trying to fit all exceptions into a single box, which is silly. Some exceptions are clearly part of the preconditions of the subprogram -- the only reason that they are exceptions is because it is currently beyond the state of the art to check these statically. Any occurrence of these exceptions in a program represents a bug; they should never happen in a correct program. For instance, the mode check for a file. OTOH, some exceptions are reporting issues that only are detectable *after* the subprogram has been called (for example, the Use_Error caused when a disk is full). Those should be in the exception contract (not the postcondition; that's only for "normal" return; the exception contract might have a separate postcondition for each exceptional return). Deciding between these is something that only the designer of a subprogram can do. No mathematical theory can ever do that. ... >> Nothing you say on this topic makes any sense, at least from an Ada >> perspective. Here you are saying that Ada's entire design and reason for >> existing is "not defendable" > > Why entire? Dynamic correctness checks are not defendable, as demonstrated > on numerous examples. The only kind of correctness checks that *can* exist in general are dynamic. Ada's entire reason to exist is to include checks like range checks and overflow checks to programs. Without them you get the buffer overflows and other errors that plague C code. Compile-time detection of bugs is only possible in very limited and not very useful cases. Limiting a programming language to those cases only makes it unusable (exhibit #1 - SPARK). I suppose you have a totally different definition of "correctness checks" than I do; as usual, we can't have a useful discussion because you have your own set of terminology. ... >> How your ideal language might work is irrelevevant in this forum. > > It is not mine language. It is a methodology of defining and proving > program correctness as introduced by Dijkstra. It applies to all languages > without exemption. We're not interested in "proving program correctness". That's (still) beyond the state of the art for any realistic programming language. We *are* interested in dynamic features that can provide information to future static analysis tools. But realistic analysis tools will never (and should never) try for "complete" analysis. >> Please talk about Ada, not impossible theory. > > The only impossible theory here is about meaning of dynamically checked > preconditions, e.g. #1 or #2? That is indeed impossible, because > inconsistent. Otherwise Dijkstra's approach works pretty well with any > language, e.g. SPARK does for Ada. SPARK is next to useless for real programs - at best it can be used only to prove small parts of a program, and it takes a lot of effort to get there. It's the sort of thing that turns programmers off (it *certainly* has done that to me!) and essentially pushes them to stick with the unsafe languages that they are using. Instead of getting the benefits of building in Ada now, and getting more and more static checks as compilers improve. This idea of "perfect" proving has essentially prevented these techniques from moving into the mainstream, and it is sad that this is the case. Anyway, if you are going to push "program proving", then we literally have nothing to talk about. So this conversation is done. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 4:51 ` Randy Brukardt @ 2012-07-03 12:46 ` Dmitry A. Kazakov 2012-07-05 2:18 ` Randy Brukardt 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-03 12:46 UTC (permalink / raw) On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:1oih2rok18dmt.avbwrres5k12.dlg@40tude.net... >> You seem to imply that value in the range is a precondition of the >> operation constrained to that range. This is wrong. > > It can't be "wrong", because the programmer of an abstraction decides what > the preconditions and postconditions are. No. He cannot decide them to implement the contract. That he actually can, per allowing dynamic checks, is a language design bug. >> If S is a subtype of T then the precondition is >> >> X in T >> >> The postcondition is >> >> (X in S and <something>) or (X not in S and Constraint_Error propagated) >> >>> And Ada *always* has had dynamic preconditions: >>> >>> procedure New_Line (Spacing : in Positive_Count := 1); >> >> The precondition here is Spacing in Positive_Count'Base because the >> behavior of New_Line is *defined* when Spacing is not in >> Positive_Count'Range. >> >> New_Line(0) >> >> is a *legal* Ada program. > > Legality has nothing to do with preconditions or postconditions. => It is OK to violate a "contract" defined by these. Here you are. > The only kind of correctness checks that *can* exist in general are dynamic. > Ada's entire reason to exist is to include checks like range checks and > overflow checks to programs. Without them you get the buffer overflows and > other errors that plague C code. Yes, but irrelevant. These checks are not contract checks, because, otherwise you are in contradiction. No words can change that. But also there are important consequences for software engineering. Since these checks have nothing to do with contracts, they must be considered as a part of the program semantics and all possible outcomes must be *handled*. The problem of buffer overflow is exactly in pretending that it cannot overflow. So the program is broken when it does. > I suppose you have a totally different definition of "correctness checks" > than I do; as usual, we can't have a useful discussion because you have your > own set of terminology. Terminology is secondary to the semantics. The problem is with the meaning. > SPARK is next to useless for real programs - at best it can be used only to > prove small parts of a program, and it takes a lot of effort to get there. You don't need to prove every possible aspect of the program. The language should allow the programmer to choose. Ada 83 had provable contracts stated in terms of types. Nothing prevents us from having more detailed contracts as well as other program correctness stuff. I simply don't understand where is a problem with that. > Instead of getting the benefits of building in Ada now, > and getting more and more static checks as compilers improve. I don't see tracking down exceptions as a benefit. Neither would it be a for the maintainer to discover that the program suddenly became illegal because static checks has been "improved." I prefer to rely on things known to work now. These I use and hope that they will continue to work in the future. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-03 12:46 ` Dmitry A. Kazakov @ 2012-07-05 2:18 ` Randy Brukardt 2012-07-05 8:48 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-05 2:18 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... > On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: ... >> Legality has nothing to do with preconditions or postconditions. > > => It is OK to violate a "contract" defined by these. Here you are. No, it's not OK; that is the crux of our disagreement. You seem to think that the only kind of "contract" is some sort of static thing. But that's never, ever been true in Ada. Exactly. You claim that there cannot be such a thing as a dynamically enforced contract. But that's simply bogus - Ada has had those since the beginning of time - they were called "constraints". Failing one of these checks means that your program is wrong. Ada of course defines what happens (raising an exception, etc.), but handling those does not make your program less wrong. The only reason that these aren't detected statically is the difficulty (and impossibility, in some cases) of detecting them statically. Yes, of course, there are also exceptions raised for reasons outside of a contract (that is, those that don't appear in the profile of a subprogram), and handling those might make sense in a correct program. But handling exceptions raised for contracts does not make the program any less wrong; indeed, the only legitimate reasons for handling those is to make debugging easier [and, in a few applications, to make the application "bullet-proof"]. >> The only kind of correctness checks that *can* exist in general are >> dynamic. >> Ada's entire reason to exist is to include checks like range checks and >> overflow checks to programs. Without them you get the buffer overflows >> and >> other errors that plague C code. > > Yes, but irrelevant. These checks are not contract checks, because, > otherwise you are in contradiction. No words can change that. Certainly not if you insist on using an unnecessarily limiting definition of "contract". > But also there are important consequences for software engineering. Since > these checks have nothing to do with contracts, they must be considered as > a part of the program semantics and all possible outcomes must be > *handled*. The problem of buffer overflow is exactly in pretending that it > cannot overflow. So the program is broken when it does. That's certainly a fallacy in general. Most Ada programs are best off *not* handling exceptions caused by outright bugs, because the Ada runtime will do a better job of pinpointing the source of the error than any facility you could create yourself. Of course, some programs have to be bullet-proof, but that is the tiny minority. In a sense, of course, it's the Ada runtime that's providing the "handling" of those bugs (runtime contract failures). And that means a programmer doesn't have to, unless they need bulletproof code that is resistent to bugs. A lot of programs are *not* in this category. The Janus/Ada compiler, for instance, makes no attempt to handle such bugs -- it's much better to abandon the compilation attempt immediately rather than producing a program based on guessing what was intended. >> I suppose you have a totally different definition of "correctness checks" >> than I do; as usual, we can't have a useful discussion because you have >> your >> own set of terminology. > > Terminology is secondary to the semantics. The problem is with the > meaning. Right. I recall in the past that you've been unwilling to grasp the idea of bugs being detected at runtime. Just because Ada defines what happens in those cases does not suddenly make it OK to introduce bugs into a program. >> SPARK is next to useless for real programs - at best it can be used only >> to >> prove small parts of a program, and it takes a lot of effort to get >> there. > > You don't need to prove every possible aspect of the program. The language > should allow the programmer to choose. Ada 83 had provable contracts > stated > in terms of types. Nothing prevents us from having more detailed contracts > as well as other program correctness stuff. I simply don't understand > where > is a problem with that. That's what we're trying to do, and you *obviously* have a problem with that. Learning more languages and more tools to do what an Ada compiler ought to be able to do is silly. >> Instead of getting the benefits of building in Ada now, >> and getting more and more static checks as compilers improve. > > I don't see tracking down exceptions as a benefit. Neither would it be a > for the maintainer to discover that the program suddenly became illegal > because static checks has been "improved." That's not a real problem, because any such program is already wrong (its depending on the failure of a dynamic contract). Sure, people can write such code, but it's just like overlaying objects using address clauses -- it might work, but its still wrong and there is no guarentee that a newer compiler version will not break such things. [As an aside, this means you do not want real exception contracts, since they cannot usefully be done without having it be implementation-defined when an exception is raised by a predefined check. The canonical semantics of Ada would require assuming that every line raises Storage_Error, Program_Error, and usually Constraint_Error -- that would make it virtually impossible to eliminate those exceptions from contracts. OTOH, compilers can and do remove most of those canonical checks, and letting the contracts be enforced against whatever is actually raised by the generated code would be much more useful. But it is impractical to specify the checks that have to be removed (and not very helpful - it could only be a very small number), so what is raised has to be implementation-defined. Which means that just because a contract works on one compiler does not mean that it will work on another compiler (including a later version of the same compiler). I agree with you that runtime detection of exception contract failure makes no sense, so the only choices are implementation-defined or non-existent.] Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 2:18 ` Randy Brukardt @ 2012-07-05 8:48 ` Dmitry A. Kazakov 2012-07-05 12:07 ` Georg Bauhaus 2012-07-07 0:43 ` Randy Brukardt 0 siblings, 2 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-05 8:48 UTC (permalink / raw) On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... >> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: > ... >>> Legality has nothing to do with preconditions or postconditions. >> >> => It is OK to violate a "contract" defined by these. Here you are. > > No, it's not OK; that is the crux of our disagreement. You seem to think > that the only kind of "contract" is some sort of static thing. Exactly. Because the contract exists *before* any programs implementing it and after them. The contract exists even when there is no such program. Therefore it cannot depend on the program state. Another way to understand this: a contract describes states of a program. As such it cannot depend on them. Yet another way: the language of contracts is not the object language: http://en.wikipedia.org/wiki/Object_language > But that's never, ever been true in Ada. I already said that type constraints are not contracts. E.g. an actual value of the discriminant does not create a new contract. The contract covers *all* possible values of the discriminant. > Exactly. You claim that there cannot be such a thing as a dynamically > enforced contract. Absolutely. How could you enforce a contract which has been *already* violated? If a program reaches an illegal state, it is in that state. Period. > But handling exceptions raised for contracts does not make the program any > less wrong; Really? What is the purpose of the exercise? Raising exception, rolling the stack, finalizing stuff, and so on only to resign that the program is as wrong as it was before? (Maybe it is even *more* wrong than it was? (:-)) >>> The only kind of correctness checks that *can* exist in general are dynamic. >>> Ada's entire reason to exist is to include checks like range checks and >>> overflow checks to programs. Without them you get the buffer overflows >>> and other errors that plague C code. >> >> Yes, but irrelevant. These checks are not contract checks, because, >> otherwise you are in contradiction. No words can change that. > > Certainly not if you insist on using an unnecessarily limiting definition of > "contract". Yes, the contract as opposed to the implementation limits the former not to be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada 2012 "contracts" are implementations [POV #1]. Do you? >> But also there are important consequences for software engineering. Since >> these checks have nothing to do with contracts, they must be considered as >> a part of the program semantics and all possible outcomes must be >> *handled*. The problem of buffer overflow is exactly in pretending that it >> cannot overflow. So the program is broken when it does. > > That's certainly a fallacy in general. Most Ada programs are best off *not* > handling exceptions caused by outright bugs, What about the statement: "Most Ada programs are best off not adding integer numbers caused by outright bugs"? The actual fallacy is in pretending that a bug can be handled. You can handle/be in only anticipated states. The proper statement should have been: "Ada is best to make the programmer aware of the states he might overlooked." >>> I suppose you have a totally different definition of "correctness checks" >>> than I do; as usual, we can't have a useful discussion because you have >>> your own set of terminology. >> >> Terminology is secondary to the semantics. The problem is with the >> meaning. > > Right. I recall in the past that you've been unwilling to grasp the idea of > bugs being detected at runtime. Sure, because that is rubbish, and always was: http://en.wikipedia.org/wiki/Liar_paradox > [As an aside, this means you do not want real exception contracts, since > they cannot usefully be done without having it be implementation-defined > when an exception is raised by a predefined check. The canonical semantics > of Ada would require assuming that every line raises Storage_Error, > Program_Error, and usually Constraint_Error -- that would make it virtually > impossible to eliminate those exceptions from contracts. I don't see it as a big problem. There is a difference between an obligation to raise exception and a possibility that an exception could be raised. The contract language should deploy the intuitionistic logic. That is necessary anyway because some things are not provable. In the intuitionistic logic A or not A is not true (no law of excluded middle). E.g. "raise E" (I will raise E) and not "not raise E" (I may raise E. I don't promise not to rase E) are not equivalent statements. The vendors could gradually reduce the number of cases where E may be raised without making clients relying on weaker contracts illegal. The second cannot be misused to prove that E is raised. It just does not follow from the second, and conversely. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 8:48 ` Dmitry A. Kazakov @ 2012-07-05 12:07 ` Georg Bauhaus 2012-07-05 12:13 ` Georg Bauhaus 2012-07-05 12:31 ` Dmitry A. Kazakov 2012-07-07 0:43 ` Randy Brukardt 1 sibling, 2 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-05 12:07 UTC (permalink / raw) On 05.07.12 10:48, Dmitry A. Kazakov wrote: > On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... >>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: >> ... >>>> Legality has nothing to do with preconditions or postconditions. >>> >>> => It is OK to violate a "contract" defined by these. Here you are. >> >> No, it's not OK; that is the crux of our disagreement. You seem to think >> that the only kind of "contract" is some sort of static thing. > > Exactly. Because the contract exists *before* any programs implementing it > and after them. The contract exists even when there is no such program. OK > Therefore it cannot depend on the program state. The "therefore" does not follow, because "it" makes too far reaching assumptions, from which, I think, no one suggests your logic does not follow. "It", for a start, once it materializes in this or that form. Contract checking built into a program is rather a design tool than some oracular inference engine. Correctness need not be assumed at this stage. If the checks are severely flawed bacause some programmer inserts viral side effects in checked expressions, or just wishes to start from the proof of the absence of 666 consecutive digits of e in π on the way, then so be it. He or she is violating the goals of designing with the help of assertions. The goal is *not* unrolling proven assumptions into source text, but arriving at proven systems. So that turning off assertion checking can be considered safe. Safe because checking will not affect the desired effect of the program in any way that is covered by the contract-as-agreed as being essential. So IMHO Pre/Post/Inv are really improvements of pragma Assert. > Another way to understand this: a contract describes states of a program. That's not a contract. There are no parties. There is no obligation to make predicates true on either side. A program could define states, in the contract's space. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 12:07 ` Georg Bauhaus @ 2012-07-05 12:13 ` Georg Bauhaus 2012-07-05 12:31 ` Dmitry A. Kazakov 1 sibling, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-05 12:13 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 12:07 ` Georg Bauhaus 2012-07-05 12:13 ` Georg Bauhaus @ 2012-07-05 12:31 ` Dmitry A. Kazakov 2012-07-05 18:16 ` Georg Bauhaus 1 sibling, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-05 12:31 UTC (permalink / raw) On Thu, 05 Jul 2012 14:07:02 +0200, Georg Bauhaus wrote: > On 05.07.12 10:48, Dmitry A. Kazakov wrote: >> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: >> >>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >>> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... >>>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: >>> ... >>>>> Legality has nothing to do with preconditions or postconditions. >>>> >>>> => It is OK to violate a "contract" defined by these. Here you are. >>> >>> No, it's not OK; that is the crux of our disagreement. You seem to think >>> that the only kind of "contract" is some sort of static thing. >> >> Exactly. Because the contract exists *before* any programs implementing it >> and after them. The contract exists even when there is no such program. > > OK >> Therefore it cannot depend on the program state. > > The "therefore" does not follow, It does. States of P do not exist before P, which does not exist before its contract. ["exists before" is a transitive relation] > because "it" makes too far reaching > assumptions, from which, I think, no one suggests your logic does not > follow. Can you point these assumptions out? >> Another way to understand this: a contract describes states of a program. > > That's not a contract. Not any such thing is a contract. But any contract is such thing. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 12:31 ` Dmitry A. Kazakov @ 2012-07-05 18:16 ` Georg Bauhaus 2012-07-05 19:57 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-05 18:16 UTC (permalink / raw) 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 ... ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 18:16 ` Georg Bauhaus @ 2012-07-05 19:57 ` Dmitry A. Kazakov 2012-07-06 6:53 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-05 19:57 UTC (permalink / raw) On Thu, 05 Jul 2012 20:16:42 +0200, Georg Bauhaus wrote: > On 05.07.12 14:31, Dmitry A. Kazakov wrote: >>> too far reaching >>> > assumptions, from which, I think, no one suggests your logic does not >>> > follow. >> Can you point these assumptions out? >> > > moment, please ... (infinite recursion into self-referential propositions (:-)) -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 19:57 ` Dmitry A. Kazakov @ 2012-07-06 6:53 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-07-06 6:53 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-05 8:48 ` Dmitry A. Kazakov 2012-07-05 12:07 ` Georg Bauhaus @ 2012-07-07 0:43 ` Randy Brukardt 2012-07-07 8:06 ` Dmitry A. Kazakov 1 sibling, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-07-07 0:43 UTC (permalink / raw) "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message news:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net... > On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: > >> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message >> news:13hfxjlq0xqtq.x3v8evyf4pku$.dlg@40tude.net... >>> On Mon, 2 Jul 2012 23:51:19 -0500, Randy Brukardt wrote: >> ... >>>> Legality has nothing to do with preconditions or postconditions. >>> >>> => It is OK to violate a "contract" defined by these. Here you are. >> >> No, it's not OK; that is the crux of our disagreement. You seem to think >> that the only kind of "contract" is some sort of static thing. > > Exactly. Because the contract exists *before* any programs implementing it > and after them. The contract exists even when there is no such program. > Therefore it cannot depend on the program state. > > Another way to understand this: a contract describes states of a program. > As such it cannot depend on them. That's not my meaning of "contract". It doesn't have anything specific with "program states" (whatever the heck you mean by that -- I can't assume any reasonable interpretation because you make up terminology all the time). > Yet another way: the language of contracts is not the object language: We're not interested in other languages here (this is an Ada forum, after all); Ada is the *only* language worth talking about. So by your definition, nothing you are talking about is even relevant. Why do you bother? (Why do *I* bother? ;-) ... >> But that's never, ever been true in Ada. > > I already said that type constraints are not contracts. E.g. an actual > value of the discriminant does not create a new contract. The contract > covers *all* possible values of the discriminant. > >> Exactly. You claim that there cannot be such a thing as a dynamically >> enforced contract. > > Absolutely. How could you enforce a contract which has been *already* > violated? If a program reaches an illegal state, it is in that state. > Period. Illegal /= Wrong. An illegal state cannot be reached because you can't compile the program. An incorrect state can be reached simply by violating a check or contract. >> But handling exceptions raised for contracts does not make the program >> any >> less wrong; > > Really? What is the purpose of the exercise? Raising exception, rolling > the > stack, finalizing stuff, and so on only to resign that the program is as > wrong as it was before? (Maybe it is even *more* wrong than it was? (:-)) Practicality -- it's not possible to find all program errors before a program is fielded. And a lot of programs cannot fail - so that they have to have a failback position even when they self-detect that they are internally incorrect. It doesn't make the program any less wrong, but it keeps the system up so the plane still can land or you can still retrive files for www.ada-auth.org. But if you *could* have detected the "wrong" program earlier, you surely would have wanted to, so you could have eliminated the incorrect state. A whole lot about programming language design is about practicality and not about ivory tower exercises. Languages which are purely ivory tower exercises rarely have been used off of a college campus. >>>> The only kind of correctness checks that *can* exist in general are >>>> dynamic. >>>> Ada's entire reason to exist is to include checks like range checks and >>>> overflow checks to programs. Without them you get the buffer overflows >>>> and other errors that plague C code. >>> >>> Yes, but irrelevant. These checks are not contract checks, because, >>> otherwise you are in contradiction. No words can change that. >> >> Certainly not if you insist on using an unnecessarily limiting definition >> of >> "contract". > > Yes, the contract as opposed to the implementation limits the former not > to > be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada > 2012 "contracts" are implementations [POV #1]. Do you? No, because I use a very different definition of these terms. Contract is roughly equivalent to (Ada) specification. Implementation is roughly equivalent to (Ada) body. No caller should *ever* depend in any way on "implementation". (Ada screws this up for exceptions and tasking behaviors like blocking and abort.) The only things a caller can depend upon is that which is given in the specification. And that includes both dynamic and static parts. Tools which depend in any way on the contents of Ada bodies (other than the one they are processing) are limiting and violate the philosophy of Ada. Thus we have to get more machine-processable information into the Ada specification, so tools can process calls without having to violate separation by looking at the implementation (that is, the body). ... > The actual fallacy is in pretending that a bug can be handled. You can > handle/be in only anticipated states. Really? That's certainly not true of my web server or many other programs. exception when Err:others => Log_Error (Err); Reset_to_Known_Good_State; The above is that the bottom of most of my tasks. I have no idea what state the task is in when it gets to this handler; it certainly represents an "unanticipated state" in that any state that I actually anticipated has its own handlers and recovery mechanisms. But this handler works to recover the processing in 99% of the cases (good enough for this application); whatever caused the problem is abandoned, and it resets to handle another command. I suppose you'll twist the terminology around in some bizarre way to claim that an unanticipated state - which is the only way to reach this handler - is somehow anticipated simply because I can write a handler for it. That's of course nonsense - whatever I (or any other programmer) thought of is what I anticipated, and there is no way for an outside observer to know anything about those. So you cannot reason about those in any useful way - it's an irrelevant qualifier. >> Right. I recall in the past that you've been unwilling to grasp the idea >> of >> bugs being detected at runtime. > > Sure, because that is rubbish, and always was: > > http://en.wikipedia.org/wiki/Liar_paradox I don't get it. Just because you cannot detect *all* bugs -- that is, that you can't ever make a statement that a program is bug-free -- does not mean that you cannot detect *some* bugs. Indeed, this misguided focus on absolutes has prevented most practical progress in this area. And you're trying hard to prevent progress as well. I'm obviously wasting my time discussing this with you, so I'm done. (If I can resist, I'm surely going to try.) Randy. ... >> [As an aside, this means you do not want real exception contracts, since >> they cannot usefully be done without having it be implementation-defined >> when an exception is raised by a predefined check. The canonical >> semantics >> of Ada would require assuming that every line raises Storage_Error, >> Program_Error, and usually Constraint_Error -- that would make it >> virtually >> impossible to eliminate those exceptions from contracts. > > I don't see it as a big problem. There is a difference between an > obligation to raise exception and a possibility that an exception could be > raised. No one cares about an "obligation to raise an exception"; I can't imagine including those in exception contracts. (Indeed, any such "obligations" should be in the precondition or subtype predicates, so they never even reach the body of the subprogram.) The only contracts of interest are the "possibility that an exception could be raised", as those probably depend on outside effects (user input, file system results, etc.) ... > The vendors could gradually reduce the number of cases where E may be > raised without making clients relying on weaker contracts illegal. The > second cannot be misused to prove that E is raised. It just does not > follow > from the second, and conversely. I don't see this at all. Once you call a routine that has a contract that says "E might be raised", you have to include "E might be raised" in your contract as well. This "poisoning" is the major objection to exception contracts in practice. Moreover, if you have a language-defined check that raises E in a subprogram S, then you have to include the "E might be raised" contract if you have any exception contract at all. That's where the legality comes in. If you allow that contract to be omitted if the compiler can prove that the language-defined check will not fail (and this is common), then you have an implementation-defined legality check. If you *don't* allow that contract to be omitted, then you will have to include such a host of "E might be raised" contracts on every subprogram that no one would ever use the feature. (There are at least 8 common exceptions that could occur in large chunks of my code; and almost no code could be without Constraint_Error, Program_Error, and Storage_Error.) I'm pretty certain that the only useful exception contract would have to allow check elimination to affect legality -- and that's definitely a problem for some. (And they might even be right.) But my feeling is that it would be very valuable to specify that a routine does *not* raise Constraint_Error, and have the compiler verify (or refute) that fact. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 0:43 ` Randy Brukardt @ 2012-07-07 8:06 ` Dmitry A. Kazakov 2012-07-07 11:17 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 8:06 UTC (permalink / raw) On Fri, 6 Jul 2012 19:43:08 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message > news:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net... >> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote: >>> Exactly. You claim that there cannot be such a thing as a dynamically >>> enforced contract. >> >> Absolutely. How could you enforce a contract which has been *already* >> violated? If a program reaches an illegal state, it is in that state. >> Period. > > Illegal /= Wrong. An illegal state cannot be reached because you can't > compile the program. An incorrect state can be reached simply by violating a > check or contract. "violating the contract enforced by the contract check", you should have said. >>> But handling exceptions raised for contracts does not make the program >>> any less wrong; >> >> Really? What is the purpose of the exercise? Raising exception, rolling the >> stack, finalizing stuff, and so on only to resign that the program is as >> wrong as it was before? (Maybe it is even *more* wrong than it was? (:-)) > > Practicality -- it's not possible to find all program errors before a > program is fielded. No practical reasons may do wrong right. I see no practical gain in calling implementations contracts. >>>>> The only kind of correctness checks that *can* exist in general are dynamic. >>>>> Ada's entire reason to exist is to include checks like range checks and >>>>> overflow checks to programs. Without them you get the buffer overflows >>>>> and other errors that plague C code. >>>> >>>> Yes, but irrelevant. These checks are not contract checks, because, >>>> otherwise you are in contradiction. No words can change that. >>> >>> Certainly not if you insist on using an unnecessarily limiting definition of >>> "contract". >> >> Yes, the contract as opposed to the implementation limits the former not to >> be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada >> 2012 "contracts" are implementations [POV #1]. Do you? > > No, because I use a very different definition of these terms. > > Contract is roughly equivalent to (Ada) specification. Implementation is > roughly equivalent to (Ada) body. That does not change anything. There are two kind entities involved A and B. The check may be attributed to either A or B. It is not a question of terminology. >> The actual fallacy is in pretending that a bug can be handled. You can >> handle/be in only anticipated states. > > Really? That's certainly not true of my web server or many other programs. > > exception > when Err:others => > Log_Error (Err); > Reset_to_Known_Good_State; > > The above is that the bottom of most of my tasks. I have no idea what state > the task is in when it gets to this handler; But you have some ideas about the state of the log, about the meaning of the object Err, about the overall state of your program, such that Reset_to_Known_Good_State might work. > I suppose you'll twist the terminology around in some bizarre way to claim > that an unanticipated state - which is the only way to reach this handler - > is somehow anticipated simply because I can write a handler for it. Yes. Merely by the fact that the program continues. Think about it from the angle of preconditions. In ANY state of the program the preconditions of this state are met. You are going to do Log_Error (Err); Reset_to_Known_Good_State; BECAUSE the precondition "some unhandled exception is propagating" is TRUE. (Would you claim that precondition FALSE?) >>> [As an aside, this means you do not want real exception contracts, since >>> they cannot usefully be done without having it be implementation-defined >>> when an exception is raised by a predefined check. The canonical semantics >>> of Ada would require assuming that every line raises Storage_Error, >>> Program_Error, and usually Constraint_Error -- that would make it virtually >>> impossible to eliminate those exceptions from contracts. >> >> I don't see it as a big problem. There is a difference between an >> obligation to raise exception and a possibility that an exception could be >> raised. > > No one cares about an "obligation to raise an exception"; Numeric errors, e.g. overflow and zero-divide must raise. Another important example is when a constructing operation is implemented like: function Create (...) return Boo is begin raise Use_Error; return Boo; end Create; >> The vendors could gradually reduce the number of cases where E may be >> raised without making clients relying on weaker contracts illegal. The >> second cannot be misused to prove that E is raised. It just does not >> follow from the second, and conversely. > > I don't see this at all. Once you call a routine that has a contract that > says "E might be raised", you have to include "E might be raised" in your > contract as well. No. 1. It is always "E might be raised AND Condition." It might be possible to prove not Condition. E.g. x + y might raise Constraint_Error if sum is out of range (or else yield the mathematically correct result). If you can prove x + y in the range, you don't have Constraint_Error. 2. It you cannot prove not Condition, you still can handle E. The main practical purpose of exception contracts is to ensure them handled, rather than attempting to prevent exceptions from being raised. > This "poisoning" is the major objection to exception > contracts in practice. It cannot be otherwise. Any uncertainty about the condition when an exception may appear is necessarily propagates to all clients. This cannot be changed otherwise than by reducing uncertainty: - at the client side, e.g. through 1 or 2. - at the callee's side, e.g. strengthening the condition. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 8:06 ` Dmitry A. Kazakov @ 2012-07-07 11:17 ` Georg Bauhaus 2012-07-07 11:31 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-07 11:17 UTC (permalink / raw) On 07.07.12 10:06, Dmitry A. Kazakov wrote: >> Contract is roughly equivalent to (Ada) specification. Implementation is >> roughly equivalent to (Ada) body. > There are two kind entities involved A and > B. The check may be attributed to either A or B. There is no need for such attribution. Indeed, assertion monitoring (note the word) ideally works like in the following illustration. Monitoring here uses a monitoring processor (not an Ada thing, but a conceptual thing to which an Ada compiler can supply suitable code). Let there be a procedure that adds 42 to its argument (in out) unless adding 42 makes the result too large. Let the argument be passed in r1. add_42: load $2A, r2 # 42 in r2 add r2, r1 # X := X + 42; *return call_add_42: load $0, r1 # X := 0; *call add_42 # Add_42 (X); store r1, (#output) # print X *return The monitor can be turned on or off. The special instructions [X]call and [X]return can be monitored. When monitoring is on, then an auxiliary processor is hooked up to *call and/or *return. It can read all data that the program can read, too. When monitoring, any *call or *return will make the monitor evaluate the corresponding assertions. If they are true, the system continues executing the program. If they are false, the system prints a diagnostic message and stops. If "r1 is too large" means "r1 > 968", then this is the assertion associated with calling add_42. The monitor will test the assertion when "*call add_42" is the next instruction to be performed, and monitoring of calls has been turned on. The point is that the "program proper", i.e. the list of instructions, is the very same irrespective of monitoring assertions. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 11:17 ` Georg Bauhaus @ 2012-07-07 11:31 ` Dmitry A. Kazakov 2012-07-07 12:21 ` Georg Bauhaus 0 siblings, 1 reply; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 11:31 UTC (permalink / raw) On Sat, 07 Jul 2012 13:17:52 +0200, Georg Bauhaus wrote: > On 07.07.12 10:06, Dmitry A. Kazakov wrote: >>> Contract is roughly equivalent to (Ada) specification. Implementation is >>> roughly equivalent to (Ada) body. > >> There are two kind entities involved A and >> B. The check may be attributed to either A or B. > > There is no need for such attribution. Still, it is either A or B. > The point is that the "program proper", i.e. the list of instructions, > is the very same irrespective of monitoring assertions. The program is not a list of instructions. The latter is called "code" of the program. But the error is *very* telling. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 11:31 ` Dmitry A. Kazakov @ 2012-07-07 12:21 ` Georg Bauhaus 2012-07-07 13:03 ` Dmitry A. Kazakov 0 siblings, 1 reply; 125+ messages in thread From: Georg Bauhaus @ 2012-07-07 12:21 UTC (permalink / raw) On 07.07.12 13:31, Dmitry A. Kazakov wrote: >>> There are two kind entities involved A and >>> B. The check may be attributed to either A or B. >> >> There is no need for such attribution. > > Still, it is either A or B. You did notice that monitoring behavior is outside the behavior that the program given will contribute? > The program is not a list of instructions. The latter is called "code" of > the program. The list of instruction is the program that the compiler produces from an Ada program. The program given, the list of instructions, is one in the set of the only programs that can have any effect. > But the error is *very* telling. It's again the dogma versus dogma thing. Still takes time to nail down ... ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-07-07 12:21 ` Georg Bauhaus @ 2012-07-07 13:03 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-07-07 13:03 UTC (permalink / raw) On Sat, 07 Jul 2012 14:21:45 +0200, Georg Bauhaus wrote: > On 07.07.12 13:31, Dmitry A. Kazakov wrote: > >>>> There are two kind entities involved A and >>>> B. The check may be attributed to either A or B. >>> >>> There is no need for such attribution. >> >> Still, it is either A or B. > > You did notice that monitoring behavior is outside the behavior > that the program given will contribute? How exception propagation could be outside the behavior? I gather there is behavior and misbehavior? Dynamic checks must be the second. Now we are on the same page! >> The program is not a list of instructions. The latter is called "code" of >> the program. > > The list of instruction is the program that the compiler produces from > an Ada program. The program given, the list of instructions, is one in > the set of the only programs that can have any effect. > >> But the error is *very* telling. > > It's again the dogma versus dogma thing. It is confusion of program and the semantics thereof. Just like with contracts and implementations. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi 2012-06-20 14:02 ` Georg Bauhaus 2012-06-20 14:13 ` Dmitry A. Kazakov @ 2012-06-20 19:18 ` Anh Vo 2012-06-20 20:16 ` Jeffrey R. Carter 2012-06-21 20:23 ` Randy Brukardt 4 siblings, 0 replies; 125+ messages in thread From: Anh Vo @ 2012-06-20 19:18 UTC (permalink / raw) Cc: nma 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi ` (2 preceding siblings ...) 2012-06-20 19:18 ` Anh Vo @ 2012-06-20 20:16 ` Jeffrey R. Carter 2012-06-20 20:21 ` Jeffrey R. Carter ` (3 more replies) 2012-06-21 20:23 ` Randy Brukardt 4 siblings, 4 replies; 125+ messages in thread From: Jeffrey R. Carter @ 2012-06-20 20:16 UTC (permalink / raw) Cc: nma 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 20:16 ` Jeffrey R. Carter @ 2012-06-20 20:21 ` Jeffrey R. Carter 2012-06-20 20:51 ` Maciej Sobczak ` (2 subsequent siblings) 3 siblings, 0 replies; 125+ messages in thread From: Jeffrey R. Carter @ 2012-06-20 20:21 UTC (permalink / raw) Cc: nma On Wednesday, June 20, 2012 1:16:44 PM UTC-7, Jeffrey R. Carter wrote: > > if Is_Full (S) then > -- stack is full, do something else > else Push (S, Element); > etc... > end if; -- Jeff Carter jrcarter commercial-at-sign acm (period | full stop) org ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 20:16 ` Jeffrey R. Carter 2012-06-20 20:21 ` Jeffrey R. Carter @ 2012-06-20 20:51 ` Maciej Sobczak 2012-06-20 21:04 ` Dmitry A. Kazakov 2012-06-20 22:19 ` Robert A Duff 2012-06-21 20:37 ` Randy Brukardt 3 siblings, 1 reply; 125+ messages in thread From: Maciej Sobczak @ 2012-06-20 20:51 UTC (permalink / raw) Cc: nma 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 20:51 ` Maciej Sobczak @ 2012-06-20 21:04 ` Dmitry A. Kazakov 0 siblings, 0 replies; 125+ messages in thread From: Dmitry A. Kazakov @ 2012-06-20 21:04 UTC (permalink / raw) On Wed, 20 Jun 2012 13:51:32 -0700 (PDT), Maciej Sobczak wrote: > Decades of experience (OK, Java is a bit younger) show that it will usually be used as: > > begin > Push (S, Element); > exception > when others => null; > -- TODO: (errr, it never happens, right?) > end; > > The first version is at least easier to follow in the debugger... Not in Ada where exceptions are not contracted. In Ada one just forgets to catch. Which raises an interesting question: if Ada had contracted exceptions, people would start adding meaningless when others =>. But with contracted exceptions the compiler would know all exceptions possible in the context. We could make others an illegal choice in such cases. The programmer would have to explicitly specify exceptions to catch. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 20:16 ` Jeffrey R. Carter 2012-06-20 20:21 ` Jeffrey R. Carter 2012-06-20 20:51 ` Maciej Sobczak @ 2012-06-20 22:19 ` Robert A Duff 2012-06-21 6:32 ` Georg Bauhaus 2012-06-21 20:37 ` Randy Brukardt 3 siblings, 1 reply; 125+ messages in thread From: Robert A Duff @ 2012-06-20 22:19 UTC (permalink / raw) "Jeffrey R. Carter" <ggsub@pragmada.co.cc> writes: > Any checks worth having during testing are worth having after testing. I say: If you don't need to turn off (at least some) assertions for efficiency reasons, then you probably don't have enough assertions. - Bob ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 22:19 ` Robert A Duff @ 2012-06-21 6:32 ` Georg Bauhaus 0 siblings, 0 replies; 125+ messages in thread From: Georg Bauhaus @ 2012-06-21 6:32 UTC (permalink / raw) On 21.06.12 00:19, Robert A Duff wrote: > "Jeffrey R. Carter"<ggsub@pragmada.co.cc> writes: > >> Any checks worth having during testing are worth having after testing. > > I say: If you don't need to turn off (at least some) assertions for > efficiency reasons, then you probably don't have enough assertions. One measure for "enough assertions" is, I think, when some set of assertions will finally have been shown to be a consequence of the program. What are we testing if this set would still be worth testing, then? ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 20:16 ` Jeffrey R. Carter ` (2 preceding siblings ...) 2012-06-20 22:19 ` Robert A Duff @ 2012-06-21 20:37 ` Randy Brukardt 2012-06-21 20:55 ` Jeffrey Carter 3 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-06-21 20:37 UTC (permalink / raw) "Jeffrey R. Carter" <ggsub@pragmada.co.cc> wrote in message news:4f0d55a9-83e1-44fe-8943-0c73a34a594d@googlegroups.com... ... > Any checks worth having during testing are worth having after testing. > This is why you want a way to ensure they're always done. Right on. > For your own use, the answer is to keep the checks on. The real problem is > for reusable code. > The caller may not be you, and so may have turned off the checks, so such > code should not > have the precondition, but should have the hard-coded checks. "Hard-coded checks" prevent the compiler from doing call-site optimizations and tools from doing much of anything. They should be avoided. The solution is the pragma I showed earlier: pragma Assertion_Policy (Pre => Check, Pre'Class => Check, Static_Predicate => Check, Dynamic_Predicate => Check); put in *every* reusable package spec. They still can suppress the checks by manually deleting the pragma, but it will render command line switches and IDE checkboxes ineffective. And if they do delete the pragma, they've intentionally shot themselves in the foot, and it is no longer your (the package maintainers) problem. (Unless of course they want to spend extra $$$.) Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-21 20:37 ` Randy Brukardt @ 2012-06-21 20:55 ` Jeffrey Carter 2012-06-22 19:15 ` Randy Brukardt 0 siblings, 1 reply; 125+ messages in thread From: Jeffrey Carter @ 2012-06-21 20:55 UTC (permalink / raw) On 06/21/2012 01:37 PM, Randy Brukardt wrote: > > "Hard-coded checks" prevent the compiler from doing call-site optimizations > and tools from doing much of anything. They should be avoided. The solution > is the pragma I showed earlier: > > pragma Assertion_Policy (Pre => Check, > Pre'Class => Check, > Static_Predicate => Check, > Dynamic_Predicate => Check); > > put in *every* reusable package spec. They still can suppress the checks by > manually deleting the pragma, but it will render command line switches and > IDE checkboxes ineffective. And if they do delete the pragma, they've > intentionally shot themselves in the foot, and it is no longer your (the > package maintainers) problem. (Unless of course they want to spend extra > $$$.) Interesting. I wasn't aware of checks that can't be overridden by compiler options, and will be surprised if most compilers don't include a way to override these as well. -- Jeff Carter "Death awaits you all, with nasty, big, pointy teeth!" Monty Python & the Holy Grail 20 --- Posted via news://freenews.netfront.net/ - Complaints to news@netfront.net --- ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-21 20:55 ` Jeffrey Carter @ 2012-06-22 19:15 ` Randy Brukardt 0 siblings, 0 replies; 125+ messages in thread From: Randy Brukardt @ 2012-06-22 19:15 UTC (permalink / raw) "Jeffrey Carter" <spam.jrcarter.not@spam.not.acm.org> wrote in message news:js01ol$76g$1@adenine.netfront.net... > On 06/21/2012 01:37 PM, Randy Brukardt wrote: >> >> "Hard-coded checks" prevent the compiler from doing call-site >> optimizations >> and tools from doing much of anything. They should be avoided. The >> solution >> is the pragma I showed earlier: >> >> pragma Assertion_Policy (Pre => Check, >> Pre'Class => Check, >> Static_Predicate => Check, >> Dynamic_Predicate => Check); >> >> put in *every* reusable package spec. They still can suppress the checks >> by >> manually deleting the pragma, but it will render command line switches >> and >> IDE checkboxes ineffective. And if they do delete the pragma, they've >> intentionally shot themselves in the foot, and it is no longer your (the >> package maintainers) problem. (Unless of course they want to spend extra >> $$$.) > > Interesting. I wasn't aware of checks that can't be overridden by compiler > options, and will be surprised if most compilers don't include a way to > override these as well. A compiler option is essentially equivalent (or should be) to a configuration pragma. Nested pragmas override any outer pragmas (or switches). The same is true for Suppress/Unsuppress. You might be right, but that would be evil in the extreme. This pragma is used in the same way that Unsuppress is used for other checks, and overrriding an explicit Unsuppress would be very, very bad (as it would cause code to malfunction). The same is true here. Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi ` (3 preceding siblings ...) 2012-06-20 20:16 ` Jeffrey R. Carter @ 2012-06-21 20:23 ` Randy Brukardt 2012-06-22 7:34 ` Martin 4 siblings, 1 reply; 125+ messages in thread From: Randy Brukardt @ 2012-06-21 20:23 UTC (permalink / raw) "Nasser M. Abbasi" <nma@12000.org> wrote in message news:jrsjr7$uuo$1@speranza.aioe.org... ... > ----------------------------- > pragma Assertion_Policy(Check); > > procedure Push(S: in out Stack; X: in Item) > with > Pre => not Is_Full(S), > Post => not is Empty(S); > is > .... > end Push; > --------------------- > > One thing to notice right away, is that the pre/post checks > can be disabled or enabled by the pragma. Yes, but this is not a problem if you are careful. Specifically, your packages should at least contain pragma Assertion_Policy (Pre => Check, Pre'Class => Check, Static_Predicate => Check, Dynamic_Predicate => Check); (That is, all of the "inbound" assertion checks.) Then, the only way for someone to ignore these checks is to edit the source code of your library. If they do that, they've clearly "violated the warranty", and you have no obligation to make the body do anything useful if they do that. [Aside: note that assertions are "ignored", not "suppressed". The difference is that suppressed checks can still be made; it is only a permission to the compiler, not a requirement; ignored checks cannot be made.] This was a major topic of the Texas ARG meeting (the last one mainly about Ada 2012), and the above is the solution that we came up with. Note that there was a *lot* of discussion and opinion on this topic. Some people felt that any time someone ignores checks, that the program is erroneous and there ought to be no expectation that it works (if the checks would fail). Others (including me) felt that adding erroneous behavior because you added something that was supposed to make the program safer was nonsensical. ... > So, what is one to do? use pre/post AND also add > an extra check for full stack in the code as before? > does not make sense. Do as above. Force "inbound" checks to always be on (there is no need to leave "post" and "invariant" on, they only can fail due to a bug in your own code, not by anything that the caller can do). Randy. ^ permalink raw reply [flat|nested] 125+ messages in thread
* Re: about the new Ada 2012 pre/post conditions 2012-06-21 20:23 ` Randy Brukardt @ 2012-06-22 7:34 ` Martin 0 siblings, 0 replies; 125+ messages in thread From: Martin @ 2012-06-22 7:34 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 125+ messages in thread
end of thread, other threads:[~2012-07-07 13:32 UTC | newest] Thread overview: 125+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2012-06-20 13:39 about the new Ada 2012 pre/post conditions Nasser M. Abbasi 2012-06-20 14:02 ` Georg Bauhaus 2012-06-20 14:13 ` Dmitry A. Kazakov 2012-06-20 14:24 ` Nasser M. Abbasi 2012-06-20 14:37 ` Dmitry A. Kazakov 2012-06-20 17:02 ` Georg Bauhaus 2012-06-20 18:28 ` Dmitry A. Kazakov 2012-06-21 20:32 ` Randy Brukardt 2012-06-22 7:23 ` Dmitry A. Kazakov 2012-06-22 11:54 ` Georg Bauhaus 2012-06-22 12:39 ` Georg Bauhaus 2012-06-22 12:43 ` Dmitry A. Kazakov 2012-06-22 14:30 ` Georg Bauhaus 2012-06-22 14:36 ` Georg Bauhaus 2012-06-22 15:05 ` Dmitry A. Kazakov 2012-06-22 15:52 ` Georg Bauhaus 2012-06-22 16:35 ` Dmitry A. Kazakov 2012-06-22 16:53 ` Georg Bauhaus 2012-06-22 16:45 ` Georg Bauhaus 2012-06-22 17:24 ` Dmitry A. Kazakov 2012-06-22 19:41 ` Randy Brukardt 2012-06-22 23:08 ` Dmitry A. Kazakov 2012-06-23 10:46 ` Georg Bauhaus 2012-06-23 11:01 ` Dmitry A. Kazakov 2012-06-23 17:46 ` AdaMagica 2012-06-23 19:23 ` Dmitry A. Kazakov 2012-06-24 14:59 ` Georg Bauhaus 2012-06-24 16:06 ` Dmitry A. Kazakov 2012-06-24 19:51 ` Georg Bauhaus 2012-06-25 7:48 ` Dmitry A. Kazakov 2012-06-25 10:10 ` Georg Bauhaus 2012-06-25 8:08 ` Dmitry A. Kazakov 2012-06-25 10:17 ` Georg Bauhaus 2012-06-25 11:54 ` Dmitry A. Kazakov 2012-06-25 12:39 ` Georg Bauhaus 2012-06-25 12:51 ` Georg Bauhaus 2012-06-25 13:19 ` Dmitry A. Kazakov 2012-06-25 16:43 ` Georg Bauhaus 2012-06-25 14:08 ` stefan-lucks 2012-06-25 14:36 ` Dmitry A. Kazakov 2012-06-25 14:37 ` Dmitry A. Kazakov 2012-06-25 16:26 ` stefan-lucks 2012-06-25 19:42 ` Dmitry A. Kazakov 2012-06-26 11:50 ` stefan-lucks 2012-06-26 13:07 ` Dmitry A. Kazakov 2012-06-26 13:49 ` Georg Bauhaus 2012-06-26 14:45 ` Dmitry A. Kazakov 2012-06-26 16:48 ` Georg Bauhaus 2012-06-26 19:43 ` Dmitry A. Kazakov 2012-06-27 8:23 ` Georg Bauhaus 2012-06-27 8:52 ` Dmitry A. Kazakov 2012-06-27 10:30 ` Georg Bauhaus 2012-06-27 12:19 ` Dmitry A. Kazakov 2012-06-27 13:41 ` Nasser M. Abbasi 2012-06-28 7:00 ` Georg Bauhaus 2012-06-27 15:08 ` Georg Bauhaus 2012-06-29 21:03 ` Shark8 2012-06-30 8:26 ` Dmitry A. Kazakov 2012-06-30 12:54 ` Niklas Holsti 2012-07-05 2:58 ` Shark8 2012-07-05 7:24 ` Dmitry A. Kazakov 2012-07-06 6:23 ` Shark8 2012-07-06 7:57 ` Dmitry A. Kazakov 2012-07-07 1:09 ` Randy Brukardt 2012-07-07 8:44 ` Dmitry A. Kazakov 2012-06-26 14:54 ` stefan-lucks 2012-06-26 15:14 ` Dmitry A. Kazakov 2012-07-03 5:28 ` Randy Brukardt 2012-07-03 12:53 ` Dmitry A. Kazakov 2012-07-03 13:48 ` Georg Bauhaus 2012-07-03 14:06 ` Dmitry A. Kazakov 2012-07-03 16:12 ` Georg Bauhaus 2012-07-03 16:45 ` Georg Bauhaus 2012-07-05 1:45 ` Randy Brukardt 2012-07-05 7:48 ` Dmitry A. Kazakov 2012-07-05 19:11 ` Adam Beneschan 2012-07-05 19:55 ` Dmitry A. Kazakov 2012-07-06 7:41 ` Georg Bauhaus 2012-07-06 7:47 ` Georg Bauhaus 2012-07-06 8:05 ` Dmitry A. Kazakov 2012-07-06 8:30 ` Georg Bauhaus 2012-07-06 9:01 ` Dmitry A. Kazakov 2012-07-06 11:33 ` Simon Wright 2012-07-06 13:25 ` Dmitry A. Kazakov 2012-07-06 12:07 ` Georg Bauhaus 2012-07-06 13:37 ` Dmitry A. Kazakov 2012-07-06 16:17 ` Georg Bauhaus 2012-07-06 16:34 ` Georg Bauhaus 2012-07-06 19:18 ` Dmitry A. Kazakov 2012-07-07 1:24 ` Randy Brukardt 2012-07-07 9:09 ` Dmitry A. Kazakov 2012-07-07 1:18 ` Randy Brukardt 2012-07-07 9:14 ` Dmitry A. Kazakov 2012-07-07 12:06 ` Georg Bauhaus 2012-07-07 12:54 ` Dmitry A. Kazakov 2012-07-07 13:31 ` Georg Bauhaus 2012-07-03 5:10 ` Randy Brukardt 2012-07-03 4:51 ` Randy Brukardt 2012-07-03 12:46 ` Dmitry A. Kazakov 2012-07-05 2:18 ` Randy Brukardt 2012-07-05 8:48 ` Dmitry A. Kazakov 2012-07-05 12:07 ` Georg Bauhaus 2012-07-05 12:13 ` Georg Bauhaus 2012-07-05 12:31 ` Dmitry A. Kazakov 2012-07-05 18:16 ` Georg Bauhaus 2012-07-05 19:57 ` Dmitry A. Kazakov 2012-07-06 6:53 ` Georg Bauhaus 2012-07-07 0:43 ` Randy Brukardt 2012-07-07 8:06 ` Dmitry A. Kazakov 2012-07-07 11:17 ` Georg Bauhaus 2012-07-07 11:31 ` Dmitry A. Kazakov 2012-07-07 12:21 ` Georg Bauhaus 2012-07-07 13:03 ` Dmitry A. Kazakov 2012-06-20 19:18 ` Anh Vo 2012-06-20 20:16 ` Jeffrey R. Carter 2012-06-20 20:21 ` Jeffrey R. Carter 2012-06-20 20:51 ` Maciej Sobczak 2012-06-20 21:04 ` Dmitry A. Kazakov 2012-06-20 22:19 ` Robert A Duff 2012-06-21 6:32 ` Georg Bauhaus 2012-06-21 20:37 ` Randy Brukardt 2012-06-21 20:55 ` Jeffrey Carter 2012-06-22 19:15 ` Randy Brukardt 2012-06-21 20:23 ` Randy Brukardt 2012-06-22 7:34 ` Martin
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox