4.2.1 Перекодировщик

Задача. Распечатать заданную последовательность литер, заменяя в ней каждое вхождение цифры 1 на слово ONE, а цифры 2 -- на слово TWO.

Решение. Введем следующие обозначения. Пусть $F$ -- это функция, сопоставляющая литере строку по следующим правилам: $F('1')$ = 'ONE', $F('2')$ = 'TWO', $F(X) = X$ для любой литеры $Х$, отличной от '1' и '2'. Обозначим через $КОД$ ту функцию преобразования последовательности, которую должна реализовать обрабатываемая программа. Непосредственно из условия задачи получаем следующие соотношения:

(1) КОД$(\Lambda) = \Lambda$

(2) КОД$(\alpha)$ = F(Голова$(\alpha)) \parallel$КОД(Хвост$(\alpha)),$ если $\mid \alpha \mid > 0$.

Соотношение (2) говорит о том, что оператор, реализующий вычисление функции $КОД$, можно записать как оператор цикла с условием на продолжение, тело которого -- это оператор, осуществляющий ввод очередной литеры из входного файла (обозначим ее через Х) и печать строки F(X) в выходной файл; при этом из соотношения (1) видно, что условием продолжения цикла будет непустота входного файла. В результате мы получаем программу
 

module Перекодировщик;
    var X : char;
begin
(*  1*)     (* {Output=КОД(Input1),$\mid Input1\mid=0\}$*)
(*  2*)     while ~ Eof do
(*  3*)            (* {Ограничивающее выражение:$\mid Input2 \mid \}$*)
(*  4*)            (*{Output = КОД(Input1), $\mid Input2 \mid >0 \}$*)
(*  5*)            read(X);
(*  6*)           if X = '1' then write ('ONE') end;
(*  7*)            if X = '2' then write ('TWO') end;
(*  8*)            if (X # '1') & (X # '2') then write (X) end
(*  9*)            (* {Output = КОД(Input1)} *)
(*10*)    end
(*11*)    (* {Output =КОД(Input)}*)
end Перекодировщик.

В это программе, как и в некоторых других, мы для удобства ссылок на части программы указываем в комментариях номера строчек.

Покажем, что программа действительно решает сформулированную задачу, т.е. является правильной относительно предусловия $\{Input \in Char^*$, $\mid Output\mid=\mid Input1\mid=0\}$ и постусловия {Output =КОД(Input)}.

Нетрудно проверить, что программа является частично правильной, т.е. если программа начинает с состояния, удовлетворяющего предусловию -- утверждению$\{Input \in Char^*$, $\mid Output\mid=\mid Input1\mid=0\},$ и завершает свою работу нормальным образом, то результирующее состояние удовлетворяет постусловию -- утверждению {Output = КОД(Input1)}.

Действительно, утверждение 1 (записанное в строчке программы с номером 1) вытекает из предусловия (в силу определения функции КОД) и является инвариантом цикла 2-9. Таким образом, по правилу вывода свойств оператора цикла с условием на продолжение получаем справедливость утверждения {Output=КОД(Input1),$\midInput2\mid=0\}.$ Что по правилу вывода следствий завершает доказательство справедливости утверждения 11 и, тем самым, частичной правильности программы.

Нужно еще показать, что программа нормальна завершается на любом состоянии памяти, удовлетворяющем предусловию. Для доказательства этого свойства во-первых заметим, что в ходе выполнения программы аварийные остановы программы не возможны. Вся программа -- это цикл 2-10, условие которого (см. строчку 2) выполнимо на любом состоянии памяти, а тело (строчки 5-8) применимо к любому состоянию памяти, удовлетворяющему утверждению 4.

Для доказательства нормальной завершаемости программы проведенных рассуждений, вообще говоря, может оказаться недостаточно, поскольку программа, содержащая цикл, может зациклиться. В данном случае доказательство конечности работы тривиально, поскольку программа Перекодировщик содержит только один цикл, а количество его повторений совпадает с длиной входной последовательности, которая хотя и различна для разных исполнений программы, но для каждого из них фиксирована и конечна. В качестве ограничивающего выражения цикла можно взять $\mid Input2\mid.$

Программа Перекодировщик$Перекодировщик$ может быть улучшена (см. программу Перекодировщик$Перекодировщик2$), если вычисление и печать F(X) (строчки 6-8) осуществить более эффективным и наглядным образом.
 

module Перекодировщик2;
    var X : char;
begin
    (* $\{Output= КОД(Input1) \}$*)
    while ~ Eof do (* {Ограничивающее выражение:$\mid Input2 \mid \}$*)
        (* {Output = КОД(Input1), $\mid Input2 \mid >0 \}$*)
        read(X);
        if X = '1' then write('ONE')
        elsif X = '2' then write('TWO')
        else write(X)
        end
        (* {Output = КОД(Input1)}*)
    end
    (* {Output = КОД(Input)}*)
end Перекодировщик2.

Если изменить условие исходной задачи, дополнив его предположением о непустоте входной последовательности, то проверка на пустоту в программе $Перекодировщик2$ становится избыточной и более адекватным решением для этой (несколько другой!) задачи будет программа$Перекодировщик3$.

module Перекодировщик3;
      var X : char;
begin
     (* {Output = КОД(Input1), $\mid Input2 \mid >0 \}$*)
     repeat
        (* {Output = КОД(Input1), $\mid Input2 \mid >0 \}$ *)
        read(X);
        if X = '1' then write('ONE')
        elsif X = '2' then write('TWO')
        else write(X)
        end
        (* {Output =КОД(Input1)}*)

        (* {Ограничивающее выражение:$\mid Input2 \mid \}$*)
     until Eof;
     (* {Output =КОД(Input)}*)
end Перекодировщик3.
 

© В.Н. Касьянов, Е.В.Касьянова, 2004