gnatprove_13.2.1_28fc3583/share/examples/spark/stopwatch/timer.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
with Ada.Real_Time;

with TuningData;
with Display;

package Timer with
  SPARK_Mode,
  Abstract_State => (Control with Synchronous,
                                  External => (Async_Readers,
                                               Async_Writers))
is

   --  We note the resolution of this timing loop is 1 second. So if
   --  you stop the clock after .25 of a second has passed, and then
   --  start it again the display will only updated after an entire
   --  new second has passed.

   task Timer
     with Global => (In_Out => Control,
                     Input => Ada.Real_Time.Clock_Time,
                     Output => Display.LCD),
     Depends => (Display.LCD => Control,
                 Control => Control,
                 null => Ada.Real_Time.Clock_Time),
     Priority => TuningData.TimerPriority;

   procedure StartClock with
     Global  => (In_Out => Control),
     Depends => (Control => Control);

   procedure StopClock with
     Global  => (In_Out => Control),
     Depends => (Control => Control);

end Timer;