Следующие главы будут развивать программное исчисление, что позволит вычислять P для любой программы. Однако, часто в простых случаях возможно определить P неформально, точно зафиксировав что делает программа P с помощью неформального анализа.
Любая программа, используя оператор READ, может встретить маркер конца строки или конца файла, что усложняет значение программы. Например, пусть Q – программа:
PROGRAM ReadWriteRead(INPUT, OUTPUT);
VAR
Ch: CHAR;
BEGIN
READ(Ch);
WRITELN(Ch);
READ(Ch)
END.
Входной файл может быть организован как список строк, каждая из которых завершена маркером конца строки. Здесь есть несколько вариантов, которые следует рассмотреть.
Если список пуст, первый оператор READ приведет к ошибке выполнения. Если INPUT - 1-список, и его единственная строка – пустая строка, первый оператор READ прочитает маркер конца строки (как пробел), а второй приведет к аварийному завершению работы.
Если первая строка в INPUT не пуста, тогда первый оператор READ возвратит первый символ, второй оператор READ вернет либо второй символ, либо маркер конца строки, если второй символ отсутствует. В этом случае Q выполняется корректно и выводит первый символ первой строки INPUT в OUTPUT. Если INPUT 2- или более-список, и первая строка пуста, тогда оператор READ возвращает символ конца строки как пробел, а второй оператор RED берет первый символ второй строки, если таковой имеется, или ее маркер конца строки. В этом случае Q выполняется корректно и записывает пробел в OUTPUT. Этот анализ суммируется в следующей нотации для Q, как преобразования INPUT в OUTPUT.
Q = {<L, M>: L ¹ <>, L1 ¹ ††, M = <Ñ (Θ L1)>,} È
{<L, M>: L ¹ <>, Λ L ¹ <>, L1 = ††, M =†□†}
Отметим, что здесь L1, первый элемент списка L здесь означает первую строку в INPUT.
Область определения и область значений Q могут быть определены прямо из Q путем нахождения первого и второго элементов в парах. Область определения – список строк
domain (Q) = {L: L ¹ <>, L1 ¹ †† } È { L: L ¹ <>, Λ L ¹ <>, L1 = ††}
Для range (Q) вторые элементы пар 1-списки 1-строк, и единственный символ это либо начальный символ строки или пробел. Таким образом,
range (Q) = {M: M – 1-список, содержащий 1-строку}
Необходимо отметить, что значение программы просто пропускает пары, для которых не существует корректное выполнение, например, для которых L – пустой список или 1-список с элементом - пустой первой строкой.
Рассмотрим R:
PROGRAM CopyTwice(INPUT, OUTPUT);
VAR
Ch: CHAR;
BEGIN
READ(Ch);
READ(Ch);
WRITE (Ch);
WRITELN(Ch);
END.
Для того, чтобы записать значение R, нужно найти второй символ, если таковой есть списка строк L в INPUT, учитывая встречаемость строковых маркеров.
| Условия | Комментарии |
| L = <> | аварийное завершение |
| L ¹ <> | рассмотреть L1 |
| L1 = †† | рассмотреть существование L2 |
| Λ L = <> | аварийное завершение |
| Λ L ¹ <> | рассмотреть L2 |
| L2 = †† | напечатать пробел дважды |
| L2 ¹ †† | напечатать дважды Θ L2 |
| L1 ¹ †† | рассмотреть L1 |
| Λ L1 = †† | напечатать пробел дважды |
| Λ L1 ¹ †† | напечатать дважды Θ (Λ L1) |
Как результат этого анализа значение R будет:
R = {<L, M>: L ¹ <>, L1 = ††, Λ L ¹ <>, L2 = ††, M = <†□□†>} È
{<L, M>: L ¹ <>, L1 = ††, Λ L ¹ <>, L2 ¹ ††, M = <(Ñ(Θ L2))Ñ (Θ L2)>} È
{<L, M>: L ¹ <>, L1 ¹ ††, Λ L1 = ††, M = <†□□†>} È
{<L, M>: L ¹ <>, L1 ¹ ††, Λ L1 ¹ ††, M = <(Ñ(Θ (Λ L1)))Ñ (Θ (Λ L1))>}.
Заключение
Строки, списки и множества обеспечивают необходимый инструментарий для точного определения значений CF Pascal программ. Строки и списки используют операции конкатенации (&), композиции (Ñ)б и декомпозиции (Θ и Λ). Рассматривая текстовые файлы как 3-список мы можем дать точное описание файловым манипуляциям, включая все сложные ситуации с границами строки допустимые последовательности операций.
Для множеств определены операции объединения (È), пересечения (Ç), и разности (–). Множества базовые математические понятия, используемые при создании отношений и функций, которые используются для анализа значений программ.
Box-нотация различает синтаксический аспект программы P (ее символьная строка) и семантический аспект P (функция ее значения).
