Version 1.1 of acs/ac-00331.txt

Unformatted version of acs/ac-00331.txt version 1.1
Other versions for file acs/ac-00331.txt

!standard A.5.5(0)          20-09-03 AC95-00331/00
!standard A.5.6(0)
!standard A.5.7(0)
!class Amendment 20-09-03
!status received no action 20-09-03
!status received 20-06-09
!subject Prefix Big_ is incorrect
!summary
!appendix

!topic Calendar.Formatting.Image contract improvements
!reference Ada 202x RM9.6.1(35/2-36/2)
!from Brad Moore 20-06-13
!keywords Calendar Formatting Image Contract
!discussion

The standard package Ada.Calendar.Formatting defines two versions of
an Image function. One that returns the image of a Calendar.Time object,
and one that returns the image of a Duration.

The version that returns the image of a Time value returns a string
in the form, "yyyy-mm-dd hh:mm:ss" or "yyyy-mm-dd hh:mm:ss.mmm",
depending on the value of the parameter Include_Time_Fraction, 
where yyyy is the year in digits, mm is the month, dd is the day, 
hh is hours, mm is minutes, ss is seconds, and mmm is milliseconds.

Similarly, for the version that returns the Image of a Duration, 
the format of the result is in the form, "hh:mm:ss" or "hh:mm:ss.mmm",
depending on the value of the parameter Include_Time_Fraction, where hh
is hours, mm is minues, ss is seconds, and mmm is milliseconds.
For this Image function, the result is implementation defined, if the
Duration is 100 or more hours.

The language defined contracts for these functions currently do not
specify a maximum length of the result as a post condition, nor do they
specify any constraints on the Elapsed_Time Duration parameter.

Now that Ada supports contracts, it would be an improvement if these
functions incorporated these details in their contracts. This can be
particularly helpful for the Image function that converts a Duration
value, since the result can be implementation defined.

A precondition should specify the maximum Duration that the implementation
supports, and any exceptions that might get raised if the input exceeds
that limit. A postcondition should either specify the length of the
result, dependent on the Include_Time_Fraction parameter, and the Duration
value, or at the very least specify the maximum length of the result.

This can be helpful for SPARK programs as well, because currently
concatenating the result to another string fails proof since SPARK
has to assume that the length of the resulting concatenation might
overflow the maximum length for a String. A pragma Assume is needed
to get SPARK to prove this snippet of code.

For example,

   declare
      Result : constant String :=
         Calendar.Formatting.Image
            (Elapsed_Time          => Time_Left,
             Include_Time_Fraction => True);
      pragma Assume (Result'Length <= 12);
   begin
      Put_Line ("Time Left is "  & Result);
   end;

***************************************************************

From: Randy Brukardt
Sent: Tuesday, June 16, 2020  8:34 PM

...
> The language defined contracts for these functions currently do not 
> specify a maximum length of the result as a post condition, nor do 
> they specify any constraints on the Elapsed_Time Duration parameter.
> 
> Now that Ada supports contracts, it would be an improvement if these 
> functions incorporated these details in their contracts. This can be 
> particularly helpful for the Image function that converts a Duration 
> value, since the result can be implementation defined.
...

Could you propose some contracts for these functions? It's not completely
clear from your message what you have in mind. It is getting pretty late in
the Ada 202x work to be adding anything, and a complete proposal that can be
evaluated is a lot more likely to be adopted than a lot of justification 
without a proposal.

Note to the general public: Brad is an ARG member, so it's helpful if he 
provides a proposal with his problem. Everyone should provide a problem 
statement with any proposal that they make. Also, we're not taking new ideas 
for Ada 202x at this point, only refinements like contracts.

***************************************************************

Questions? Ask the ACAA Technical Agent