gnatprove_13.2.1_28fc3583/share/examples/spark/gnatprove_by_example/ug__semaphores1/semaphores1.ads

1
2
3
4
5
6
7
8
with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control;
package Semaphores1 with
  SPARK_Mode
is
   Semaphore : Suspension_Object;
   task T1;
   task T2;
end Semaphores1;