Контрольная работа: Базис стандартной и рекурсивной схемы. Верификация программы

S:=S-F2; {vychitanie iz summy poslednego chisla, kotoroe prevoshodit M}

WriteLn; WriteLn;

WriteLn('O T V E T: Summa etih chisel ravna ', S); ReadLn

END .

Результаты работы Pascal-программы (рис. 5).

Рис. 5

Слабейшие предусловия операторов:

1. начальный оператор - слово вида start(F₀ , F₁ , F₂ ), где F₀ = 1, F₁ = 1,

F₂ - переменные, называемые результатом этого оператора;

2. заключительный оператор - слово вида stop(S), где S = 2 - терм; вхождения переменных в терм S называются аргументами этого оператора;

3. оператор присваивания – F₀ :=1; F₁ :=1; F₂ :=2; S:=4; F₀ :=F₁ , где F₁ =1; F₁ :=F₂ , где F₂ =2; F₂ :=F₀ +F₁ , где F₀ =1, F₁ =1; S:=S+F₂ , где S=4, F₂ =3; S:=S–F₂ , где S=4, F₂ =2;

4. условный оператор (тест) – логическое выражение; F₂ <=M, где F₂ =2,

M>1;

5. оператор петли - односимвольное слово While . Слабейшее предусловие такое же, как в условном операторе .

Задание 4

Разработать алгоритм программы, решающей поставленную задачу;

Составить стандартную схему программы и записать полученную программу в линейной форме (рис. 6);

Используя метод индуктивных утверждений и правила верификации Хоара произвести верификацию программы.

6	Расчет произведения чисел Фибоначчи

Рис. 6

Turbo Pascal

Program ProizFib;

Uses Crt;

Var M, {zadannoe chislo }

F0, F1, F2, {tri posledovatelnyh chisla Fibonachchi}

S : Integer; {summa chisel Fibonachchi}

R : Real; {proizvedenie chisel Fibonachchi}

BEGIN