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) <= P
{P} repeat A until b {Q and b}
Formula P se numeste specificatie invarianta.
Pentru simplitate, aplicarea acestor reguli in demonstratii se va nota prin:
repeat repeat
{P} {P}
A sau A
{Q} {Q}
until b until b
{Q and b}
Observatie: din prezentarea neformalizata a semanticii, se stie ca instructiumea:
repeat A until b
este echivalenta cu instructiunea compusa:
begin A;
while not b do
A
End
Se poate arata acum, in termenii semanticii axiomantice, ca regula instructiunii repeat poate fi dedusa din regula instructiunii while, regula consecintelor si regula instructiunii compuse. Intr- adevar, in ipostazele {P} A {Q} si (Q and not b) <= P poate fi construita urmatoarea demonstratie:
{P}
begin A;
{Q}
while not b do
{Q}
A
end
{Q and b}.
Regula consecintelor a fost aplicata pentru a demonstra ca specificatia Q este invarianta pentru instructiunea while:
{Q and not b}
{P}
A
{Q}.
Exemplu. Notatia:
Program R1;
Type natural =0..maxint;
Var x, y, z, u : natural
{(x = a) and (y = b) and (a >= 0) and (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 inmultire 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 (b > 0) and (x = a) and (y = b)}
begin
repeat
{(x > 0) and (b > 0) and (x > a) and (y > b)}
while x > y do
{(x > 0) and (y > 0) and ((a, b) = (x, y))}
x := x - y;
while y > x do
{(x > 0) and (y > 0) and ((x, y) and (a, b))}
y := y - x;
{(0 < y <= x) and ((a, b) = (x, y))}
until x = y
{(0 < y <= x) and ((a, b) = (x, y)) and (x = y)}
end.
{x = (a, b)}
