How to use Assert and loop_invariants

Question

Specification:

package PolyPack with SPARK_Mode is 
type Vector is array (Natural range <>) of Integer;
function RuleHorner (X: Integer; A : Vector) return Integer
with
Pre => A'Length > 0 and A'Last < Integer'Last;
end PolyPack ;

I want to write body of PolyPack package with Assert and loop_invariants that the gnatprove program can prove my function RuleHorner correctness.

I write my function Horner but I don;t know how put assertions and loop_invariants in this program to prove its corectness :

with Ada.Integer_Text_IO;
package body PolyPack with SPARK_Mode is

   function RuleHorner (X: Integer; A : Vector) return Integer is
      Y : Integer := 0;
      begin       
      for I in 0 .. A'Length - 1 loop
         Y := (Y*X) + A(A'Last - I);
      end loop;
      return Y;
      end RuleHorner ;
end PolyPack ;

gnatprove :

overflow check might fail (e.g. when X = 2 and Y = -2)
overflow check might fail

overflow check are for line Y := (Y*X) + A(A'Last - I);

Can someone help me how remove overflow check with loop_invariants

Try running `Rulehorner (1, (Integer'Last, Integer'Last))`; it gives a `Constraint_Error`. — Simon Wright, Mar 09 '19 at 17:00
@Simon Wright Have you any idea how improve specification and body horner_rule with spark to prove all assert? — PoliteMan, Mar 19 '19 at 23:00
What I’m saying is that you *cannot* prove freedom from exceptions as things stand, because there are inputs for which this function *will* raise exceptions! It’s *your* function, you could help yourself by stating what it’s supposed to do, preferably in the form of better preconditions and a postcondition. In English would be a start; I have no idea. — Simon Wright, Mar 20 '19 at 07:55

score 3 · Answer 1 · answered Mar 09 '19 at 04:56

3

The analysis is correct. The element type for type Vector is Integer. When X = 2, Y = -2, and A(A'Last - I) is less than Integer'First + 4 an underflow will occur. How do you think this should be handled in your program? Loop invariants will not work here because you cannot prove that an overflow or underflow cannot occur. Is there a way you can design your types and/or subtypes used within Vector and for variables X and Y to prevent Y from overflowing or underflowing?

I am also curious why you want to ignore the last value in your Vector. Are you trying to walk through the array in reverse? If so simply use the following for loop syntax:

for I in reverse A'Range loop

answered Mar 09 '19 at 04:56

Jim Rogers

4,822
1
11
24

Quite why gnatprove says that X * Y might overflow when X is 2 and Y is -2" I don’t understand. – Simon Wright Mar 09 '19 at 16:58
I don't ignore the last value because it iterates from 0. – PoliteMan Mar 19 '19 at 14:21
@PoliteMan I think Jim is trying to help you simplify your for loop down to something like For E of reverse A loop Y := Y * X + E; end loop; Though he was suggesting the index version of for I in reverse A'Range loop Y := Y * X +A(I); end loop; – Jere Mar 20 '19 at 10:53

How to use Assert and loop_invariants

1 Answers1