From: Anh Vo <anhvofrcaus@gmail.com>
Subject: Re: Puzzled by SPARK global aspect
Date: Sat, 1 Jul 2017 17:59:43 -0700 (PDT)
Date: 2017-07-01T17:59:43-07:00 [thread overview]
Message-ID: <0453e3ad-01e5-4654-b4fa-50b1d14c3e14@googlegroups.com> (raw)
In-Reply-To: <8dd3c359-2486-46a2-9be8-b298659e5e95@googlegroups.com>
On Saturday, July 1, 2017 at 5:45:28 PM UTC-7, Anh Vo wrote:
> On Saturday, July 1, 2017 at 11:25:20 AM UTC-7, digitig wrote:
> > On Saturday, July 1, 2017 at 4:51:22 PM UTC+1, Anh Vo wrote:
> > > On Friday, June 30, 2017 at 2:29:38 PM UTC-7, digitig wrote:
> > Here's a fairly minimal spec and body, then, which gives the problem I describe:
> >
> > ---- main.ads ----
> > package Main
> > with
> > SPARK_Mode => On
> > is
> > type Quadrant_Specification is record
> > N_Klingons: Integer := 0;
> > end record;
> >
> > subtype Klingon_Counter is Integer range 0..20;
> >
> > type Quadrant_Specification_Array is
> > array(1..8, 1..8)
> > of Quadrant_Specification;
> >
> >
> > function N_Total_Klingons return Integer
> > with
> > Global => null,
> > Depends => (N_Total_Klingons'Result => null),
> > Pre => True;
> >
> > end Main;
> >
> > ---- Main.adb ----
> > package body Main
> > with
> > SPARK_Mode => On
> > is
> > Quadrant_Specifications: Quadrant_Specification_Array;
> >
> > function N_Total_Klingons return Integer
> > -- with
> > -- Refined_Global => Quadrant_Specifications
> > is
> > Total: Integer := 0;
> > begin
> > for X in Quadrant_Specifications'Range loop
> > for Y in Quadrant_Specifications'Range(2) loop
> > Total := Total + Quadrant_Specifications(X, Y).N_Klingons;
> > end loop;
> > end loop;
> > return Total;
> > end N_Total_Klingons;
> > end Main;
>
> Both Global and Depends are under umbrella of Abstract_State at the package level. Therefore, Abstract_State must be defined below. Note that Package_State is an arbitrary name.
package Main
with
SPARK_Mode => On, Abstract_State => Package_State
is
--...
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State);
end Main;
In the package body, the Refined_State must be defined to associated with the constituents Quadrant_Specifications as shown below.
> package body Main
> with
> SPARK_Mode => On,
> Refined_State => (Package_State => Quadrant_Specifications)
> is
> -- ...
>
> In addition, Global and Depends are defined below because this function depends on local global variable.
>
> function N_Total_Klingons return Integer
> with
> Global => Package_State,
> Depends => (N_Total_Klingons'Result => Package_State)
> is
> -- ...
>
> In the package body Refined_State must be defined to use Quadrant_Specifications as shown below.
>
> package body Main
> with
> SPARK_Mode => On,
> Refined_State => (Package_State => Quadrant_Specifications)
> is
> -- ...
>
> Moreover, Refined_Global and Refined_Depends aspects must be declared to use the array variable Quadrant_Specifications.
Sorry, I cut out some good part before hitting the send button. Please ignore the previously incomplete post. Below is the complete one.
Both Global and Depends are under umbrella of Abstract_State at the package level. Therefore, Abstract_State must be defined below. Note that Package_State is an arbitrary name.
package Main
with
SPARK_Mode => On, Abstract_State => Package_State
is
--...
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State);
end Main;
In the package body, the Refined_State must be defined to associated with the constituents Quadrant_Specifications as shown below.
package body Main
with
SPARK_Mode => On,
Refined_State => (Package_State => Quadrant_Specifications)
is
-- ...
In addition, Global and Depends are defined below because this function depends on local global variable.
function N_Total_Klingons return Integer
with
Global => Package_State,
Depends => (N_Total_Klingons'Result => Package_State)
is
-- ...
prev parent reply other threads:[~2017-07-02 0:59 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-06-30 21:29 Puzzled by SPARK global aspect digitig
2017-07-01 15:51 ` Anh Vo
2017-07-01 18:25 ` digitig
2017-07-02 0:45 ` Anh Vo
2017-07-02 0:59 ` Anh Vo [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox