gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__semaphores2/semaphores2.ads

1
2
3
4
5
6
7
8
with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;
package Semaphores2 with
  SPARK_Mode
is
   Semaphore1, Semaphore2 : Suspension_Object;
   task T1;
   task T2;
end Semaphores2;