CVS difference for ai12s/ai12-0293-1.txt

Differences between 1.2 and version 1.3
Log of other versions for file ai12s/ai12-0293-1.txt

--- ai12s/ai12-0293-1.txt	2018/12/05 01:52:15	1.2
+++ ai12s/ai12-0293-1.txt	2018/12/05 07:39:08	1.3
@@ -1,4 +1,5 @@
-!standard 13.13.1(9)                                  18-11-28  AI12-0293-1/02
+!standard 13.13.1(1)                                  18-12-04  AI12-0293-1/02
+!standard 13.13.1(9)
 !standard 13.13.1(9.1/1)
 !class Amendment 18-10-14
 !status Amendment 1-2012 18-11-27
@@ -33,14 +34,22 @@
 
 !wording
 
+Add after 13.13.1(1):
+
+   The library package Ada.Streams has the following definition:
+
 Add after 13.13.1(9) (the end of the static semantics section):
+
+   In addition, three packages provide stream implementations which do not make use of any 
+   file operations. These three packages provide the same operations, with Streams.FIFO_Streams 
+   providing an abstract interface, and two child packages providing implementations of that 
+   interface. The difference is that for Streams.FIFO_Streams.Bounded, the maximum storage is
+   bounded.
 
-   The following related units are also declared; they provide
-   stream implementations which do not make use of any file operations.
+   The library package Ada.Streams.FIFO_Streams has the following definition:
 
       package Ada.Streams.FIFO_Streams
-        with Pure, Nonblocking
-      is
+        with Pure, Nonblocking is
          type FIFO_Stream is abstract new Root_Stream_Type with private;
 
          function Element_Count (Stream : FIFO_Stream)
@@ -51,9 +60,10 @@
           ... -- not specified by the language
       end Ada.Streams.FIFO_Streams;
 
+   The library package Ada.Streams.FIFO_Streams.Unbounded has the following definition:
+
       package Ada.Streams.FIFO_Streams.Unbounded
-        with Prelaborated, Nonblocking
-      is
+        with Prelaborated, Nonblocking is
           type Stream_Type is new FIFO_Stream with private
           with Default_Initial_Condition =>
             Element_Count (Stream_Type) = 0;
@@ -64,19 +74,20 @@
              Item   : out Stream_Element_Array;
              Last   : out Stream_Element_Offset)
              with Post =>
-               --  Element_Count decreases by the number of elements read.
-               (Item (Item'First .. Last)'Length =
-                Element_Count (Stream)'Old - Element_Count (Stream))
-
-               and
-
-               --  Number of elements read is minimum of Item'Length and
-               --  number of available items. If that number is 0, then
-               --  Last = Item'First - 1.
-               (if Element_Count (Stream)'Old < Item'Length
-                  then Element_Count (Stream) = 0
-                elsif Item'Length = 0 then Last = Item'First - 1
-                else Last = Item'Last);
+                 (declare
+                   Num_Read : constant Stream_Element_Count :=
+                     Stream_Element_Count'Min 
+                       (Element_Count(Stream)'Old, Item'Length);
+                begin
+                     Last = Num_Read + Item'First - 1
+                   and
+                      Element_Count (Stream) = 
+                         Element_Count (Stream)'Old - Num_Read);
+
+            AARM Discussion: Num_Read is the number of elements read; this is the
+            minimum of Item'Length and the number of available elements. Last
+            then is determined by that, and the Element_Count decreases by the 
+            number of elements read.
 
           overriding
           procedure Write (
@@ -96,17 +107,11 @@
       private
           ... -- not specified by the language
       end Ada.Streams.FIFO_Streams.Unbounded;
+
+   The library package Ada.Streams.FIFO_Streams.Bounded has the following definition:
 
-      package Ada.Streams.FIFO_Streams.Bounded
-        with Pure, Nonblocking
-      is
-         -- The spec for package Bounded is the same as for package
-         -- Unbounded except that it is Pure instead of Preelaborated,
-         -- the Max_Elements discriminant is present, and there is a
-         -- precondition for Write which references that discriminant.
-         -- It is intended that the implementation of Unbounded might
-         -- make use of controlled types and dynamic storage allocation,
-         -- whereas the implementation of Bounded will not.
+     package Ada.Streams.FIFO_Streams.Bounded
+        with Pure, Nonblocking is
 
          type Stream_Type (Max_Elements : Stream_Element_Count)
            is new FIFO_Stream with private
@@ -119,19 +124,15 @@
              Item   : out Stream_Element_Array;
              Last   : out Stream_Element_Offset)
              with Post =>
-               --  Element_Count decreases by the number of elements read.
-               (Item (Item'First .. Last)'Length =
-                Element_Count (Stream)'Old - Element_Count (Stream))
-
-               and
-
-               --  Number of elements read is minimum of Item'Length and
-               --  number of available items. If that number is 0, then
-               --  Last = Item'First - 1.
-               (if Element_Count (Stream)'Old < Item'Length
-                  then Element_Count (Stream) = 0
-                elsif Item'Length = 0 then Last = Item'First - 1
-                else Last = Item'Last);
+                 (declare
+                   Num_Read : constant Stream_Element_Count :=
+                     Stream_Element_Count'Min 
+                       (Element_Count(Stream)'Old, Item'Length);
+                begin
+                     Last = Num_Read + Item'First - 1
+                   and
+                     Element_Count (Stream) = 
+                         Element_Count (Stream)'Old - Num_Read);
 
           overriding
           procedure Write (
@@ -159,7 +160,8 @@
 The Element_Count functions return the number of stream elements
 that are available for reading from the given stream.
 
-The Read and Write procedures behave as described in section 13.13.1.
+The Read and Write procedures behave as described for package 
+Ada.Streams above.
 Stream elements are read in FIFO (first-in, first-out) order; stream
 elements are available for reading immediately after they are written.
 
@@ -172,17 +174,178 @@
 
 Implementation Advice
 
-Bounded.Stream_Type objects should be implemented without implicit pointers or
-dynamic allocation.
+Streams.FIFO_Streams.Bounded.Stream_Type objects should be implemented without
+implicit pointers or dynamic allocation.
 
-  AARM Reason: The FIFO_Streams.Bounded package is provided in order to
-  make available an alternative to the FIFO_Streams.Unbounded
+  AARM Reason: The Streams.FIFO_Streams.Bounded package is provided in orde
+  to make available an alternative to the Streaams.FIFO_Streams.Unbounded
   package which gives more predictable memory usage.
 
 !discussion
 
 None yet.
 
+!corrigendum 13.13.1(1)
+
+@dinsa
+The abstract type Root_Stream_Type is the root type of the class of stream 
+types. The types in this class represent different kinds of streams. A new 
+stream type is defined by extending the root type (or some other stream type), 
+overriding the Read and Write operations, and optionally defining additional 
+primitive subprograms, according to the requirements of the particular kind 
+of stream. The predefined stream-oriented attributes like T'Read and T'Write 
+make dispatching calls on the Read and Write procedures of the 
+Root_Stream_Type. (User-defined T'Read and T'Write attributes can also make 
+such calls, or can call the Read and Write attributes of other types.) 
+@dinst
+The library package Ada.Streams has the following definition:
+
+!corrigendum 13.13.1(9)
+
+@dinsa
+The Write operation appends Item to the specified stream.
+@dinss
+In addition, three packages provide stream implementations which do not make 
+use of any file operations. These three packages provide the same operations,
+with Streams.FIFO_Streams providing an abstract interface, and two child 
+packages providing implementations of that interface. The difference is that 
+for Streams.FIFO_Streams.Bounded, the maximum storage is bounded.
+
+The library package Ada.Streams.FIFO_Streams has the following definition:
+
+@xcode<@b<package> Ada.Streams.FIFO_Streams
+   @b<with> Pure, Nonblocking @b<is>>
+
+@xcode<   @b<type> FIFO_Stream @b<is abstract new> Root_Stream_Type @b<with private>;>
+
+@xcode<   @b<function> Element_Count (Stream : FIFO_Stream)
+      @b<return> Stream_Element_Count @b<is abstract>;>
+
+@xcode<   @b<procedure> Clear (Stream : @b<in out> FIFO_Stream) @b<is abstract>;>
+
+@xcode<@b<private>
+   ... -- @ft<@i<not specified by the language>>
+@b<end> Ada.Streams.FIFO_Streams;>
+
+The library package Ada.Streams.FIFO_Streams.Unbounded has the following 
+definition:
+
+@xcode<@b<package> Ada.Streams.FIFO_Streams.Unbounded
+   @b<with> Prelaborated, Nonblocking @b<is>>
+
+@xcode<   @b<type> Stream_Type @b<is new> FIFO_Stream @b<with private>
+      @b<with> Default_Initial_Condition =@>
+         Element_Count (Stream_Type) = 0;>
+
+@xcode<   @b<overriding>
+   @b<procedure> Read (
+      Stream : @b<in out> Stream_Type;
+      Item   : @b<out> Stream_Element_Array;
+      Last   : @b<out> Stream_Element_Offset)
+      @b<with> Post =@>
+         (@b<declare>
+            Num_Read : @b<constant> Stream_Element_Count :=
+               Stream_Element_Count'Min 
+                  (Element_Count(Stream)'Old, Item'Length);
+          @b<begin>
+                Last = Num_Read + Item'First - 1
+             @b<and>
+                Element_Count (Stream) = 
+                   Element_Count (Stream)'Old - Num_Read);>
+
+@xcode<   @b<overriding>
+   @b<procedure> Write (
+      Stream : @b<in out> Stream_Type;
+      Item   : @b<in> Stream_Element_Array)
+      @b<with> Post =@>
+         Element_Count (Stream) =
+         Element_Count (Stream)'Old + Item'Length;>
+
+@xcode<   @b<overriding>
+   @b<function> Element_Count (Stream : Stream_Type)
+      @b<return> Stream_Element_Count;>
+
+@xcode<   @b<overriding>
+   @b<procedure> Clear (Stream : @b<in out> Stream_Type)
+      @b<with> Post =@> Element_Count (Stream) = 0;>
+
+@xcode<@b<private>
+   ... -- @ft<@i<not specified by the language>>
+@b<end> Ada.Streams.FIFO_Streams.Unbounded;>
+
+The library package Ada.Streams.FIFO_Streams.Bounded has the following
+definition:
+
+@xcode<@b<package> Ada.Streams.FIFO_Streams.Bounded
+   @b<with> Pure, Nonblocking @b<is>>
+
+@xcode<   @b<type> Stream_Type (Max_Elements : Stream_Element_Count) 
+      @b<is new> FIFO_Stream @b<with private>
+         @b<with> Default_Initial_Condition =@>
+            Element_Count (Stream_Type) = 0;>
+
+@xcode<   @b<overriding>
+   @b<procedure> Read (
+      Stream : @b<in out> Stream_Type;
+      Item   : @b<out> Stream_Element_Array;
+      Last   : @b<out> Stream_Element_Offset)
+      @b<with> Post =@>
+         (@b<declare>
+            Num_Read : @b<constant> Stream_Element_Count :=
+               Stream_Element_Count'Min 
+                  (Element_Count(Stream)'Old, Item'Length);
+          @b<begin>
+                Last = Num_Read + Item'First - 1
+             @b<and>
+                Element_Count (Stream) = 
+                   Element_Count (Stream)'Old - Num_Read);>
+
+@xcode<   @b<overriding>
+   @b<procedure> Write (
+      Stream : @b<in out> Stream_Type;
+      Item   : @b<in> Stream_Element_Array)
+      @b<with> Pre =@>
+              Element_Count (Stream) + Item'Length <= Stream.Max_Elements
+              @b<or else> (@b<raise> Constraint_Error),
+           Post =@>
+              Element_Count (Stream) =
+              Element_Count (Stream)'Old + Item'Length;>
+ 
+@xcode<   @b<overriding>
+   @b<function> Element_Count (Stream : Stream_Type)
+      @b<return> Stream_Element_Count
+      @b<with> Post =@> Element_Count'Result <= Stream.Max_Elements;>
+
+@xcode<   @b<overriding>
+   @b<procedure> Clear (Stream : @b<in out> Stream_Type)
+      @b<with> Post =@> Element_Count (Stream) = 0;>
+
+@xcode<@b<private>
+   ... -- @ft<@i<not specified by the language>>
+@b<end> Ada.Streams.FIFO_Streams.Bounded;>
+
+The Element_Count functions return the number of stream elements
+that are available for reading from the given stream.
+
+The Read and Write procedures behave as described for package 
+Ada.Streams above.
+Stream elements are read in FIFO (first-in, first-out) order; stream
+elements are available for reading immediately after they are written.
+
+The Clear procedures remove any available stream elements from the given
+stream.
+
+!corrigendum 13.13.1(9.1/1)
+
+@dinsa
+If Stream_Element'Size is not a multiple of System.Storage_Unit, then the 
+components of Stream_Element_Array need not be aliased. 
+@dinst
+@s8<@i<Implementation Advice>>
+
+Streams.FIFO_Streams.Bounded.Stream_Type objects should be implemented without
+implicit pointers or dynamic allocation.
+
 !ASIS
 
 No changed needed.
@@ -212,3 +375,76 @@
 
 ****************************************************************
 
+From: Randy Brukardt
+Sent: Tuesday, December 4, 2018  11:52 PM
+
+For the record:
+
+I've made various editorial changes to this AI based on conversation with 
+Tucker. To summarize:
+
+(1) We usually start package definitions with "The library package 
+Blah.Blah has the following definition:" This clause defines Ada.Streams 
+and it doesn't include those words or any alternative (the RM does use several
+other wordings, in particular that the package "exists"; this one seems more 
+formal). So, fix that for all four of these packages (including the original 
+one):
+
+Add after 13.13.1(1):
+
+The library package Ada.Streams has the following definition:
+
+
+And introduce each new package separately:
+
+The library package Ada.Streams.FIFO_Streams has the following definition:
+The library package Ada.Streams.FIFO_Streams.Unbounded has the following 
+  definition:
+The library package Ada.Streams.FIFO_Streams.Bounded has the following 
+  definition:
+
+(2) The description of the difference between the Unbounded and Bounded 
+packages is found in a comment (see next item). That's weird; we usually use
+introductory text for that. So the introductory text for these units should 
+discuss the differences between them.
+
+   In addition, three packages provide stream implementations which do not 
+   make use of any file operations. These three packages provide the same 
+   operations, with Streams.FIFO_Streams providing an abstract interface, and 
+   two child packages providing implementations of that interface. The 
+   difference is that for Streams.FIFO_Streams.Bounded, the maximum storage is
+   bounded.
+
+(3) The large comment at the start of Ada.Streams.FIFO_Streams.Bounded is 
+unnecessary. The part about the difference is covered above, and the part 
+about not allowing dynamic allocation is given as Implementation Advice. 
+Thus it is deleted.
+
+(4) I noted that one of the comments in the Post condition as provided by 
+Tucker was in the wrong place (the first comment belongs to the declaration
+expression). Tucker replied that he thought that these comments belong in 
+AARM notes, so I moved them there.
+
+(5) "is" typically is on the same line as the aspects for a package, assuming 
+those aspects are short (which is the case for Boolean aspects like Pure and 
+Nonblocking).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, December 5, 2018  1:01 AM
+
+Got one more:
+
+(6) "The Read and Write procedures behave as described in section 13.13.1."
+
+But we put these packages into 13.13.1! This could be interpreted as a 
+recursive reference.
+
+It would be better to say "The Read and Write procedures behave as described 
+for package Ada.Streams above."
+
+
+P.S. It's not a "section", itís a "subclause". Grumble.
+
+****************************************************************

Questions? Ask the ACAA Technical Agent