src/HOL/SPARK/Manual/document/loop_invariant.adb
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 45044 2fae15f8984d
permissions -rw-r--r--
obsolete;

package body Loop_Invariant
is

   procedure Proc1 (A : in Natural; B : in Word32; C : out Word32)
   is
   begin
      C := 0;
      for I in Natural range 1 .. A
        --# assert Word32 (I - 1) * B = C;
      loop
         C := C + B;
      end loop;
   end Proc1;

   procedure Proc2 (A : in Natural; B : in Word32; C : out Word32)
   is
   begin
      C := 0;
      for I in Natural range 1 .. A
        --# assert Word32 (I - 1) * B = C;
      loop
         C := C + B;
        --# assert Word32 (I) * B = C;
      end loop;
   end Proc2;

end Loop_Invariant;