...structiuni, contrar se trece mai departe.Iata cum arata instructiunea REPEAT prezentata cu ajutorul diagramei de sintaxaINSTRUCbIUNE INSTRUCbIUNEA 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 REPEATAre formaIPS A IQS, Q and not b PIPS repeat A until b IQ and bSFormula P se numeste specificatie invarianta.Pentru simplitate, aplicarea acestor reguli in demonstratii se va nota prin repeat repeat IPS IPSA sau AIQS IQSuntil b until bIQ and bS Observatie din prezentarea neformalizata a semanticii, se stie ca instructiumea repeat A until beste echivalenta cu instructiunea compusa begin A hile not b do A EndSe poate arata acum, in termenii semanticii axiomantice, ca regula instructiunii repeat poate fi dedusa din regula instructiunii hile, regula consecintelor si regula instructiunii compuse. Intr- adevar, in ipostazele IPS A IQS si Q and not b P poate fi construita urmatoarea demonstratie IPS begin A IQS hile not b do IQS A end IQ and bS.Regula consecintelor a fost aplicata pentru a demonstra ca specificatia Q este invarianta pentru instructiunea hileIQ and not bSIPSAIQS.Exemplu. NotatiaProgram R1Type natural 0..maxintVar x, y, z, u naturalIx a and y b and a 0 and b 0SIx y x y and x 0Sbegin z 0 Iz x y x y and x 0S u x repeat Iz u y x y and x 0S z z y Iz u - 1 y x y and u 1S u u - 1 Iz u y x y and u 0S until u 0 Iz u y x y and u 0 and u 0Send. IIz a bSeste o demonstratie a corectitudinii partiale a unui algoritm de inmultire a doua numere naturale prin adunare repetata. Pentru instructiunea repeat until u0, specificatia invarianta este zuyxy and u0.Exemplu. Notatia IProgram R2S type natural 0..maxinitvar x, y naturalIa 0 and b 0 and x a and y bSbegin repeat Ix 0 and b 0 and x a and y bS hile x y do Ix 0 and y 0 and a, b x, yS x x - y hile y x do Ix 0 and y 0 and x, y and a, bS y y - x I0 y x and a, b x, yS until x y I0 y x and a, b x, y and x ySend. Ix a, bSeste o demonstratie a corectitudinii partiale a unui algoritm de calcul al celui mai mare divizor comun a, b a doua numere naturale. In demonstratie s-au mai folosit urmatoarele specificatii adevaratex y x, y x - y, yx, y y, xx, x x.Exemplu. Urmatoarea notatieIprogram R3Stype natural 0..maxintvar x, s, t naturalIx a and y b and a 0 and b 0Sbegin s 0 repeat Is a - x bS t 0 repeat Is a - x b t and y bS s s 1 t t 1 until t y Is a x b t and y b and t yS Is a - x b b x x - 1 Is a - x bS until x 0 I s a - x b and x 0Send.Ix a bSeste o demonstratie a corectitudinii unui algoritm de inmultire a doua numere naturale folosind operatiile succ si pred.Exemplu. Se citeste un numar natural n, mai mare sau egal cu 1. sa se calculeze suma primelor n numere naturale.program sumavar n, s, i integerbegin rite n readln n i 1 s 0 repeat s s i i i 1 until i n ri...
Download