From: Dmitrij Novikov <drr73@gmx.de>
Subject: Re: Proof of array initialization in SPARK 2014
Date: Thu, 12 May 2016 07:43:59 -0700 (PDT)
Date: 2016-05-12T07:43:59-07:00 [thread overview]
Message-ID: <f185d6a5-c91d-4529-8d5e-5abfee0f4687@googlegroups.com> (raw)
In-Reply-To: <ceeb8d7c-d5a2-4720-bee6-a07e34fc5aae@googlegroups.com>
Using the aggregate the array would be initialized twice without being read between the assignments.
I would prefer to use the Annotate pragma or is it considered bad style?
The second problem is that in some cases there might be no suitable post condition. For example when an array is initialized with values from different temperature sensors. So the array elements might have any allowed value. The only thing to prove would be that all elements of the array are covered by the assignment.
next prev parent reply other threads:[~2016-05-12 14:43 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-05-12 12:01 Proof of array initialization in SPARK 2014 Dmitrij Novikov
2016-05-12 12:13 ` ake.ragnar.dahlgren
2016-05-12 14:43 ` Dmitrij Novikov [this message]
2016-05-12 15:47 ` Phil Thornley
2016-05-12 16:58 ` Dmitrij Novikov
2016-05-15 19:42 ` rieachus
2016-05-19 9:30 ` Dmitrij Novikov
2016-05-19 18:12 ` Simon Wright
2016-05-21 2:00 ` rieachus
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox