From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.129.122.72 with SMTP id v69mr5363424ywc.40.1472602293711;
        Tue, 30 Aug 2016 17:11:33 -0700 (PDT)
X-Received: by 10.157.18.211 with SMTP id g77mr566298otg.19.1472602293667;
 Tue, 30 Aug 2016 17:11:33 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!c52no12037006qte.1!news-out.google.com!b4ni5070iti.0!nntp.google.com!n75no317664ith.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 30 Aug 2016 17:11:33 -0700 (PDT)
In-Reply-To: <ly1t16k0kk.fsf@pushface.org>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=174.28.146.45;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 174.28.146.45
References: <ly1t16k0kk.fsf@pushface.org>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <2a104643-59b9-4a46-b543-5c124984bf43@googlegroups.com>
Subject: Re: SPARK 2014 and protected objects
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Wed, 31 Aug 2016 00:11:33 +0000
Content-Type: text/plain; charset=UTF-8
X-Received-Bytes: 2446
X-Received-Body-CRC: 275166516
Xref: news.eternal-september.org comp.lang.ada:31652
Date: 2016-08-30T17:11:33-07:00
List-Id: <comp.lang.ada>

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;