Re: SPARK 2014 and protected objects

[Shark8 <onewingedshark@gmail.com>]

Pragma Ada_2012;
Pragma Profile(Ravenscar);
Pragma Partition_Elaboration_Policy(Sequential);

package PO
with
  Spark_Mode     =>  On,
  Abstract_State => (State with External),
  Initializes    =>  State
is

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

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

private

   protected Impl
     with Part_Of => State
   is
      procedure Set (Value : Integer)
        with Depends => ((Impl =>+ Value));
      procedure Get (Value : out Integer)
        with Depends => (Impl => Impl, Value => Impl);

   private
	Protected_Value : Integer := 0;
   end Impl;
    
    -- GNAT doesn't allow Volatile on the protected object's with.
    Pragma Volatile(Impl);
    
end PO;

-----------------

package body PO
with Spark_Mode => On, Refined_State  => (State => Impl) is

   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;