Quelle loop_invariant.adb Sprache: Ada

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;

quality87%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.