Can I get some code review on some Ada SPARK 2014 code?

Can I get some code review on some Ada SPARK 2014 code?

[stevenselectronicmail]

In particular I'm still struggling to get a handle on Abstract_State specifications.

https://gitlab.com/linted/linted/blob/7cd64941f902f08095c1a9326d83004afbe2971b/src/ada-core/src/linted-io_pool.adb

Re: Can I get some code review on some Ada SPARK 2014 code?

[Jacob Sparre Andersen]

stevenselectronicmail@gmail.com writes:

> In particular I'm still struggling to get a handle on Abstract_State
> specifications.

"Abstract_State" indicates names you use to represent package state in a
package specification.

In the package body you then use "Refined_State" to map the abstract
states to actual variables declared inside package.

Section 4.3 in "Building High Integrity Applications with SPARK"
explains it rather well.

Greetings,

Jacob
-- 
"I've got _plenty_ of common sense!"
"I just choose to ignore it."

Re: Can I get some code review on some Ada SPARK 2014 code?

[stevenselectronicmail]

On Sunday, January 29, 2017 at 1:09:02 AM UTC-8, Jacob Sparre Andersen wrote:
> stevenselectronicmail@gmail.com writes:
> 
> > In particular I'm still struggling to get a handle on Abstract_State
> > specifications.
> 
> "Abstract_State" indicates names you use to represent package state in a
> package specification.
> 
> In the package body you then use "Refined_State" to map the abstract
> states to actual variables declared inside package.
> 
> Section 4.3 in "Building High Integrity Applications with SPARK"
> explains it rather well.
> 
> Greetings,
> 
> Jacob
> -- 
> "I've got _plenty_ of common sense!"
> "I just choose to ignore it."

I'll check that book out.

New question.

In Ada SPARK how do I make use of an object composed of multiple protected types?

   type Composed is record
      A : A_Type;
      B : B_Type;
   end record;

if Composed is not Volatile the code does not compile. If Composed is Volatile I cannot pass A and B into subprocedures.

Re: Can I get some code review on some Ada SPARK 2014 code?

[G.B.]

On 02.02.17 05:00, stevenselectronicmail@gmail.com wrote:

> In Ada SPARK how do I make use of an object composed of multiple protected types?
>
>    type Composed is record
>       A : A_Type;
>       B : B_Type;
>    end record;
>
> if Composed is not Volatile the code does not compile. If Composed is Volatile I cannot pass A and B into subprocedures.

If my understanding of earlier editions of SPARK is still correct,
and applies, it is a good idea to imagine tasks and protected objects
as having rather fixed places in SPARK programs.
So, anything that is reminiscent of moving or creating objects
at run-time (dynamically), in local scopes say, or passing those
things around, won't work.  Rethinking might help, for example,
by finding ways to pass the identity of A and B to subprograms.