From: sdalemorrey@gmail.com
Subject: Re: I'm a noob here.
Date: Mon, 5 May 2014 06:52:37 -0700 (PDT)
Date: 2014-05-05T06:52:37-07:00 [thread overview]
Message-ID: <c5be2835-dbb0-490d-a484-19c1a252a175@googlegroups.com> (raw)
In-Reply-To: <42945a0c-e4ae-41ff-a2ce-d3faf41336ce@googlegroups.com>
On Monday, May 5, 2014 6:43:50 AM UTC-6, Dan'l Miller wrote:
> In brief, what the OP is asking is: precisely how does a SPARK compiler actually utilize the meta-information annotations? E.g., precisely how does a SPARK compiler make logical inferences regarding correctness of Ada-subset source code to verify that the imperative code does what the annotations have declared?
Well there is that and then there is the more general question of "What is the relationship of Ada to Spark" is one a subset or superset of the other?
Is every valid Spark program a valid Ada program, or is every valid Ada program also a valid Spark program?
Ada documentation seems to be a bit thin, but Spark documentation has been nearly impossible to track down. To my mind this means I'm either asking the question wrong, or asking the wrong question.
A good primer on Spark as well as what tools I would need to see Spark in it's full glory would be a good place for me to start I believe.
next prev parent reply other threads:[~2014-05-05 13:52 UTC|newest]
Thread overview: 13+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-05-05 11:28 I'm a noob here sdalemorrey
2014-05-05 12:43 ` Dan'l Miller
2014-05-05 13:52 ` sdalemorrey [this message]
2014-05-05 13:59 ` roderick.chapman
2014-05-05 16:40 ` G.B.
2014-05-05 16:47 ` G.B.
2014-05-05 17:35 ` Shark8
2014-05-06 10:47 ` Brian Drummond
2014-05-05 13:57 ` roderick.chapman
2014-05-05 17:34 ` Shark8
2014-05-05 17:46 ` Jeffrey Carter
2014-05-05 18:07 ` Nasser M. Abbasi
2014-05-05 19:02 ` Georg Bauhaus
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox