File : a-calend-cert.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT RUN-TIME COMPONENTS --
4 -- --
5 -- A D A . C A L E N D A R --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2004-2015, AdaCore --
10 -- --
11 -- This specification is derived from the Ada Reference Manual for use with --
12 -- GNAT. The copyright notice above, and the license provisions that follow --
13 -- apply solely to the contents of the part following the private keyword. --
14 -- --
15 -- GNAT is free software; you can redistribute it and/or modify it under --
16 -- terms of the GNU General Public License as published by the Free Soft- --
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
21 -- --
22 -- --
23 -- --
24 -- --
25 -- --
26 -- You should have received a copy of the GNU General Public License and --
27 -- a copy of the GCC Runtime Library Exception along with this program; --
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
29 -- <http://www.gnu.org/licenses/>. --
30 -- --
31 -- GNAT was originally developed by the GNAT team at New York University. --
32 -- Extensive contributions were provided by Ada Core Technologies Inc. --
33 -- --
34 ------------------------------------------------------------------------------
35
36 -- This version is for the Cert runtime. It assumes type
37 -- Duration is represented on 64-bits.
38
39 -- RQ 0: Provide the language-defined library package Ada.Calendar.
40
41 -- RQ 1: Provide the specification of the Ada.Calendar package.
42
43 package Ada.Calendar with
44 SPARK_Mode,
45 Abstract_State => (Clock_Time with Synchronous,
46 External => (Async_Readers,
47 Async_Writers)),
48 Initializes => Clock_Time
49 is
50
51 type Time is private;
52 -- RQ 1-1: Time must allow representation of any point in time between
53 -- January 1st 1901 and December 31st 2099 with the precision of at
54 -- least System.Tick seconds.
55 --
56 -- Note: Time type is represented as a Modified Julian Day Number (MJDN).
57 -- MJDN is a number of days elapsed since midnight of November 16th/17th,
58 -- 1858, so day 0 in the system of MJDN is the day 17th November 1858.
59
60 -- Declarations representing limits of allowed local time values. Note that
61 -- these do NOT constrain the possible stored values of time which may well
62 -- permit a larger range of times (this is explicitly allowed in Ada 95).
63
64 subtype Year_Number is Integer range 1901 .. 2099;
65 subtype Month_Number is Integer range 1 .. 12;
66 subtype Day_Number is Integer range 1 .. 31;
67
68 subtype Day_Duration is Duration range 0.0 .. 86_400.0;
69
70 function Clock return Time with
71 Volatile_Function,
72 Global => Clock_Time;
73 -- RQ 2.9: This function shall return the current time in days which
74 -- elapsed since 17'th November 1858.
75
76 function Year (Date : Time) return Year_Number;
77 -- RQ 2.19: This function shall return year of the specified time.
78
79 function Month (Date : Time) return Month_Number;
80 -- RQ 2.11: This function shall return month of the specified time.
81
82 function Day (Date : Time) return Day_Number;
83 -- RQ 2.10: This function shall return day of the specified time.
84
85 function Seconds (Date : Time) return Day_Duration;
86 -- RQ 2.12: This function shall return seconds of the specified time.
87
88 procedure Split
89 (Date : Time;
90 Year : out Year_Number;
91 Month : out Month_Number;
92 Day : out Day_Number;
93 Seconds : out Day_Duration);
94 -- RQ 2.13: This function shall get a Gregorian date (year number, month
95 -- number, day number and duration) corresponding to the specified value
96 -- of the Time type.
97 -- Note: Algorithm used to convert modified Julian day number to Gregorian
98 -- date has been adopted from the one described by the Jean Meeus in
99 -- "Astronomical Algorithms" p. 63-4.
100
101 function Time_Of
102 (Year : Year_Number;
103 Month : Month_Number;
104 Day : Day_Number;
105 Seconds : Day_Duration := 0.0)
106 return Time;
107 -- RQ 2.14: This function shall convert the specified Greogorian date into
108 -- a value of type Time.
109 -- RQ 2.14.1: If the specified values do not represent a valid Gregorian
110 -- calendar date, then raise the Time_Error.
111
112 function "+" (Left : Time; Right : Duration) return Time;
113 -- RQ 2.1: This function shall add the specified duration to the given
114 -- point in time.
115 -- RQ 2.1-1: If the result is not representable in the type Time, then
116 -- raise the Time_Error.
117
118 function "+" (Left : Duration; Right : Time) return Time;
119 -- RQ 2.2: This function shall add the specified duration to the given
120 -- point in time.
121 -- RQ 2.2-1: If the result is not representable in the type Time, then
122 -- raise the Time_Error.
123
124 function "-" (Left : Time; Right : Duration) return Time;
125 -- RQ 2.3: This function shall subtract the specified duration from the
126 -- given point in time.
127 -- RQ 2.3-1: If the result is not representable in the type Time, then
128 -- raise the Time_Error.
129
130 function "-" (Left : Time; Right : Time) return Duration;
131 -- RQ 2.4: This function shall determine the amount of time which elapsed
132 -- since <Left> point in time till <Right>.
133 -- RQ 2.4-1: If the result is not representable in the type Duration, then
134 -- raise the Time_Error.
135
136 function "<" (Left, Right : Time) return Boolean;
137 -- RQ 2.5: This function shall return True if the <Left> point in time is
138 -- before the <Right> point in time, False otherwise.
139
140 function "<=" (Left, Right : Time) return Boolean;
141 -- RQ 2.6: This function shall return True if both times are equal or the
142 -- <Left> point in time is before the <Right> point in time, False
143 -- otherwise.
144
145 function ">" (Left, Right : Time) return Boolean;
146 -- RQ 2.7: This function shall return True if the <Left> point in time is
147 -- after the <Right> point in time, False otherwise.
148
149 function ">=" (Left, Right : Time) return Boolean;
150 -- RQ 2.8: This function shall return True if both times are equal or the
151 -- <Left> point in time is after the <Right> point in time, False
152 -- otherwise.
153
154 Time_Error : exception;
155
156 private
157 pragma SPARK_Mode (Off);
158
159 pragma Inline (Year);
160 pragma Inline (Month);
161 pragma Inline (Day);
162
163 pragma Inline ("<");
164 pragma Inline ("<=");
165 pragma Inline (">");
166 pragma Inline (">=");
167
168 -- Time is represented as a Modified Julian Day number plus fraction of a
169 -- day within the range of dates defined for Ada.Calendar.Time. The small
170 -- of the type preserves the precision of type Duration (64 bits).
171
172 -- We introduce type Modified_Julian_Day so that expressions will be
173 -- cleaner when we want the operations from Standard as opposed to those
174 -- defined in Ada.Calendar on type Time.
175
176 -- The Julian Day approach simplifies Time_Of and Split substantially, as
177 -- well as being well-known algorithms. The use of the Modified Julian Day
178 -- number allows us to preserve the precision of type Duration.
179
180 -- Time zones are not supported in this implementation
181
182 -- Modified Julian Day. The range is exactly that of the dates supported
183 -- within the constraints on the components that make up a date.
184
185 type Constrained_Modified_Julian_Day is delta Duration'Small / 86_400.0
186 range 15_385.0 .. 88_069.0;
187 for Constrained_Modified_Julian_Day'Small use Duration'Small / 86_400.0;
188
189 subtype Modified_Julian_Day is Constrained_Modified_Julian_Day'Base;
190
191 type Time is new Modified_Julian_Day;
192
193 end Ada.Calendar;