From: Anh Vo <anhvofrcaus@gmail.com>
Subject: Re: Puzzled by SPARK global aspect
Date: Sat, 1 Jul 2017 17:45:26 -0700 (PDT)
Date: 2017-07-01T17:45:26-07:00 [thread overview]
Message-ID: <8dd3c359-2486-46a2-9be8-b298659e5e95@googlegroups.com> (raw)
In-Reply-To: <9d8c9cd9-f6b8-4ca3-859e-46f8c1ef019b@googlegroups.com>
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 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.
next prev parent reply other threads:[~2017-07-02 0:45 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 [this message]
2017-07-02 0:59 ` Anh Vo
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox