Re: Hi-Lite high integrity showcase and overflow errors

["yannick.moy" <yannick.moy@gmail.com>]

On Monday, September 3, 2012 11:56:28 PM UTC+2, Georg Bauhaus wrote:
> http://www.open-do.org/projects/hi-lite/a-lighter-introduction-to-hi-lite/
> introduces AdaCore's new proof tools. This introduction makes me worry
> about integrity, pardon me.

This is a natural concern when considering formal verification technology. As leader of the technical developments of GNATprove, I assure you that we always have it in mind.

And you are right on one thing: the code as presented in the "Light Introduction to Hi-Lite" does not fly. This is confirmed by running GNATprove on your code:

alicebob.adb:8:20: info: range check proved
alicebob.adb:8:20: info: overflow check proved
alicebob.adb:10:18: info: range check proved
alicebob.adb:7:13: overflow check not proved

Indeed, the possible overflow in line 7 (the test in Mult) can be raised at run-time, hence the overflow check failure when compiling with -gnato.

You can check these results by downloading GNATprove at http://www.open-do.org/projects/hi-lite/gnatprove/ and running:

$ gnatprove -P test --mode=prove --report=all

(with a simple test.gpr project file setting the language to Ada 2012)

> The high integrity example program fails miserably. (C programmers 
> should have a good laugh.)

You should take this example for what it is: an introduction to a research project. When I wrote this example, GNATprove did not exist. Instead, I used Frama-C and SPARK (and I have given the corresponding annotations). With these annotations, in particular the logical preconditions that X*Y<10000, then you can prove that Mult is safe, and still call Mult in a context where this precondition is not satisfied. One advantage of the new Ada 2012 executable annotations is that you can execute preconditions, which would catch the problem at the caller site.

Now that a prototype for GNATprove is available, you can check that Mult is indeed not safe as written. You can either add a precondition, or change My_Int definition into:
  subtype My_Int is Integer range 0 .. 10_000; 
With this definition, GNATprove now proves all checks in Mult:

alicebob.adb:8:20: info: range check proved
alicebob.adb:8:20: info: overflow check proved
alicebob.adb:10:18: info: range check proved
alicebob.adb:7:13: info: overflow check proved

I have modified the webpage to use this definition of Mult. Note that this verification is dependent on the base type of Mult, so dependent on the target for which you're doing the verification. That's a choice we have made for this technology, because we want to integrate proving and testing, and that requires knowledge of target features.

> So to ask a provocative question, what is the use of all these tools
> if they still lead to programs that overflow so easily?

They don't.

> Or am I just incorrectly assuming thing and X * Y will make the tools
> complain fiercely about possible overflow?

Not fiercely, but in all cases where it cannot prove that it does not overflow, it will issue an error message, yes.