******************************************************* Listing of SPARK Text SPARK Examiner GPL Edition, Version 8.1.1, Build Date 20090505, Build 13202 Copyright (C) 2009 Praxis High Integrity Systems Ltd., Bath, U.K. ******************************************************* DATE : 15-APR-2010 10:29:08.32 Line 1 package body Time 2 is 3 4 ------------------------------------------------------------------ 5 -- Types and constants 6 -- 7 ------------------------------------------------------------------ 8 MilliSecsInMin : constant := 60 * MilliSecsInSec; 9 MilliSecsInHr : constant := 60 * MilliSecsInMin; 10 11 ------------------------------------------------------------------ 12 -- Private Operations 13 ------------------------------------------------------------------ 14 15 ------------------------------------------------------------------ 16 -- SetStringSegment 17 -- 18 -- Definition: 19 -- Sets the section of the string S from SStart to SEnd with 20 -- the String representation of the Value. 21 -- Pads to the left with '0'. 22 -- Truncates if Value is too big to fit. 23 -- 24 -- Implementation Notes: 25 -- None. 26 -- 27 ------------------------------------------------------------------ 28 procedure SetStringSegment 29 ( S : in out String; 30 Value : in Natural; 31 SStart : in Positive; 32 SEnd : in Positive) 33 --# derives S from *, 34 --# Value, 35 --# SEnd, 36 --# SStart; 37 --# pre S'Last >= SEnd and S'First <= SStart; 38 is 39 V : Natural; 40 begin 41 42 V := Value; 43 44 for I in reverse Positive range SStart .. SEnd loop 45 --# assert I <= SEnd and I >= SStart 46 --# and I <= S'Last and I >= S'First 47 --# and V in Natural ; 48 S(I) := Character'Val(Character'Pos('0') + (V mod 10)); 49 V := V / 10; 50 end loop; 51 52 end SetStringSegment; +++ Flow analysis of subprogram SetStringSegment performed: no errors found. 53 54 ------------------------------------------------------------------ 55 -- GreaterThan 56 -- 57 -- Implementation Notes: 58 -- None. 59 -- 60 ------------------------------------------------------------------ 61 62 function GreaterThan ( Left, Right : T ) return Boolean 63 is 64 begin 65 return Left.Year > Right.Year 66 or (Left.Year = Right.Year 67 and Left.Month > Right.Month ) 68 or (Left.Year = Right.Year 69 and Left.Month = Right.Month 70 and Left.Day > Right.Day) 71 or (Left.Year = Right.Year 72 and Left.Month = Right.Month 73 and Left.Day = Right.Day 74 and Left.MilliSec > Right.MilliSec); 75 end GreaterThan; +++ Flow analysis of subprogram GreaterThan performed: no errors found. 76 77 ------------------------------------------------------------------ 78 -- LessThan 79 -- 80 -- Implementation Notes: 81 -- None. 82 -- 83 ------------------------------------------------------------------ 84 85 function LessThan ( Left, Right : T ) return Boolean 86 is 87 begin 88 return Left.Year < Right.Year 89 or (Left.Year = Right.Year 90 and Left.Month < Right.Month ) 91 or (Left.Year = Right.Year 92 and Left.Month = Right.Month 93 and Left.Day < Right.Day) 94 or (Left.Year= Right.Year 95 and Left.Month = Right.Month 96 and Left.Day = Right.Day 97 and Left.MilliSec < Right.MilliSec); 98 end LessThan; +++ Flow analysis of subprogram LessThan performed: no errors found. 99 100 ------------------------------------------------------------------ 101 -- GreaterThanOrEqual 102 -- 103 -- Implemention Notes: 104 -- None. 105 -- 106 ------------------------------------------------------------------ 107 108 function GreaterThanOrEqual ( Left, Right : T ) return Boolean 109 is 110 begin 111 return GreaterThan (Left, Right) or Left = Right; 112 end GreaterThanOrEqual; +++ Flow analysis of subprogram GreaterThanOrEqual performed: no errors found. 113 114 ------------------------------------------------------------------ 115 -- LessThanOrEqual 116 -- 117 -- Implemention Notes: 118 -- None. 119 -- 120 ------------------------------------------------------------------ 121 122 function LessThanOrEqual ( Left, Right : T ) return Boolean 123 is 124 begin 125 return LessThan (Left, Right) or Left = Right; 126 end LessThanOrEqual; +++ Flow analysis of subprogram LessThanOrEqual performed: no errors found. 127 128 129 130 ------------------------------------------------------------------ 131 -- SplitTime 132 -- 133 -- Implementation Notes: 134 -- This always rounds down. 135 -- 136 ------------------------------------------------------------------ 137 procedure SplitTime 138 (TheTime : in T; 139 Year : out YearsT; 140 Month : out MonthsT; 141 Day : out DaysT; 142 Hour : out HoursT; 143 Min : out MinutesT) 144 is 145 146 begin 147 Year := TheTime.Year; 148 Month := TheTime.Month; 149 Day := TheTime.Day; 150 Hour := HoursT (TheTime.MilliSec / MilliSecsInHr); 151 Min := MinutesT ((TheTime.MilliSec mod MilliSecsInHr ) 152 / MilliSecsInMin); 153 end SplitTime; +++ Flow analysis of subprogram SplitTime performed: no errors found. 154 155 ------------------------------------------------------------------ 156 -- StartOfDay 157 -- 158 -- Implementation Notes: 159 -- None. 160 -- 161 ------------------------------------------------------------------ 162 function StartOfDay (TheTime : T) return T 163 is 164 begin 165 return T'(Year => TheTime.Year, 166 Month => TheTime.Month, 167 Day => TheTime.Day, 168 MilliSec => MilliSecsT'First); 169 end StartOfDay; +++ Flow analysis of subprogram StartOfDay performed: no errors found. 170 171 172 ------------------------------------------------------------------ 173 -- PrintDuration 174 -- 175 -- Implementation Notes: 176 -- None. 177 -- 178 ------------------------------------------------------------------ 179 function PrintDuration (TheDuration : DurationT ) return DurationTextT 180 is 181 LocalText : DurationTextT := "hh:mm:ss.s"; 182 FirstHourIndex : constant TextI := 1; 183 LastHourIndex : constant TextI := 2; 184 185 FirstMinIndex : constant TextI := 4; 186 LastMinIndex : constant TextI := 5; 187 188 FirstSecIndex : constant TextI := 7; 189 LastSecIndex : constant TextI := 8; 190 191 TenthSecIndex : constant TextI := 10; 192 193 TenthSecsInSec : constant := 10; 194 TenthSecsInMin : constant := 60 * TenthSecsInSec; 195 TenthSecsInHr : constant := 60 * TenthSecsInMin; 196 begin 197 198 SetStringSegment(LocalText, 199 Natural(TheDuration / TenthSecsInHr), 200 FirstHourIndex, 201 LastHourIndex); 202 203 SetStringSegment(LocalText, 204 Natural((TheDuration mod TenthSecsInHr) 205 / TenthSecsInMin), 206 FirstMinIndex, 207 LastMinIndex); 208 209 SetStringSegment(LocalText, 210 Natural((TheDuration mod TenthSecsInMin) 211 / TenthSecsInSec), 212 FirstSecIndex, 213 LastSecIndex); 214 215 SetStringSegment(LocalText, 216 Natural(TheDuration mod TenthSecsInSec), 217 TenthSecIndex, 218 TenthSecIndex); 219 220 return LocalText; 221 end PrintDuration; +++ Flow analysis of subprogram PrintDuration performed: no errors found. 222 223 ------------------------------------------------------------------ 224 -- PrintTime 225 -- 226 -- Implementation Notes: 227 -- None. 228 -- 229 ------------------------------------------------------------------ 230 function PrintTime (TheTime : T ) return TextT 231 is 232 LocalText : TextT := "yyyy-mm-dd hh:mm:ss.s"; 233 234 FirstYearIndex : constant TextI := 1; 235 LastYearIndex : constant TextI := 4; 236 237 FirstMonthIndex : constant TextI := 6; 238 LastMonthIndex : constant TextI := 7; 239 240 FirstDayIndex : constant TextI := 9; 241 LastDayIndex : constant TextI := 10; 242 243 FirstHourIndex : constant TextI := 12; 244 LastHourIndex : constant TextI := 13; 245 246 FirstMinIndex : constant TextI := 15; 247 LastMinIndex : constant TextI := 16; 248 249 FirstSecIndex : constant TextI := 18; 250 LastSecIndex : constant TextI := 19; 251 252 TenthSecIndex : constant TextI := 21; 253 254 begin 255 --# assert LocalText'First = TextI'First and 256 --# LocalText'Last = TextI'Last; 257 258 SetStringSegment(LocalText, 259 Natural(TheTime.Year), 260 FirstYearIndex, 261 LastYearIndex); 262 263 SetStringSegment(LocalText, 264 Natural(TheTime.Month), 265 FirstMonthIndex, 266 LastMonthIndex); 267 268 SetStringSegment(LocalText, 269 Natural(TheTime.Day), 270 FirstDayIndex, 271 LastDayIndex); 272 273 SetStringSegment(LocalText, 274 Natural(TheTime.MilliSec / MilliSecsInHr), 275 FirstHourIndex, 276 LastHourIndex); 277 278 SetStringSegment(LocalText, 279 Natural((TheTime.MilliSec mod MilliSecsInHr) 280 / MilliSecsInMin), 281 FirstMinIndex, 282 LastMinIndex); 283 284 SetStringSegment(LocalText, 285 Natural((TheTime.MilliSec mod MilliSecsInMin) 286 / MilliSecsInSec), 287 FirstSecIndex, 288 LastSecIndex); 289 290 SetStringSegment(LocalText, 291 Natural((TheTime.MilliSec mod MilliSecsInSec) 292 / MilliSecsInTenthSec), 293 TenthSecIndex, 294 TenthSecIndex); 295 296 return LocalText; 297 end PrintTime; +++ Flow analysis of subprogram PrintTime performed: no errors found. 298 299 end Time; No summarized warnings --End of file--------------------------------------------------