|
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;
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
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.
|
