From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: Array initialization in SPARK
Date: Thu, 28 Oct 2010 09:38:40 -0700 (PDT)
Date: 2010-10-28T09:38:40-07:00 [thread overview]
Message-ID: <eca9714d-6e0e-4c11-8e0a-afca76891e52@t13g2000yqm.googlegroups.com> (raw)
In-Reply-To: 20101028182601.058336d9@senier-offen
On 28 Oct, 17:26, Alexander Senier <m...@senier.net> wrote:
[...]
> It may be benificial to restrict the initialization to simple patterns
> that could be verified (semi-)automatically in the future.
[...]
That's excellent advice.
But if you can't do that, and it really is important to ensure
complete initialization, and you are completing run-time check proofs,
then you could force a check on the array:
--# check for all I in Natural range Out_Matrix'Range(1) =>
--# (for J in Natural range Out_Matrix'Range(2) =>
--# (Out_Matrix(I, J) in Types.Float8));
but, for a complex initialization, completing the proof of this check
will be correspondingly complex :-(
Cheers,
Phil
next prev parent reply other threads:[~2010-10-28 16:38 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
2010-10-28 16:26 ` Alexander Senier
2010-10-28 16:38 ` Phil Thornley [this message]
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