From: Jacob Sparre Andersen <jacob@jacob-sparre.dk>
Subject: Re: Can I get some code review on some Ada SPARK 2014 code?
Date: Sun, 29 Jan 2017 10:09:00 +0100
Date: 2017-01-29T10:09:00+01:00 [thread overview]
Message-ID: <87inoynsgj.fsf@adaheads.sparre-andersen.dk> (raw)
In-Reply-To: 4c37d9c4-73f0-4a22-8276-8174856cd42e@googlegroups.com
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."
next prev parent reply other threads:[~2017-01-29 9:09 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 [this message]
2017-02-02 4:00 ` stevenselectronicmail
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