SPARK vs PO

--  po.gpr
project PO IS

   for Object_Dir use ".build";

   package Builder is
      for Global_Configuration_Pragmas use "gnat.adc";
   end Builder;

end PO;

--  gnat.adc
pragma Partition_Elaboration_Policy (Sequential);
pragma Profile (Ravenscar);

--  po.ads
package PO
with Spark_Mode => On,
  Abstract_State => State,
  Initializes => State
is

   procedure Set (Value : Integer)
     with Depends => (State =>+ Value);

   procedure Get (Value : out Integer)
     with Depends => (Value => State);

end PO;

--  po.adb
package body PO
with Refined_State => (State => (Protected_Value,
                                 Impl))
is

   Protected_Value : Integer := 0
     with Volatile;

   protected Impl is
      procedure Set (Value : Integer);
      procedure Get (Value : out Integer);
   end Impl;

   procedure Set (Value : Integer) is
   begin
      Impl.Set (Value);
   end Set;

   procedure Get (Value : out Integer) is
   begin
      Impl.Get (Value);
   end Get;

   protected body Impl is
      procedure Set (Value : Integer) is
      begin
         Protected_Value := Value;
      end Set;

      procedure Get (Value : out Integer) is
      begin
         Value := Protected_Value;
      end Get;
   end Impl;

end PO;