(FI.2 = z s B & b s Z & w ’
Ch, FO.1, FI.1, FI.2 := Z, FO.1 s Ch & x s □, FI.1 & x s B & b s Z, w) | (FI.2 = z s B & b s / ’
Ch, FO.1, FI.1, FI.2 := □,FO.1 s Ch & x, FI.1 & x s B & b s /, ††) | (FI.2 = z s / ’
Ch, FO.1, FI.1, FI.2 :=□, FO.1 s Ch & x, FI.1 & x s /, ††)) |

((Ch = ‘ ‘) AND (NOT(EOF(FI))) AND (FI.3 = R) ’

((FI.2 = b s Z & w) AND (FO.3 = W) ’
Ch FO.1, FI.1, FI.2 := Z, FO.1 s □, FI.1 & b s Z, w) | (FI.2 = b s / ’ Ch, FI.1, FI.2 := □, FI.1 & FI.2, ††)) |

((Ch = ‘ ‘) AND (EOF(FI)) AND (FI.3 = R) ’ )

Номера слева идентичны случаям, осуждаемым выше. Эта функция описывает копирование слова из FileIn в FileOut, начинающегося с символа в Ch (в том случае, когда  он не равен пробелу); когда Ch  является пробелом, единственный пробел добавляется к FileOut за исключение случая, при котором курсор в FileIn указывает на конец файла.

В проекте процедуры RemoveExtraBlanks входной и выходной файлы были описаны с использованием нотации Бекуса-Наура. Строки, описываемые нотацией BNF, могут также быть описаны с использованием формальных строковых операций, как это было сделано в определении функции g. Наличие соответствия между этими двумя описаниями помогает понять, как программа решает задачу. В случае 1, нам показывают, что входная строка имеет вид:

s Ch & x s B & b s Z & w

Подчеркнутая последовательность может быть описана в виде BNF так:

<слово> <пробелы> <не пробел>

НЕ нашли? Не то? Что вы ищете?

где <слово> - это непустая строка непробельных символов, <пробелы> - непустая строка □, а <непробел> - это непробельный символ. B & b могут содержать маркеры конца строки, но они будут сконвертированы в пробелы до того, как будут рассмотрены в Ch)

Выходная строка для случая 1 функции g изменяется путем добавления:

s Ch & x s □,

что в нотации BNF представляет собой

<слово> <пробел>

В случае 1, функция g конвертирует строку вида:

<слово> <пробелы> <не пробел>,

в строку вида:

<слово> <пробел> <не пробел>.

Аналогичным способом  запишем в виде BNF оставшиеся случачаи:

Нотация Бекуса-Наура части DO функции g

Случай

Ch, FileIn

FileOut

Ch

EOF

1

<слово><пробелы><непробел>

<слово> <пробел>

<непробел>

FALSE

4

<слово> <пробелы>

<слово>

<пробел>

TRUE

6

<слово> <пробел>

<слово>

<пробел>

TRUE

7

<пробелы> <непробел>

<пробел>

<непробел>

FALSE

10

<пробелы>

<пустая строка>

<пробел>

TRUE

12

<пробел>

<пустая строка>

<пробел>

TRUE

Часть DO оператора WHILE в процедуре RemoveExtraBlanks содержит функцию g, описанную выше. BNF  - таблица, описывающая g помогает в понимании итераций цикла. Оператор WHILE такой:

WHILE NOT EOF(FileIn)

DO

  {Вычислить g}

Любой из шести образцов может возникнуть на входе и g произведет соответствующий образец на выходе, подготовившись к приему следующего образца, пока на входе не будет встречен конец файла.

Используя таблицу может бать записано BNF-описание файлов, обрабатываемых оператором WHILE. Как только встретится <непробел> в Ch и части FileIn, данный образец может повториться. Пусть <R> обозначает вовлеченную строку. Только случаи 1 и 4 вовлекаются, поскольку только они начинаются со <слова>, которое начинает <непробел>. (Случай 6 является менее общей версией случая 4). Таким образом, рекурсивное правило будет таким:

<R> ::= <слово> <пробелы> <R>        (1)

               | <слово> <пробелы>                (4)

Случаи 7 и 10 могут быть применены только изначально, поскольку они требуют, чтобы в Ch находился пробел, и ни одного случая не приводит к этой ситуации – все они приводят к появлению пробела в Ch лишь в конце файла, при котором происходит прекращение оператора WHILE:

<Файл1> ::= <слово> <пробелы> <R>        (1)

               |<слово> <пробелы>                        (4)

               |<пробелы> <R>                        (7)

               |<пробелы>                                (10)

Случай 12 является менее общей версией случая 10.

Можно заметить что первые 2 альтернативы являются <R>, поэтому:

<Файл1> ::= <R>                (1, 4)

               |<пробелы> <R>        (7)

               |<пробелы>                (10)

Выходной файл, создаваемый программой может быть описан в форме BNF для <Файл2> подобным образом. Случаи 4 и 6 являются дубликатами, как 10 и 12. Повторение может возникнуть в случаях 1 и 4, как и раньше, приводя нас к строкам <S>:

<S> ::= <слово> <пробел> <S>        (1)

               | <слово>                        (4)

Остальные случаи могут возникнуть только изначально:

<Файл2> ::= <слово> <пробел> <S>        (1)

               | <слово>                        (4)

               | <пробел> S                        (7)

               | <пустая строка>                (10)

Путем замены первых двух альтернатив на S получаем:

<Файл2> ::= <S>                        (1, 4)

               | <пробел> S                        (7)

               | <пустая строка>                (10)

Очевидно из таблицы для функции g, что <слова> из <Файла1> перемещаются в <Файл2> в том же порядке, в котором появляются. Таким образом, функция f цикла WHILE конвертирует <Файл1> в <Файл2>, приготовляя порядок <слов> в том случае, если EOF(FileIn) равен FALSE, и идентична в противном случае, т. е:

f = ((NOT(EOF(FileIn)) AND FIleIn.3=R AND FIleOuot.3=W) ’

       FileIn, FileOut := <FileIn.1 & FileIn.2, ††. R>,

               <FileOut.1 & convert(FileIn.2), ††, W>) |

       (EOF(FileIn)) AND FileIn.3 = R ’ )

где convert принимает в качестве аргумента строку в виде <Файл1> и производит строку в виде <Файл2>, причем слова и их порядок не изменяются.

Формальное доказательство того, что функция f является функцией выполняемой оператором WHILE, дано не будет, но три условия правила проверки WHILE будут обсуждены неформально.

domain(f) = domain( WHILE... ) (EOF(FileIn) ’ f) = (EOF(FileIn) ’ ) f  = IF NOT EOF(FileIn) THEN {вычислить g} ◦ f

Задание 5. Покажите справедливость правил 1-3 самостоятельно

(30 баллов)

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

Программный анализ заставляет использовать множество различных формализмов. Этот пример использует строковую нотацию и нотацию Бекуса-Наура, а также условные присваивания и трассировочные таблицы. Формализмы были придуманы для того, чтобы сделать задачу сложного анализа проще. Новые формализмы могут быть придуманы для решения других задач.

Задание 6. Предположим, что на входе RemoveExtraBlanks дан файл, который состоит из более чем одной строки. Объясните подробно, что произойдет на границах строк.

(10 баллов)

Задание 7. Измените проект RemoveExtraBlanks таким образом, чтобы он сохранял линейную структуру текста, продолжая, тем не менее, удалять лишние пробелы на каждой строке. Начните с BNF-описания измененной проблемы, используя <маркер конца строки> в качестве маркера конца строки. Прикиньте, какая часть анализа потребует изменений, чтобы охватить измененную программу.

Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 5 6