*******************************************************
                            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--------------------------------------------------