* Can I get some code review on some Ada SPARK 2014 code?
@ 2017-01-29 0:18 stevenselectronicmail
2017-01-29 9:09 ` Jacob Sparre Andersen
0 siblings, 1 reply; 4+ messages in thread
From: stevenselectronicmail @ 2017-01-29 0:18 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Can I get some code review on some Ada SPARK 2014 code?
2017-01-29 0:18 Can I get some code review on some Ada SPARK 2014 code? stevenselectronicmail
@ 2017-01-29 9:09 ` Jacob Sparre Andersen
2017-02-02 4:00 ` stevenselectronicmail
0 siblings, 1 reply; 4+ messages in thread
From: Jacob Sparre Andersen @ 2017-01-29 9:09 UTC (permalink / raw)
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."
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Can I get some code review on some Ada SPARK 2014 code?
2017-01-29 9:09 ` Jacob Sparre Andersen
@ 2017-02-02 4:00 ` stevenselectronicmail
2017-02-02 11:52 ` G.B.
0 siblings, 1 reply; 4+ messages in thread
From: stevenselectronicmail @ 2017-02-02 4:00 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Can I get some code review on some Ada SPARK 2014 code?
2017-02-02 4:00 ` stevenselectronicmail
@ 2017-02-02 11:52 ` G.B.
0 siblings, 0 replies; 4+ messages in thread
From: G.B. @ 2017-02-02 11:52 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2017-02-02 11:52 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-01-29 0:18 Can I get some code review on some Ada SPARK 2014 code? stevenselectronicmail
2017-01-29 9:09 ` Jacob Sparre Andersen
2017-02-02 4:00 ` stevenselectronicmail
2017-02-02 11:52 ` G.B.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox