gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__synchronous_abstractions/synchronous_abstractions.adb

 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
with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;

package body Synchronous_Abstractions with SPARK_Mode,
  Refined_State => (Synchronous_State => (P,V,S), Normal_State => T)
is
   task T;
   protected P is
      function Read return Natural;
   private
      V : Natural := 0;
   end P;

   S : Suspension_Object;
   V : Natural := 0 with Atomic, Async_Readers, Async_Writers;

   protected body P is
      function Read return Natural is (V);
   end P;

   procedure Do_Something is
   begin
      Suspend_Until_True (S);
   end Do_Something;

   task body T is
      R : Natural := P.Read;
      VV : Natural := V;
   begin
      V := R;
      loop
         null;
      end loop;
   end T;
end Synchronous_Abstractions;