(ПОВЕРНУТИ операнд)
Функції:
В· Висновок () - вивести рядок;
Верифікація
Без розгалуження:
ra = r1
rb = r2
sm = ra - rb
(r1> = r2) {ra = r1; rb = r2; sm = ra - rb} sm <= ra
(r1> = r2) {ra = r1; rb = r2;} ra - rb <= ra
(r1> = r2) {ra = r1} ra - r2 <= ra
(r1> = r2) ГЁ r1 - r2 <= r1
true & true ГЁ true ГЁ true
розгалуженням:
(last == 1)
{ra = r1;}
{ra = 0;}
) ((last = 1)? (last = 0)) & (last = 1) {ra = r1} (ra = r1)? (ra = 0);
((last = 1)? (last = 0)) & (last = 1)? (R1 = r1)? (R1 = 0); & true? true? true.
) ((last = 1)? (last = 0)) & В¬ (last = 1) {ra = 0} (ra = r1)? ( ra = 0);
((last = 1)? (last = 0)) & В¬ (last = 1)? (0 = r1)? (0 = 0); & true? true? true.
Верифікація циклу: = count;
{(...);
... -;
} while (i> 0);
= ((count ГЋ N)? (count = 0)); = (i> 0); = (i = i-1); = (i? 0).
В
((countГЋN)? (count = 0)) & (i? count) {while i> 0 do i = i-1 end} i? 0;
1. Інваріант циклу задовольняється при вході в цикл:
В
((countГЋN)? (count = 0))? (I? Count)? false? true? true
2. Інваріант циклу задовольняється при перевірці умови виконання циклу:
В
(i? count) {(i> 0)} (i? count)
true? true
3. Інваріант циклу задовольняється в тілі циклу:
В
(i? count) & (i> 0) {i = i-1} (i? count)
(i? count) & (i> 0)? (I-1? Count)
(i? count) & (i> 0)? (I? Count +1) & true? true? true
4. Інваріант циклу і заперечення умови виконання имплицируют постусловіем:
В
(i? count) & В¬ (i> 0)? (I? 0)
(i? count) & (i? 0)? (I? 0) & true? true? true
Мережі Петрі
