Анализ процедуры RemoveExtraBlanks

Тестирование процедуры RemoveExtraBlanks.

Для тестирования этой процедуры полезно пометить начало и конец строк, чтобы их легко было видеть. Для этой цели можно использовать символ #.

 

PROGRAM TestRes(INPUT, OUTPUT)

VAR

Ch: CHAR;

TestIn, TestOut: TEXT;

PROCEDURE RemoveExtraBlanks(VAR FileIn, FileOut: TEXT);

{ копирует слова из FileIn в FileOut, удаляя головные и хвостовые пробелы, а также лишние пробелы между словами }

BEGIN

ASSIGN(TestIn, ‘TestIn.txt’);

ASSIGN(TextOut, ‘TestOut.txt’);

WHILE NOT EOF

{копируем одну строку из INPUT в файл TestIn, с эхом ввода};

 

RemoveExtraBlanks(TestIn, TestOut);

 

{Копируем результирующую строку из TestOut в OUTPUT}

END

END

Задание 2. Написать недостающие разделы проекта для программы TestRes. При выводе результата на экран пометить начало и конец входной и выходной строки символом #.

INPUT:

Pack my box with six.

SOLIDPACKED□□

OUTPUT:

Input is: # Pack my box with six.#

Output is: #Pack my box with six.#

Input is: #SOLIDPACKED #

Output is: #SOLIDPACKED#

(15 баллов)

Программа передает каждую входную строку процедуре RemoveExtraBlanks и выводит результат. Описание синтаксиса входной строки в форме Бекуса-Наура для всех возможных входов (правила 1 и 2) дают нам способ выбора тестовых данных. Если мы полагаем, что разделы RemoveExtraBlanks для пропуска пробелов и копирования слов работают корректно, единственное, что должно быть протестировано – это комбинация позиций <слов> и <пробелов> описываемых данными синтаксическими правилами. Согласно этим правилам возможно 4 варианта:

<пробел>

<слово> <пробелы> <список-слов-пробелов> <пробел>

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

<пробелы> <слово> <проелы> <список-слов-пробелов> <пробел>

 

Заслуживающие внимания тестовые случаи, за исключением конечного <списка-слов-пробелов> <пробела> такие:

††

†the †

† †

† the †

 

 

Анализ процедуры RemoveExtraBlanks

Для того чтобы продемонстрировать, что RemoveExtraBlanks выполняет то, ради чего была спроектирована, ее функция должна быть вычислена. Пролект для части DO внутреннего оператора WHILE такой:

{копируем слово};

FlushBlanks(Ch);

{вставляем пробел, если это не последнее слово}

 

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

Функция C для копирования слова такая:

C = C1 | C2

где

C1 = ((Ch <> ‘ ‘)

AND (NOT(EOF(FileIn))) AND (FileIn.2 = (x s B) & y)

AND (FileIn.3 = R) AND (FileOut.3 = W) ’

Ch,FileOut.1,FileIn.1, FileIn.2 :=

□,(FileOut.1 s Ch) & x,FileIn.1 & (x s B),y)

и

C2 = (Ch = ‘ ‘ ’ )

 

где x – строка не пробельных символов, не содержащая маркера конца строки, y – строка, а B – либо маркер конца строки, либо □. В этом и в следующих условных присваиваниях элементы 3-списков файлов изображаются при помощи индекса, следующего за точкой. Например, FileIn.2 означает FileIn₂, второй элемент списка (являющийся строкой будущего). Такая нотация позволяет записывать условные присваивания в комментариях программе, где запись индексов не возможна.

Функция F для FlushBlanks(Ch) такая:

F = (F0 ’ (F1 | F2)) | F3

где

F0 = ((Ch = ‘ ‘) AND (NOT(EOF(FileIn))) AND (FileIn.3 = R)

F1 = (FileIn.2 = b s Z & w ’

Ch, FileIn.1, FileIn.2 := Z, FileIn.1 & b s Z, w)

F2 = (FileIn.2 = b s / ’

Ch, FileIn.1, FileIn.2 := □, FileIn.1 & FileIn.2, ††)

F3 = ((Ch <> ‘ ‘) OR (EOF(FileIn)) ’ )

где b - строка из пробелов и маркеров конца строки (возможно, пустая), Z – это символ, отличный от пробела и маркера конца строки, а w – непустая строка символов.

 

 

Задание 3. Доказать, что

BEGIN {copy word} … END = C

и

FlushBlanks(Ch) = F

(30 баллов)

 

Доказательство того, что функция I соответствует условной вставке пробела, следует далее:

 

I = I1 | I2

I1 = ((NOT(EOF(FileIn))) AND (FileOut.3 = W) AND (FileIn.3 = 3) ’

FileOut.1 = FileOut.1 s □)

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

 

Значение части DO, следовательно, является композицией этих трех функций C◦ F ◦ I. Композиция может быть вычислена с использованием условных трассировочных таблиц. Каждое условие помечается. Имеется два условия для C, три условия для F и два - для I. Всего 12 комбинаций. Каждая таблица помечается условиями, которые она покрывает. Например, (C1, F1, I1) представляет первое условие C, первое условие F и первое условие I. FileIn и FileOut будут сокращенно называться FI и FO, соответственно.

12 случаев:

Случай 1(C1, F1, I1)	Случай 5 (C1, F3, I1)	Случай 9 (C2, F2, I1)
Случай 2(C1, F1, I2)	Случай 6 (C1, F3, I2)	Случай 10 (C2, F2, I2)
Случай 3(C1, F2, I1)	Случай 7 (C2, F1, I1)	Случай 11 (C2, F3, I1)
Случай1 4(C1, F2, I2)	Случай 8 (C2, F1, I2)	Случай 12 (C2, F3, I2)

 

Случай 1(C1, F1, I1)

Условие	Ch	F0.1	FI.1	FI.2
(Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.2 = z s B & y) AND (FI.3 = R) AND (FO.3 = W)	□	FO.1 s Ch & z	FI.1 & z s B	y
(□ = ‘ ‘) AND (NOT(EOF(<FI.1 & z s B,y,FI.3>))) AND (FI.3 = R) AND (y = b s Z & w)	Z		FI.1 & z s B & b s Z	w
NOT(EOF(<FI.1 & z & B & b s Z, w, FI.3>)) AND (FI.3 = R) AND (FO.3 = W)		FO.1 s Ch & z s □

 

Условие такое:

(Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.2 = z s B & y) AND (FI.3 = R) AND (FO.3 = W) AND (□ = □)

AND (NOT(EOF(<FI.1 & z s B,y,FI.3>)) AND (y = b s Z & w)

AND (NOT(EOF(<FI.1 & z & B & b s Z, w, FI.3>)))

 

Несколько частей данного условия эквивалентны TRUE:

 

Условие	равно TRUE, т.к.
□ = □	Очевидно
NOT(EOF(<FI.1 & z s B,y,FI.3>))	Из-за следующего условия: y = b s Z & w, а w – не пусто
NOT(EOF(<FI.1 & z & B & b s Z, w, FI.3>))	W не пусто

 

Таким образом, выполнив подстановку y, условие уменьшается до:

Условие:

(Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.2 = x s B & b s Z & w) AND (FI.3 = R) AND (FO.3 = W)

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

Ch, FO.1, FI.1, FI.2 := Z, FO.1 s Ch & x s □, FI.1 & x s B & b s Z, w

 

Задание 4. Аналогичным образом напишите условные присваивания для случаев 2 - 12. Покажите, что произойти могут только случаи 1, 4, 6, 7, 10 и 12.

(55 баллов)

 

 

Собирая вместе все возможные случаи, композиция трех функций C◦F◦I имеет условия и присваивания:

Случай 1.

Условие: (Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.2 = x s B & b s Z & w) AND (FI.3 = R) AND (FO.3 = W)

return false">ссылка скрыта

Присваивание: Ch, FO.1, FI.1, FI.2 := Z, FO.1 s Ch & x s □, FI.1 & x s B & b s Z, w

 

Случай 4.

Условие: (Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.2 = x s B & b s /) AND (FI.3 = R) AND (FO.3 = W)

Присваивание: Ch, FO.1, FI.1, FI.2 := □, FO.1 s Ch & x s □, FI.1 & x s B & b s /, ††

 

Случай 6.

Условие: (Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.3 = R) AND (FO.3 = W) AND (FI.2 = x s /)

Присваивание: Ch, FO.1, FI.1, FI.2 := □, FO.1 s Ch & x, FI.1 & x s /, ††

 

Случай 7.

Условие: (Ch = ‘ ‘) AND (NOT(EOF(FI))) AND (FI.3 = R) AND (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

 

Случай 10.

Условие: (Ch = ‘ ‘) AND (NOT(EOF(FI))) AND (FI.3 = R) AND (FI.2 = b s /)

Присваивание: Ch, FI.1, FI.2 := □, FI.1 & FI.2, ††

 

Случай 12.

Условие: (Ch = ‘ ‘) AND (NOT(EOF(FI))) AND (FI.3 = R)

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

 

Игнорируя условия того, что входной файл должен быть открыт для чтения, а выходной – для записи, случаи 1, 4 и 6 происходят когда значении Ch не равно □, а входной файл не закончился, согласно значению FileIn.2, мы имеем следующее:

Случай	FileIn.2	Следующее слово z	Добавляение к FileOut.1
	Z s B & b s Z & w	пары <пробел> <слово>	s Ch & z s □
	Z s B & b s /	<пробелы>	s Ch & z
	Z s /	Маркер конца строки	s Ch & z

 

z – это строка непробельных символов, не содаржащая маркер конца строки, B – пробел, либо маркер конца строки, b – строка пробелов или маркеров конца строк, w – это непустая строка, Z- символ, не являющийся пробелом либо маркером конца строки

 

Случаи 7 и 10 происходят, когда значения Ch равно □, а входной файл не закончился.

Случай	FileIn.2	Следующие <пробелы> b	Добавляение к FileOut.1
	b s Z & w	пары <слово> <пробел>	s Ch & z s □
	b s /	Маркер конца строки	s Ch & z

Случай 12 происходит в конце файла. К FileOut ничего не добавляется.

Функция g = C ◦ F ◦ I может быть записана в виде условного присваивания при помощи комбинирования случаев, написанных выше.

g =

((Ch <> ‘ ‘) AND (NOT(EOF(FI))) AND (FI.3 = R) AND (FO.3 = W) ’

(1) (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) |

(4) (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 /, ††) |

(6) (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) ’

(7) ((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) |

(10) (FI.2 = b s / ’ Ch, FI.1, FI.2 := □, FI.1 & FI.2, ††)) |

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

(12)

 

Номера слева идентичны случаям, осуждаемым выше. Эта функция описывает копирование слова из 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
	<слово><пробелы><непробел>	<слово> <пробел>	<непробел>	FALSE
	<слово> <пробелы>	<слово>	<пробел>	TRUE
	<слово> <пробел>	<слово>	<пробел>	TRUE
	<пробелы> <непробел>	<пробел>	<непробел>	FALSE
	<пробелы>	<пустая строка>	<пробел>	TRUE
	<пробел>	<пустая строка>	<пробел>	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 будут обсуждены неформально.

1. domain(f) = domain( WHILE... )

2. (EOF(FileIn) ’ f) = (EOF(FileIn) ’ )

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

 

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

(30 баллов)

 

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

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

 

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

(10 баллов)

 

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

(15 баллов)

 

Задание 8. Модифицируйте проект RemoveExtraBlanks (для получения процедуры RemoveAllWords) так, чтобы действие программы было реверсированным: программа должна записывать только все пробелы и пропускать слова.

(15 баллов)

 

Задание 9. Обозначив входную строку буквой S, выходную строку программы RemoveExtraBlanks обозначив W, а выходную строку программы RemoveAllWords буквой B, объясните, почему:

Длина (S) ≠ длина(W) + длина (B)

(15 баллов)

 

Задание 10. Докажите, что реализацией для {вставить пробел, если это не последнее слово} также может являться:

IF Ch <> ‘ ‘

THEN

WRITE(FileOut, ‘ ‘)

(15 баллов)

 

Задание 11. Текстовый файл содержит трехзначные числа, разделенные пробелами (одним или несколькими). Числам могут предшествовать нулевые символы (несколько, либо ни одного). Цель: переформатировать файл в файл с разделителями в один пробел, с убиранием ведущих нулей (за исключением числа ноль, который должен выглядеть так: 0).

a) Опишите проблемы с использованием BNF

b) разделите множество входных строк на группы и создайте наборы тестовых данных для каждой группы.

c) Напишите проект программы, решающей данную задачу.

(50 баллов)

Задание 12. Даны 2 строки. Первая строка состоит из пробелов. Вторая – из слов и пробелов. Предположив, что длина первой строки определяет ее ширину, выведите каждое слово из второй строки в отцентрированном (относительно ширины первого слова) виде.

(20 баллов)