comp.lang.ada
 help / color / mirror / Atom feed
From: "Phil Thornley" <phil.jpthornley@gmail.com>
Subject: Re: GNATProve - interactions between units
Date: Sun, 25 Oct 2015 13:27:40 -0000
Date: 2015-10-25T13:27:40+00:00	[thread overview]
Message-ID: <n0ilcg$1tuh$1@adenine.netfront.net> (raw)
In-Reply-To: <3c3ef412-4a5c-419f-a1c5-ae5e4fe4d0a9@googlegroups.com>



> "Maciej Sobczak"  wrote in message 
> news:3c3ef412-4a5c-419f-a1c5-ae5e4fe4d0a9@googlegroups.com...

> Hi,

> My understanding of SPARK rules is that it is possible to reason about the 
> correctness of the program by proving its units individually and the role 
> of package specifications and subprogram contracts is to isolate units 
> from each other in the sense that it is not necessary to look into other 
> units in order to declare the correctness of the unit being analyzed.

> In other words, we can run GNATProve on each unit separately.

> On the other hand, running GNATProve on all program units allows the tool 
> (apart from reusing the runtime infrastructure of the prover, which 
> amortizes the startup time over many units) to get more information about 
> how units use each other and from this additional information it can 
> discharge more VCs than would be possible otherwise.
> If this is true, then running GNATProve on the whole program should 
> produce the same or *smaller* amount of undischarged VCs.

> I have a project where the opposite can be observed - that is, individual 
> units prove clean, whereas the whole produces warning messages about range 
> checks.

> Is it acceptable to consider this to be a tool bug? Or are there any flaws 
> in my reasoning above and in fact proving units separately is not 
> sufficient for analyzing correctness of the program as a whole?


I will be very surprised if proof of an individual unit uses any information 
about the set of calls of that unit. It was certainly not true for the 
original SPARK and I haven't seen anything about the new version that 
suggests that it has changed.

AFAIK, the only check that uses the whole program is the check that all 
objects are initialised before use.

You can control the operation of GNATProve via the timeout/steps parameter 
and also by the proof strategy - using 'per_check' may fail to prove some 
VCs that are proved by the other strategies (see 6.2.2 of the User Guide).

Cheers,

Phil Thornley 


---
This email has been checked for viruses by Avast antivirus software.
https://www.avast.com/antivirus


--- news://freenews.netfront.net/ - complaints: news@netfront.net ---


      parent reply	other threads:[~2015-10-25 13:27 UTC|newest]

Thread overview: 4+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2015-10-23 10:25 GNATProve - interactions between units Maciej Sobczak
2015-10-24 11:40 ` Martin
2015-10-24 20:07   ` Maciej Sobczak
2015-10-25 13:27 ` Phil Thornley [this message]
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox