GNATProve - interactions between units

GNATProve - interactions between units

[Maciej Sobczak]

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?

-- 
Maciej Sobczak * http://www.inspirel.com

Re: GNATProve - interactions between units

[Martin]

On Friday, October 23, 2015 at 11:25:21 AM UTC+1, Maciej Sobczak wrote:
> 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?
> 
> -- 
> Maciej Sobczak * http://www.inspirel.com

It may be down to the size of the problem space being analysed. It may have to 'loose' some of the information (i.e. make approximations) that it has room for in the unit analysis. Are there any 'depth of analysis' settings? It may be that you need to crank it up to 11 to ensure a "lossless" analysis and be prepared to wait for potentially very much longer to get results.

This is just a guess (I haven't used GNATProve), but it's a guess based on using other static (semantic) analysis tools for about 15 years now. ;-)

-- Martin

Re: GNATProve - interactions between units

[Maciej Sobczak]

> It may be down to the size of the problem space being analysed.

Interesting idea. I will increase the timeout limit and the max number of proof steps, which seem to be the only tuneable parameters that might be relevant here.

-- 
Maciej Sobczak * http://www.inspirel.com

Re: GNATProve - interactions between units

[Phil Thornley]

> "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 ---