Re: New to Spark, working an example

[Brad Moore <bmoore.ada@gmail.com>]

On Wednesday, December 19, 2018 at 9:58:44 AM UTC-7, Simon Wright wrote:
> Brad Moore <bmoore.ada@gmail.com> writes:
> 
> > On Sunday, December 16, 2018 at 2:48:19 AM UTC-7, Simon Wright wrote:
> 
> >> util.ads:3:16: medium: overflow check might fail (e.g. when
> >> Floor_Log2'Result = 0)
> 
> > As an aside, it appears the version of gnatprove in GNAT CE 2018 does
> > have a pretty good understanding of exponentiation, given that I was
> > able to get the following proven.
> 
> Apparently so. But the part of gnatprove that gives examples of when the
> assertion might fail is quite misleading: for example,
> 
>    util.ads:7:14: medium: postcondition might fail, cannot prove 2 **
>    Floor_Log2'Result <= X (e.g. when Floor_Log2'Result = 0 and X = 0)
> 
> *when X is Positive* !! and
> 
>    util.adb:19:15: medium: overflow check might fail (e.g. when I = 0)
> 
>    l.18 for I in 1 .. Log_Result'Last loop
>    l.19    if 2 ** I > X then

I agree that the error messages are misleading, as I was getting similar messages when when I was working on this. While the values "0" mentioned in the error messages were confusing to me, I think the messages were helpful at least in suggesting the sort of tests the prover was trying to prove, which ultimately helped me figure out the assertions that were needed to get this to pass. The values given can be a bit of a red herring sometimes, but I think the underlying test described by the message is more helpful. This is my second problem that I attempted to prove in SPARK, so I didn't know if I would succeed, or know much about how to approach this. Its kind of a rewarding feeling when you get the prover to pass.

One suggestion I have to prove post conditions, is to state the post condition as an assert before returning from the subprogram, and work backwards from there.

Brad