CVS difference for ai05s/ai05-0145-1.txt

Differences between 1.2 and version 1.3
Log of other versions for file ai05s/ai05-0145-1.txt

--- ai05s/ai05-0145-1.txt	2009/02/17 06:09:17	1.2
+++ ai05s/ai05-0145-1.txt	2009/03/15 03:48:21	1.3
@@ -386,3 +386,230 @@
 I look forward to that, we have always got stuck on invariants :-)
 
 ****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, February 22, 2009  4:51 AM
+
+I'll admit I have been bitten by the syntax bug (thanks, Randy!) for
+pre- and postconditions, and with invariants coming up I suspect it will
+continue.  Here is a general proposal that avoids introducing new reserved words,
+but is quite flexible:
+
+  To specify aspects of an entity (at least "operational" ones)
+  and link them directly to the associated declaration,
+  consider a general syntax of:
+
+   <declaration>
+     WITH
+       <aspect_name> [=> <aspect_value>],
+       <aspect_name> [=> <aspect_value>],
+       ... ;
+
+E.g.:
+
+     function Pop(S : in out Stack) return Elem
+       with
+         Pre => not Is_Empty(S),
+         Post => not Is_Full(S);
+
+     type Even is new Integer
+       with
+         Invariant => Even mod 2 = 0;
+
+     type Atomic_Array is
+       array(Positive range <>) of Natural
+         with
+           Atomic_Components;
+
+     type Set is interface
+       with
+         Invariant'Class =>
+           (Is_Empty(X)) = (Count(X) = 0);
+
+     function Union(X, Y : Set) return Set
+       is abstract with
+         Post'Class =>
+           Count(Union'Result) = Count(X) + Count(Y);
+
+     type R is record
+        X : Positive := 0
+          with Independent;
+        Y : Natural := 77
+          with Atomic;
+     end record;
+
+     type Shared_Bit_Vector is array(0..15) of Boolean
+       with Packing, Independent_Components;
+
+     type Bit_Vector is array(0..15) of Boolean
+       with Component_Size => 1;
+
+[Find the rest of this message in AI05-0147-1.]
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, February 24, 2009  10:25 AM
+
+> I'll admit I have been bitten by the syntax bug (thanks, Randy!) for 
+> pre- and postconditions, and with invariants coming up I suspect it 
+> will continue.  Here is a general proposal that avoids introducing new 
+> reserved words, but is quite
+> flexible:
+> 
+>   To specify aspects of an entity (at least "operational" ones)
+>   and link them directly to the associated declaration,
+>   consider a general syntax of:
+> 
+>    <declaration>
+>      WITH
+>        <aspect_name> [=> <aspect_value>],
+>        <aspect_name> [=> <aspect_value>],
+>        ... ;
+
+I'm not 100% convinced we need syntax (maybe 90%?), but if we do, I definitely
+like this proposal.  Much nicer than adding a whole bunch of special-case
+syntax for all the cases we need, along with the requisite reserved words.
+
+> The notation <aspect_name>'Class was intended to imply an inherited, 
+> non-overridable aspect.
+
+Seems a little bit odd, to me.  I suppose I could get used to it, but I would
+have said "Class_Invariant" rather than "Invariant'Class".
+
+>...The 'Class
+> might be implicit for abstract tagged types and their  primitive 
+>subprograms.
+
+Sounds confusing.  Especially since abstract types can have concrete procedures.
+Make the "'Class" or "Class_" explicit.
+
+[Find the rest of this message in AI05-0147-1.]
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, February 26, 2009  12:09 AM
+
+I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and
+think that pre/post conditions are important enough to warrant syntax additions.
+[What he's agreeing to can be found in AI05-0146-1 - ED]
+
+I do think that postconditions in the body are useful, and so would keep the
+pragmas, certainly in GNAT anyway. It is true that preconditions in the body
+are just assertions, so they are there just for symmetry, but postconditions
+in the body are useful in that they come up front, which is the right position,
+and they block all exits (which would be tedious to do manually with assertions).
+I also think it is good to be able to control pre/post conditions separately
+from normal assertions.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, February 26, 2009  7:34 AM
+
+> postconditions in the body are useful in that they come up front, 
+> which is the right position, and they block all exits (which would be 
+> tedious to do manually with assertions).
+
+It is true that it's useful.  But it's a kludge.  The general problem is that
+there's nowhere to put some code that you want executed on every exit point.
+This solves the problem for the case where that code happens to be an assertion.
+
+But I'm not going to fight against pre/postconditions in bodies.
+
+>... I also think it is good to be able to control  pre/post conditions 
+>separately from normal assertions.
+
+Yes.  Precondition failures should be blamed an on the caller, postcondition
+and invariant failures should be blamed on the callee.  So if you have a
+library, you might have confidence (from testing, and maybe from running
+SofCheck's Inspector) that it works, so you want to turn off postcondition
+and invariant checks, but keep precondition checks on.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, February 27, 2009  11:14 AM
+
+...
+> It is true that it's useful.  But it's a kludge.  The general problem 
+> is that there's nowhere to put some code that you want executed on every exit point.
+> This solves the problem for the case where that code happens to be an 
+> assertion.
+
+I would be happy to have the more general form. As you know the Ada compiler
+internally has a construct AT END:
+
+     begin
+        ...
+     at end
+        ...
+     end;
+
+which is essentially useful for translation of several constructs, and which would
+be indeed be a useful programming construct (it would be amazingly easy to implement
+this in GNAT :-))
+ 
+> But I'm not going to fight against pre/postconditions in bodies.
+> 
+>> ... I also think it is good to be able to control pre/post conditions 
+>> separately from normal assertions.
+> 
+> Yes.  Precondition failures should be blamed an on the caller, 
+> postcondition and invariant failures should be blamed on the callee.  
+> So if you have a library, you might have confidence (from testing, and 
+> maybe from running SofCheck's Inspector) that it works, so you want to 
+> turn off postcondition and invariant checks, but keep precondition checks on.
+
+Right, and that might be independent of assertions (in the case of body postconditions).
+Of course in GNAT you have the nice generalization of pragma Check, which allows you
+to assign a name to an arbitrary group of assertions which can then be controlled as a
+group.
+
+****************************************************************
+
+From: Arnaud Charlet
+Sent: Friday, February 27, 2009  11:21 AM
+
+> I would be happy to have the more general form. As you know the Ada 
+> compiler internally has a construct AT END:
+> 
+>     begin
+>        ...
+>     at end
+>        ...
+>     end;
+> 
+> which is essentially useful for translation of several constructs, and 
+> which would be indeed be a useful programming construct (it would be 
+> amazingly easy to implement this in GNAT :-))
+
+Indeed, and no new reserved word is even needed.
+
+Delphi also has this capability BTW (and if I remember well, it's also
+spelled "at end", or something very close).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, February 27, 2009  12:17 AM
+
+> Indeed, and no new reserved word is even needed.
+
+This is another feature that was proposed as part of Ada 9X, and rejected
+(primarily as a general size-of-change reduction, rather than objections
+to the feature itself).  It was thought that this feature isn't really needed,
+because you can achieve the same thing via finalization, albeit rather verbosely.
+
+I'm not particularly pushing for or against this feature...
+
+> Delphi also has this capability BTW (and if I remember well, it's also 
+> spelled "at end", or something very close).
+
+So does Java: try/finally, and misc other languages.
+
+Java is an interesting case because finalization is so badly broken, so people
+use try/finally fairly heavily.
+
+****************************************************************

Questions? Ask the ACAA Technical Agent