IORGA CODRIN
Clasa aXI-a A
REFERAT LA INFORMATICA-
INSTRUCTIUNEA REPEAT

Aceasta instructiune reproduce structura repeat until si are forma generala:
REPEAT
i1;
i2;
. . .
in
UNTIL expresie logica
Aici , i1,…,in reprezinta instructiuni.
Principiul de executare este urmatorul:
Se executa secventa de instructiuni;
Se evalueaza expresia logica;
Daca aceasta ia valoarea FALSE se executa din nou secventa de instructiuni, contrar se trece mai departe.
Iata cum arata instructiunea REPEAT prezentata cu ajutorul diagramei de sintaxa:


INSTRUCTIUNE

 INSTRUCTIUNEA
REPEAT






Observatie: secventa se executa cel putin odata, dupa care se pune problema daca sa se repete sau nu (prin evaluarea expresiei logice).
Regula instructiunii REPEAT
Are forma:
{P} A {Q}, (Q and not b) = 0)}
{(x * y = x * y) and (x > 0)}
begin
z := 0;
{(z + x * y = x * y) and (x > 0)}
u := x;
repeat
{(z + u * y = x * y) and (x > 0)}
z := z + y;
{(z + (u - 1) * y = x * y) and (u >= 1)}
u := u - 1
{(z + u * y = x * y) and (u >= 0)}
until u = 0
{(z + u * y = x * y) and (u >= 0) and (u = 0)}
end.
{{(z = a * b)}

este o demonstratie a corectitudinii partiale a unui algoritm de înmultire a doua numere naturale prin adunare repetata.
Pentru instructiunea repeat…until u=0, specificatia invarianta este (z+u*y=x*y) and (u>0).

Exemplu. Notatia:

{Program R2}
type natural = 0..maxinit;
var x, y : natural;
{(a > 0) and