******************************************************* 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:07.29 Line 1 with BasicTypes; 2 3 --# inherit BasicTypes; 4 5 package Time is 6 ------------------------------------------------------------------ 7 -- Time 8 -- 9 -- Description: 10 -- Internal representation of time. 11 -- 12 ----------------------------------------------------------------- 13 type T is private; 14 15 ZeroTime : constant T; 16 17 type YearsT is range 1901 .. 2099; 18 type MonthsT is range 1 .. 12; 19 type DaysT is range 1 .. 31; 20 type HoursT is range 0 .. 23; 21 type MinutesT is range 0 .. 59; 22 ------------------------------------------------------------------ 23 -- Duration 24 -- 25 -- Description: 26 -- Duration in 1/10 seconds. 27 -- The range allows 24 hours to be represented. 28 ------------------------------------------------------------------ 29 type DurationT is range 0 .. 864000; 30 31 ------------------------------------------------------------------ 32 -- Text 33 -- DurationText 34 -- 35 -- Description: 36 -- Textual representation of time used in audit records. 37 -- Times are displayed as "yyyy-mm-dd hh:mm:ss.s" 38 -- Durations are displayed as "hh:mm:ss.s" 39 ------------------------------------------------------------------ 40 subtype TextI is Positive range 1 .. 21; 41 subtype TextT is String (TextI); 42 43 subtype DurationTextI is Positive range 1 .. 10; 44 subtype DurationTextT is String (DurationTextI); 45 46 ------------------------------------------------------------------ 47 -- GreaterThan 48 -- 49 -- Description: 50 -- Boolean function implementing > on T. 51 -- 52 -- Traceunit: C.Clock.GreaterThan 53 -- 54 ------------------------------------------------------------------ 55 56 function GreaterThan (Left, Right : T) return Boolean; 57 58 ------------------------------------------------------------------ 59 -- LessThan 60 -- 61 -- Description: 62 -- Boolean function implementing < on T. 63 -- 64 -- Traceunit: C.Clock.LessThan 65 -- 66 ------------------------------------------------------------------ 67 68 function LessThan (Left, Right : T) return Boolean; 69 70 ------------------------------------------------------------------ 71 -- GreaterThanOrEqual 72 -- 73 -- Description: 74 -- Boolean function implementing >= on T. 75 -- 76 -- Traceunit: C.Clock.GreaterThanOrEqual 77 -- 78 ------------------------------------------------------------------ 79 80 function GreaterThanOrEqual (Left, Right : T) return Boolean; 81 82 ------------------------------------------------------------------ 83 -- LessThanOrEqual 84 -- 85 -- Description: 86 -- Boolean function implementing <= on T. 87 -- 88 -- Traceunit: C.Clock.LessThanOrEqual 89 -- 90 ------------------------------------------------------------------ 91 92 function LessThanOrEqual (Left, Right : T) return Boolean; 93 94 ------------------------------------------------------------------ 95 -- ConstructTime 96 -- 97 -- Description: 98 -- Constructs a time from raw constituent parts. If Time is not 99 -- valid then the Success flag is set to false. 100 -- 101 -- Traceunit: C.Clock.ConstructTime 102 -- 103 104 105 ------------------------------------------------------------------ 106 -- SplitTime 107 -- 108 -- Description: 109 -- Decomposes a time into its constituent parts. 110 -- 111 -- Traceunit: C.Clock.SplitTime 112 -- 113 ------------------------------------------------------------------ 114 procedure SplitTime 115 (TheTime : in T; 116 Year : out YearsT; 117 Month : out MonthsT; 118 Day : out DaysT; 119 Hour : out HoursT; 120 Min : out MinutesT); 121 --# derives Year, 122 --# Month, 123 --# Day, 124 --# Hour, 125 --# Min from TheTime; 126 127 ------------------------------------------------------------------ 128 -- StartOfDay 129 -- 130 -- Description: 131 -- Converts Time to the start of the day. 132 -- 133 -- Traceunit: C.Clock.StartOfDay 134 -- 135 ------------------------------------------------------------------ 136 function StartOfDay (TheTime : T) return T; 137 138 ------------------------------------------------------------------ 139 -- PrintDuration 140 -- 141 -- Description: 142 -- Converts a duration to Text for display. 143 -- 144 -- Traceunit: C.Clock.PrintDuration 145 -- 146 ------------------------------------------------------------------ 147 function PrintDuration (TheDuration : DurationT) return DurationTextT; 148 149 ------------------------------------------------------------------ 150 -- PrintTime 151 -- 152 -- Description: 153 -- Converts a time to Text for display. 154 -- 155 -- Traceunit: C.Clock.PrintText 156 -- 157 ------------------------------------------------------------------ 158 function PrintTime (TheTime : T) return TextT; 159 160 -- ------------------------------------------------------------------ 161 -- -- AddDuration 162 -- -- 163 -- -- Description: 164 -- -- Adds a duration to a time. 165 -- -- 166 -- -- Traceunit: C.Clock.AddDuration 167 -- -- 168 -- ------------------------------------------------------------------ 169 -- function AddDuration 170 -- (TheTime : T; TheDuration : DurationT ) return T; 171 172 private 173 174 MilliSecsInTenthSec : constant := 100; 175 MilliSecsInSec : constant := 1000; 176 177 type MilliSecsT is range 0 .. DurationT'Last * MilliSecsInTenthSec - 1; 178 179 type T is record 180 Year : YearsT; 181 Month : MonthsT; 182 Day : DaysT; 183 MilliSec : MilliSecsT; 184 end record; 185 186 ZeroTime : constant T := 187 T' 188 (Year => YearsT'First, 189 Month => MonthsT'First, 190 Day => DaysT'First, 191 MilliSec => MilliSecsT'First); 192 193 end Time; No summarized warnings --End of file--------------------------------------------------