From: stevenselectronicmail@gmail.com
Subject: Re: Can I get some code review on some Ada SPARK 2014 code?
Date: Wed, 1 Feb 2017 20:00:38 -0800 (PST)
Date: 2017-02-01T20:00:38-08:00 [thread overview]
Message-ID: <749b6b39-e444-4f6d-8fa1-7958cfcefc25@googlegroups.com> (raw)
In-Reply-To: <87inoynsgj.fsf@adaheads.sparre-andersen.dk>
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.
next prev parent reply other threads:[~2017-02-02 4:00 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
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 [this message]
2017-02-02 11:52 ` G.B.
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox