*******************************************************
                           Listing of SPARK Text
       SPARK95 Examiner with VC and RTC Generator Release 7.3 / 01.06
                           Demonstration Version
          *******************************************************


                       DATE : 24-MAR-2010 12:06:13.35

Line
   1  ------------------------------------------------------------------
   2  -- Tokeneer ID Station Core Software
   3  --
   4  -- Copyright (2003) United States Government, as represented
   5  -- by the Director, National Security Agency. All rights reserved.
   6  --
   7  -- This material was originally developed by Praxis High Integrity
   8  -- Systems Ltd. under contract to the National Security Agency.
   9  ------------------------------------------------------------------
  10  
  11  ------------------------------------------------------------------
  12  -- Clock
  13  --
  14  -- Description:
  15  --    Provides a "current time" for each system cycle.
  16  --
  17  ------------------------------------------------------------------
  18  with BasicTypes;
  19  
  20  -- # inherit Clock.Interface; -- notare lo spazio!
  21  --# inherit BasicTypes;
  22  
  23  package Clock
  24  --# own CurrentTime;
  25  --#     in Now;
  26  is
  27  
  28     ------------------------------------------------------------------
  29     -- Types
  30     --
  31     ------------------------------------------------------------------
  32  
  33     ------------------------------------------------------------------
  34     -- Time
  35     --
  36     -- Description:
  37     --      Internal representation of time.
  38     --
  39     -- Traceunit : C.Clock.Time
  40     -- Traceto : FD.Types.Time
  41     ------------------------------------------------------------------
  42     type TimeT is private;
  43  
  44     ZeroTime : constant TimeT;
  45  
  46     type YearsT      is range 1901 .. 2099;
  47     type MonthsT     is range 1 .. 12;
  48     type DaysT       is range 1 .. 31;
  49     type HoursT      is range 0 .. 23;
  50     type MinutesT    is range 0 .. 59;
  51     ------------------------------------------------------------------
  52     -- Duration
  53     --
  54     -- Description:
  55     --    Duration in 1/10 seconds.
  56     --    The range allows 24 hours to be represented.
  57     ------------------------------------------------------------------
  58     type DurationT is range 0 .. 864000;
  59  
  60     ------------------------------------------------------------------
  61     -- TimeText
  62     -- DurationText
  63     --
  64     -- Description:
  65     --    Textual representation of time used in audit records.
  66     --    Times are displayed as "yyyy-mm-dd hh:mm:ss.s"
  67     --    Durations are displayed as "hh:mm:ss.s"
  68     ------------------------------------------------------------------
  69     subtype TimeTextI is Positive range 1 .. 21;
  70     subtype TimeTextT is String(TimeTextI);
  71  
  72     subtype DurationTextI is Positive range 1 .. 10;
  73     subtype DurationTextT is String(DurationTextI);
  74  
  75     ------------------------------------------------------------------
  76     -- Poll
  77     --
  78     -- Description:
  79     --    Reads the system clock, and updates the internal CurrentTime.
  80     --
  81     -- Traceunit: C.Clock.Poll
  82     -- Traceto: FD.Interface.PollTime
  83     ------------------------------------------------------------------
  84  
  85     procedure Poll;
  86     --# global in     Now;
  87     --#           out CurrentTime;
  88     --# derives CurrentTime from Now;
  89  
  90     ------------------------------------------------------------------
  91     -- TheCurrentTime
  92     --
  93     -- Description:
  94     --    Returns CurrentTime recorded at the last poll.
  95     --
  96     -- Traceunit: C.Clock.TheCurrentTime
  97     -- Traceto: FD.RealWorld.State
  98     ------------------------------------------------------------------
  99  
 100     function TheCurrentTime return TimeT;
 101     --# global CurrentTime;
 102  
 103     ------------------------------------------------------------------
 104     -- GetNow
 105     --
 106     -- Description:
 107     --    Returns the system time now.
 108     --
 109     -- Traceunit: C.Clock.GetNow
 110     -- Traceto: FD.MonitoredRealWorld.State
 111     ------------------------------------------------------------------
 112  
 113     function GetNow return TimeT;
 114     --# global Now;
 115  
 116  
 117     ------------------------------------------------------------------
 118     -- GreaterThan
 119     --
 120     -- Description:
 121     --    Boolean function implementing > on the private Type Time.
 122     --
 123     -- Traceunit: C.Clock.GreaterThan
 124     --
 125     ------------------------------------------------------------------
 126  
 127     function GreaterThan ( Left, Right : TimeT ) return Boolean;
 128  
 129     ------------------------------------------------------------------
 130     -- LessThan
 131     --
 132     -- Description:
 133     --    Boolean function implementing < on the private Type Time.
 134     --
 135     -- Traceunit: C.Clock.LessThan
 136     --
 137     ------------------------------------------------------------------
 138  
 139     function LessThan ( Left, Right : TimeT ) return Boolean;
 140  
 141     ------------------------------------------------------------------
 142     -- GreaterThanOrEqual
 143     --
 144     -- Description:
 145     --    Boolean function implementing >= on the private Type Time.
 146     --
 147     -- Traceunit: C.Clock.GreaterThanOrEqual
 148     --
 149     ------------------------------------------------------------------
 150  
 151     function GreaterThanOrEqual ( Left, Right : TimeT ) return Boolean;
 152  
 153     ------------------------------------------------------------------
 154     -- LessThanOrEqual
 155     --
 156     -- Description:
 157     --    Boolean function implementing <= on the private Type Time.
 158     --
 159     -- Traceunit: C.Clock.LessThanOrEqual
 160     --
 161     ------------------------------------------------------------------
 162  
 163     function LessThanOrEqual ( Left, Right : TimeT ) return Boolean;
 164  
 165     ------------------------------------------------------------------
 166     -- ConstructTime
 167     --
 168     -- Description:
 169     --    Constructs a time from raw constituent parts. If the time is not
 170     --    valid then the Success flag is set to false.
 171     --
 172     -- Traceunit: C.Clock.ConstructTime
 173     --
 174     ------------------------------------------------------------------
 175     procedure ConstructTime
 176       (Year    : in     BasicTypes.Unsigned32T;
 177        Month   : in     BasicTypes.Unsigned32T;
 178        Day     : in     BasicTypes.Unsigned32T;
 179        Hour    : in     BasicTypes.Unsigned32T;
 180        Min     : in     BasicTypes.Unsigned32T;
 181        TheTime :    out TimeT;
 182        Success :    out Boolean);
 183     --# derives TheTime,
 184     --#         Success from Year,
 185     --#                      Month,
 186     --#                      Day,
 187     --#                      Hour,
 188     --#                      Min;
 189  
 190     ------------------------------------------------------------------
 191     -- SplitTime
 192     --
 193     -- Description:
 194     --    Decomposes a time into its constituent parts.
 195     --
 196     -- Traceunit: C.Clock.SplitTime
 197     --
 198     ------------------------------------------------------------------
 199     procedure SplitTime
 200       (TheTime : in     TimeT;
 201        Year    :    out YearsT;
 202        Month   :    out MonthsT;
 203        Day     :    out DaysT;
 204        Hour    :    out HoursT;
 205        Min     :    out MinutesT);
 206     --# derives Year,
 207     --#         Month,
 208     --#         Day,
 209     --#         Hour,
 210     --#         Min   from TheTime;
 211  
 212     ------------------------------------------------------------------
 213     -- StartOfDay
 214     --
 215     -- Description:
 216     --    Converts the time to the start of the day.
 217     --
 218     -- Traceunit: C.Clock.StartOfDay
 219     --
 220     ------------------------------------------------------------------
 221     function StartOfDay (TheTime : TimeT) return TimeT;
 222  
 223     ------------------------------------------------------------------
 224     -- PrintDuration
 225     --
 226     -- Description:
 227     --    Converts a duration to Text for display.
 228     --
 229     -- Traceunit: C.Clock.PrintDuration
 230     --
 231     ------------------------------------------------------------------
 232     function PrintDuration (TheDuration : DurationT ) return DurationTextT;
 233  
 234     ------------------------------------------------------------------
 235     -- PrintTime
 236     --
 237     -- Description:
 238     --    Converts a time to Text for display.
 239     --
 240     -- Traceunit: C.Clock.PrintText
 241     --
 242     ------------------------------------------------------------------
 243     function PrintTime (TheTime : TimeT ) return TimeTextT;
 244  
 245     ------------------------------------------------------------------
 246     -- AddDuration
 247     --
 248     -- Description:
 249     --    Adds a duration to a time.
 250     --
 251     -- Traceunit: C.Clock.AddDuration
 252     --
 253     ------------------------------------------------------------------
 254     function AddDuration
 255       (TheTime : TimeT; TheDuration : DurationT ) return TimeT;
 256  
 257  private
 258  
 259     MilliSecsInTenthSec : constant := 100;
 260     MilliSecsInSec      : constant := 1000;
 261  
 262     type MilliSecsT    is range 0 .. DurationT'Last * MilliSecsInTenthSec - 1 ;
 263  
 264     type TimeT is record
 265        Year      : YearsT;
 266        Month     : MonthsT;
 267        Day       : DaysT;
 268        MilliSec  : MilliSecsT;
 269     end record;
 270  
 271     ZeroTime : constant TimeT :=
 272       TimeT'(Year => YearsT'First,
 273              Month => MonthsT'First,
 274              Day => DaysT'First,
 275              MilliSec => MilliSecsT'First);
 276  
 277  
 278  end Clock;
 279  
 280  
 281  
 282  
 283  
 284  


--End of file--------------------------------------------------