From: "Dan'l Miller" <optikos@verizon.net>
Subject: I'm a noob here.
Date: Mon, 5 May 2014 05:43:50 -0700 (PDT)
Date: 2014-05-05T05:43:50-07:00 [thread overview]
Message-ID: <42945a0c-e4ae-41ff-a2ce-d3faf41336ce@googlegroups.com> (raw)
In-Reply-To: <2c400962-3a09-4da2-9f56-b4f1986b80f8@googlegroups.com>
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?
next prev parent reply other threads:[~2014-05-05 12:43 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 [this message]
2014-05-05 13:52 ` sdalemorrey
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