* Puzzled by SPARK global aspect @ 2017-06-30 21:29 digitig 2017-07-01 15:51 ` Anh Vo 0 siblings, 1 reply; 5+ messages in thread From: digitig @ 2017-06-30 21:29 UTC (permalink / raw) Suppose in my package specification I have type Quadrant_Specification_Array is array(Global.Quadrant_X_Index'Range, Global.Quadrant_Y_Index'Range) of Quadrant_Specification; (With QuadrantSpecification being a record type) and in my package body I have: function N_Total_Klingons return Global.Klingon_Counter with Refined_Global => (Input => Quadrant_Specifications) is Total: Global.Klingon_Counter := 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; Spark gives me an error useless refinement, subprogram "N_Total_Klingons" does not depend on abstract state with visible refinement But if I take the Refined_Global specification out I get the error "Quadrant_Specifications" must be listed in the Global aspect of "N_Total_Klingons" I feel I'm losing either way - if I do specify it I'm wrong, if I don't specify it I'm wrong. How *do* I fix this? ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect 2017-06-30 21:29 Puzzled by SPARK global aspect digitig @ 2017-07-01 15:51 ` Anh Vo 2017-07-01 18:25 ` digitig 0 siblings, 1 reply; 5+ messages in thread From: Anh Vo @ 2017-07-01 15:51 UTC (permalink / raw) On Friday, June 30, 2017 at 2:29:38 PM UTC-7, digitig wrote: > Suppose in my package specification I have > > type Quadrant_Specification_Array is > array(Global.Quadrant_X_Index'Range, Global.Quadrant_Y_Index'Range) > of Quadrant_Specification; > > (With QuadrantSpecification being a record type) and in my package body I have: > > function N_Total_Klingons return Global.Klingon_Counter > with > Refined_Global => (Input => Quadrant_Specifications) > is > Total: Global.Klingon_Counter := 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; > > Spark gives me an error > useless refinement, subprogram "N_Total_Klingons" does not depend on abstract state with visible refinement > > But if I take the Refined_Global specification out I get the error > > "Quadrant_Specifications" must be listed in the Global aspect of "N_Total_Klingons" > > I feel I'm losing either way - if I do specify it I'm wrong, if I don't specify it I'm wrong. > > How *do* I fix this? It is pretty hard to suggest advice since it is not a complete minimal code. In addition, I rather see the code instead of guessing. I would say your codes involve package Abstract State aspect. Anh Vo ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect 2017-07-01 15:51 ` Anh Vo @ 2017-07-01 18:25 ` digitig 2017-07-02 0:45 ` Anh Vo 0 siblings, 1 reply; 5+ messages in thread From: digitig @ 2017-07-01 18:25 UTC (permalink / raw) 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: > > Suppose in my package specification I have > > > > type Quadrant_Specification_Array is > > array(Global.Quadrant_X_Index'Range, Global.Quadrant_Y_Index'Range) > > of Quadrant_Specification; > > > > (With QuadrantSpecification being a record type) and in my package body I have: > > > > function N_Total_Klingons return Global.Klingon_Counter > > with > > Refined_Global => (Input => Quadrant_Specifications) > > is > > Total: Global.Klingon_Counter := 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; > > > > Spark gives me an error > > useless refinement, subprogram "N_Total_Klingons" does not depend on abstract state with visible refinement > > > > But if I take the Refined_Global specification out I get the error > > > > "Quadrant_Specifications" must be listed in the Global aspect of "N_Total_Klingons" > > > > I feel I'm losing either way - if I do specify it I'm wrong, if I don't specify it I'm wrong. > > > > How *do* I fix this? > > It is pretty hard to suggest advice since it is not a complete minimal code. In addition, I rather see the code instead of guessing. I would say your codes involve package Abstract State aspect. > > Anh Vo 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; ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect 2017-07-01 18:25 ` digitig @ 2017-07-02 0:45 ` Anh Vo 2017-07-02 0:59 ` Anh Vo 0 siblings, 1 reply; 5+ messages in thread From: Anh Vo @ 2017-07-02 0:45 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Puzzled by SPARK global aspect 2017-07-02 0:45 ` Anh Vo @ 2017-07-02 0:59 ` Anh Vo 0 siblings, 0 replies; 5+ messages in thread From: Anh Vo @ 2017-07-02 0:59 UTC (permalink / raw) 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 -- ... ^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2017-07-02 0:59 UTC | newest] Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 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 is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox