Информатика и выч. техника \ Информатика

Программа как математический объект: Методические указания для самостоятельного изучения темы и выполнения РГР, страница 29

Верификация программы:

whilecurrent(S) ¹ $ do

      next(S)               od

function

f=(S ¹ $®current(S),S := $, S-|| S+.Æ | истина ® current(S),S := $, S )

program

reset(S)

while current(S) ¹ $ do

      next(S)               od

proof

term

т.к. цепочка ограничена справа символом $,т.е. H- (S+) = $, то мы, читая последовательно по одному символу, в итоге достигнем символа $ и while_test  примет значение false

pass

 while_test = true  ( доказать (p ® f)=(p ® f ° g)

Заметим, что do - часть программы while_doвключает оператор next(S), следовательно, действия оператора  next(S), можно записать, пользуясь списковыми обозначениями, в виде следующей функции:

(S+ ¹ Æ® S, current(S) := S- Å H(S+).T(S+), H-(S-)

фрагмент

 условие

current(S)

         S-

           S+

current(S) ¹ $

 current(S0) ¹ $

current1(S0) = H-(S0-)

S-1 = S-0

 S+1 =  S+0

 next (S)

S+1 ¹ Æ

current2(S1) = H+(S1+)

S-2=S-1ÅH+(S+1)

S+2= T+(S+1)

    f

S2 ¹ $

current3(S2) = $

S-3 = S-2 || S+2

S+3 = Æ

Выводы

          условие:  current(S0) ¹ $ L S+1 ¹ Æ® H(S-0 ¹ $)  L S+0 ¹ Æ ® S-0  ¹ Æ L S+0 ¹ Æ ® S ¹ $

присваивание:

S-3 = S-2 || S+2 ® S-1 ÅH+(S+1) ||  T+(S+1) ® S-0 ÅH+(S+0) ||  T+(S+0) ®

S-0 || H+(S+0) Å T+(S+0) = S-0 || S+0     

S+3 = Æ следовательно S = S-0 || S+0. Æ

current3(S2) = $ т.к. S2 = S-2 || S+2  =  S-1 ÅH+(S+1) ||  T+(S+1) ® S-0 ÅH+(S+0) ||  T+(S+0) = S-0  || H+(S+0) Å T+(S+0) = S-0 || S+0 и  S+3 = Æ , то  S = S-0 || S+0. Æ и current(S-0 || S+0. Æ) = $ , т.к. H-( S+0) = $ по условию задачи.

Pass

while_test = false    Øp ® f = Øp ® I

current(S) = $ ® H-(S-) = $ L S+ = Æ® S = S- || S+ ® S = S- || Æ ® S = S

Pass

resultpass

Определим инвариант данного цикла, используя теорему об инварианте.

       X

  f(X)

  f(X0)

current( S)

$

 $

 S

S- || S+

S-0 || S+0

инварианты:      1. $ = $

2. S = S- || S+ = S-0 || S+0

Первый предикат не представляет интереса, т.к. не характеризует цикл. Второй  предикат характеризует цикл. Данный предикат,  истинен: при входе в цикл, во время выполнения программы и по окончанию цикла. Следовательно, его можно рассматривать, как инвариант данного цикла.

Примеры построения инвариантов приведены в 4.5.1(примеры 1, 2).

5.4 Анализ и структурирование схем – программ

Цели: выработать умения работы со схемами программ: анализ, эквивалентные преобразования, структурирование.

Задания во всех вариантах сформулированы одинаково:

Для заданной схемы:

1)  сделать анализ схемы на структурированность (см. 3.3.6, [12, 4.4, стр. 118]);

2)  построить помеченную структурированную схему;

3)  построить рекурсивную структурированную схему;

4)  описать функцию непоименованного блока;

5)  сделать анализ непоименованного блока:

n  где в блоке нарушен принцип структурированности?

n  как эта проблема решается формальным образом?

n  Можно ли найти решение этой проблемы не формально?

5.4.1  Анализ схемы на структурированность и структурирование непоименованного блока

В заданиях нет полностью структурированных схем, поэтому на этапе анализа (см. 3.3.6) необходимо выделить непоименованный блок, который в дальнейшем и должен быть структурирован. В некоторых случаях может оказаться, что таких блоков несколько, тогда следующие шаги задания можно выполнить для одного из них.

Второй и третий пункты выполняются строго по алгоритмам, приведённым в теореме о структурирование (см. 3.3.3., 3.3.4,[12, 4.4.3, 4.4.4, стр.124, стр.129]). При выполнении четвёртого пункта, используйте правила описания  программных функций. (см.  3.2.4, [12, 4.3.2, стр.112])

Скачать файл