From: "Peter C. Chapin" <pcc482719@gmail.com>
Subject: Re: Array initialization in SPARK
Date: Thu, 28 Oct 2010 08:23:19 -0700 (PDT)
Date: 2010-10-28T08:23:19-07:00 [thread overview]
Message-ID: <df8cb993-721d-4b3f-864d-81f20aeeca0c@j18g2000yqd.googlegroups.com> (raw)
In-Reply-To: 3c36d3ba-6748-4aa9-9304-a219b11415bb@30g2000yql.googlegroups.com
On Oct 28, 10:51 am, "Peter C. Chapin" <pcc482...@gmail.com> wrote:
> Thanks for the suggestion. I can see the value of accept here.
I thought of a follow up question...
My understanding is that SPARK assumes there are no flow errors when
creating verification conditions. Thus, in general, if one accepts
certain flow errors would there be a danger that one might
subsequently prove a VC that is not really relevant to the program?
Peter
next prev parent reply other threads:[~2010-10-28 15:23 UTC|newest]
Thread overview: 11+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-10-28 10:13 Array initialization in SPARK Peter C. Chapin
2010-10-28 12:47 ` Phil Thornley
2010-10-28 14:51 ` Peter C. Chapin
2010-10-28 15:23 ` Peter C. Chapin [this message]
2010-10-28 16:26 ` Alexander Senier
2010-10-28 16:38 ` Phil Thornley
2010-10-30 1:04 ` Phil Clayton
2010-10-30 8:10 ` AdaMagica
2010-10-30 13:11 ` Phil Clayton
-- strict thread matches above, loose matches on Subject: below --
2009-06-15 12:01 xorque
2009-06-15 12:10 ` xorque
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox