Программное исчисление

Часть II. Программное исчисление.

Следующий шаг.

Часть I была посвящена тому, как писать программы, решая простые задачи с использованием простого языка программирования, CF Pascal. Часть II выводит нас на следующий уровень, предлагая нам осознать обобщенные математические концепции программирования, которым подчиняются все программы. При этом наша цель остается неизменной – изучение программирования методом проб и ошибок, используя подход сходный с обучением слепой печати на клавиатуре. В части I мы рассматривали средства языка, часть II будет знакомить нас с технологиями систематического программирования.

Компактный CFPascal был подходящим выбором для части I, поскольку он позволял нам концентрироваться на программировании, а не на изучении языка программирования. Для части II он также хорошо подходит, потому что он позволит нам решить следующую задачу: рассматривать программы как математические объекты, более сложные, чем просто строки символов. Рассмотренные идеи будут масштабироваться вне зависимости от роста размеров программ, подобно тому, как, обучившись делению трехзначных чисел, мы сможем в дальнейшем делить тридцатизначные.

Понимание программ как математических объектов организовано как программное исчисление, которое ориентировано в основном на семантику программ, а не на синтаксис.

Что такое программное исчисление.

Вводный курс в дифференциальное исчисление в математике основывается на концепции гладкой функции, принимающие вещественные (real) значения. Исчисление связано с понятием вычисления двух связанных функций: производной и первообразной (интеграла) для данной функции. Такие вычисления очень значимы в физике и технических дисциплинах, собственно современная физика и производные науки без этих вычислений невозможны. Функции дифференциального исчисления имеют физический смысл, производная – это интенсивность изменения величины, например скорости движения (ускорение), интеграл – площадь подкривой.

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

Фундаментальными объектами программного исчисления так же являются функции, но эти функции дискретны, то есть определены не на множестве вещественных чисел, а на конечном множестве символов и других математических объектов сформированных из символов. Такие функции задают значение программ. Поскольку любая программа на CFPaskal заставляет Паскаль-машину преобразовывать входные данные в выходные, результат работы такой программы может быть описан с помощью функции, преобразующей множество символов из INPUT во множество символов OUTPUT.

В программном исчислении существуют две основные задачи. Первая, для данной программы как синтаксического объекта найти функцию, описывающую ее значения. Вторая, имея функцию, описывающую значение программы, найти программу с таким значением. Вторая задача ведет нас к систематическим методам проектирования и разработки программ, а первая – к систематическим методам верификации правильности программ.

Способность вывода функции значения для данной программы в программном исчислении является очень значимой для компьютерных наук. Во-первых, она позволяет проводить математическое доказательство корректности программ, а именно: задает ли программа корректное поведение компьютера любых возможных входных данных. Отладка некорректных программ является принципиальной причиной низкой продуктивности процесса разработки программного обеспечения. Способность выводить функции из программ систематическим образом является даже более важной, потому что делает возможным шаг за шагом сформировать дисциплину разработки программ, которые корректны изначально и не требуют отладки. Систематическое программирование как дисциплина является основной целью части II.

Математическими основами программного исчисления являются пять дискретных математических структур символьных данных, а именно:

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

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

Рассмотрение программ как математических объектов унифицирует и упрощает вопросы проектирования программ и достижения их корректности. Человечество не так давно занимается компьютерными программами, но они являются одним из самых логически сложных произведенных им артефактов. Для преодоления сложности у человечества нет другого средства кроме математики. Поскольку математика изменялась последние пятьсот лет под воздействием потребностей физики и технических наук, так что можно надеяться, что потребности компьютерных наук также будут иметь определяющее влияние на математику в течение следующих ста лет.

Программы как математические объекты

Фундаментальный подход в компьютерных науках предполагает понимание программ как математических объектов, о которых можно рассуждать с математической строгостью. Математически программа больше, чем ее представление на языке программирования, например таком как CFPascal. Аналогичная ситуация с числами. Число тринадцать – математический объект, который имеет свойство быть тринадцатью вне зависимости от того, как это число будет представлено в письменной или устной форме: словом «двенадцать», набором цифр «12», или в римском варианте «XII» или «дюжина». Все эти представления являются строками символов. Разница между числом и его устным или письменным обозначением в том, что число имеет определенные математические свойства, не зависимые от того, как мы называем или обозначаем это число. Двенадцать – это на два больше, чем десять, четное, кратное трем, четырем, шести и т. д.

Выделение концепции натуральных чисел в виде набора аксиом было большим достижением в математике, сделанным итальянским математиком Джузеппе Пеано, который жил на рубеже XIX и XX веков.

Пеано ввел два понятие целого (натурального) числа, понятие следования одного числа непосредственно за другим в натуральном ряде и понятие начального члена натурального ряда (за который можно принять 0 или 1). Эти понятия связаны между собой пятью аксиомами, которые можно рассматривать как аксиоматическое определение указанных основных понятий.

1)  0 есть натуральное число;

2)  следующее за натуральным числом есть натуральное число;

3)  0 не следует ни за каким натуральным числом;

4)  если натуральное число а следует за натуральным числом b и за натуральным числом с, то b и с тождественны;

5)  если какое-либо предложение доказано для 0 и если из допущения, что оно верно для натурального числа n, вытекает, что оно верно для следующего за п натурального числа, то это предложение верно для всех натуральных чисел.

Последняя аксиома - аксиома полной индукции - даёт возможность доказывать общие свойства натуральных чисел.

Обычные названия чисел могут быть интерпретированы как сокращения для неуклюжих названий, которые встречаются в работе Пеано. Пусть следующий для целого числа n будет обозначаться s(n). Тогда сокращения будут такими:

1 для s(0)

2 для s(1) = s(s(0))

…

10 для s(9) = s(s(8)) = …

…

100 для s(99) = s(s(98)) = …

Математические свойства чисел 0, 1, 2 , …, 10, …, 100,… зависят только от 0 и s, а не от представления их с помощью цифр. Например, 10 > 8, потому что существует выражение

10 = s(s(8)), 5 = 3 + 2, потому что 5 = s(s(3)) (s использовано дважды). Нужно заметить, что представления чисел ни разу не использованы в работе Пеано, за исключением символа 0, который достаточно условно взят как символ начала последовательности.

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

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

[будущие инженеры должны это знать, уже сейчас некоторые теряют интеллектуальный контроль на простых программах, пример с IFSort3б или впадают в ступор неверно поставив точку с запятой]

Свойство программ, которое не зависит от их представления, синтаксиса – управление поведением компьютером. Программа, которая сортирует строку, конечно имеет представление, выраженное в соответствии с синтаксическими правилами, но суть того, что она делает – сортировка. Может существовать множество программ на CF Pascal, которые сортируют строку, подобно тому как число 12 может быть получено из 11+1, 10+2, 7+5 и т. д. Аналогичные программ могут быть написаны на других языках программирования, таких как BASIC или С. Каждый язык программирования – всего лишь средство выражения способа решения задачи аналогично тому, как арабские или римские цифры представляют натуральные числа. Функциональное поведение программы независимо от ее представления на том или ином языке программирования и конкретной формы для выбранного языка.

Таким образом, понимание программ как математических объектов – это понимание функционального поведения программ по управлению компьютером.

Синтаксис и семантика CF Pascal

Программы на CF Pascal, как сложные объекты, могут быть рассмотрены с разных точек зрения. Персонаж, у которого программа не компилируется, может думать, что главное – соблюдение синтаксиса. Специалист по документированию – может думать, что наиболее важно соблюдать косметические моменты, такие как отступы, комментарии и т. д., не думая о проблемах компиляции. Некто, изучающий программу с целью модификации, может быть озабочен ее размером, поскольку большую программу изучать и дорабатывать сложнее.

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

Нотация Бекуса-Наура (BNF) предоставляет нам точный способ описания синтаксиса CF Pascal. Вместе с контекстными правилами, синтаксические правила BNF описывают все возможности для разработки программ на CF Pascal.

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

оно должно показывать нам, что происходит с переменными и файлами, и какими выражениями программы вызваны те или иные изменения. Тут мы сталкиваемся с проблемой тестовых данных: на каких входных данных должно быть описано поведение программы. Идеальный ответ: «на любых», или «на всех». Полное семантическое описание программы должно включать все варианты. Это означает, что с помощью таблицы выполнения такое описание получить невозможно.

Семантическое значение для данной CF Pascal программы будет математическое отношение или функция, упорядоченный набор пар, который определяет соответствие между одним набором данных (INPUT) и другим набором данных (OUTPUT). Значением программы будет трансформация данных, описанная следующим соответствием: данным значениям в INPUT соответствуют значения в OUTPUT полученные при выполнении этой программы на Паскаль-машине.

5. СЕМАНТИКА CF PASCAL.

Глава 5 знакомит нас с концепцией значения программ. Для точного описания этой идеи используются такие математические структуры как строки, списки, множества, отношения и функции.

Знать значение программы – значит быть способным определить выход программы для любого заданного входа. Если для некоторого X на входе программа выдает Y на выходе, то такая пара формирует часть значения функции. Множество всех пар X, Y для которых программа выполняется корректно, является полным значением программы.

Если какие-то входные данные X0 вызывают аварийное завершение или бесконечное выполнение, то X0 н принадлежит значению программы.

Для некоторых программ значения выражаются довольно просто.

PROGRAM Copy (INPUT, OUTPUT);

{Writes first character in INPUT to OUTPUT}

VAR

Ch: CHAR;

BEGIN

READ(Ch);

WRITELN(Ch);

END.

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

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

5.1. Строки символов.

Строки символов – математические объекты, , имеющие имена, над ними определены операции и отношения.

Новые идеи: строка символов, символьный литерал, строковый литерал, пустая строка, конкатенация, композиция, декомпозиция, подсписок.

Строковый литерал (или просто строка) - последовательность символов, чье начало и конец помечены специальным символом – маркером строки.

Строка, не имеющая символов, 0-строка, называется пустой строкой. Примеры строк:

†† - 0-строка

†□† - 1-строка

†string† - 6-строка

†□string□† - 8-строка

Символьные литералы мы помечаем горизонтальным штрихом над символом, например S для изображения пробелов используем специальный символ □.

Строковые и символьные литералы не одно и то же, их не нужно путать. 1-строка не то же самое, что символ, который в ней размещается. Например, □ – символ, †□† - 1-строка.

Строковым литералам удобно присваивать имена, например: S = †string†. Строка может иметь несколько имен, но одно имя использовать для нескольких строк некорректно. Имена лучше всего использовать для именования не каких-то определенных строк, а тех, значение которых мы можем предположить.

CF Pascal предлагает три операции для манипулирования строками:

Оператор CF Pascal	Строковая операция
WRITE(‘ABC’)	Конкатенация
WRITE(Ch)	Композиция
READ(Ch)	Декомпозиция

Эти операции над строками образуют базис для работы со строками как математическими объектами.

5.1.1. Конкатенация строк.

Выходные данные программы обычно представляют собой строку символов, создаваемую выполнением операторов WRITE. Оператор WRITE, где <список вывода> является <строкой символов>, помещает новую строку вслед за текущими данными в OUTPUT.

Операция конкатенации в CF Pascal задается оператором WRITE и заключается в помещении строки символов в OUTPUT. Конкатенацией двух строк является третья строка, полученная присоединением второй строки к первой. Например:

C= †character†

S= †string†

C&S=†characterstring†

S&C=†stringcharacter†

S&S=†stringstring†

Для пустой строки справедливо следующее тождество:

† † & S = S & † † = S

Операция конкатенации является бинарной (два операнда, оба - строки), инфиксной (символ операции помещается между операндами), ассоциативной ((C&B)&S = C&(B&S)) и не является коммутативной (S&C ¹ C & S).

5.1.2. Подстроки.

Строки W = †WRITE(Any, ‘string’)† и строка S = †string† имеют некоторое отношение, а именно символы встречаются внутри W. Говорят, что строка S является подстрокой W.

Строка P является подстрокой Q, если и только если существует строки X и Y, такие что

Q= X & P & Y

В случае с S и W мы можем записать

W = †WRITE(Any, ‘† & S & †’)†

Где согласно определению подстроки

X = †WRITE(Any, ‘†

Y = †’)†

Или для строки T = †tring†

S = †s† & T

T - подстрока S и согласно определению подстроки

X = †s†

Y = ††

или

S = †s† & T & ††

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

5.1.3. Композиция строк.

Оператор WRITE может выполнять другую операцию, присоединяя значение переменной типа CHAR к строке, которая является текущим значением OUTPUT. Это операция композиции, обозначаемая знаком Ñ. Композиция строки и символа – добавление символа к концу строки.

†strin† Ñ g = †string†

Композиция обеспечивает нам способ превращения символа в строку

† † Ñ g = †g†

Это общее тождество, связывающее символ и 1-строку содержащую этот символ.

Композиция с пустой строкой настолько полезна, что пустую строку принято опускать и получается унарная префиксная версия композиции:

Ñ g = †g†

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

Следующие варианты недопустимы для композиции

Вариант	Причина
a Ñ b	Первый операнд – символ
Ñ †x†	Операнд 1-строка, а не символ
N Ñ ††	Оба операнда выбраны неверно

5.1.3. Декомпозиция строк.

Если оператор WRITE реализует конкатенацию и композицию строк, то оператор READ выполняет разбиение строк. При каждом выполнении оператора READ с одной переменной строка символов в INPUT разделяется на две части. Первый символ в INPUT становится значением символьной переменной, которая используется в выражении READ, а оставшиеся символы становятся текущей строкой для ввода.

Строковые операции голова (head) и хвост (tail) точно описывают то, что происходит при выполнении выражения READ. Глова (Θ) и хвост (Λ) – унарные префиксные операции, определенные на непустых строках.

Θ S – первый символ в строке S

Λ S – подстрока S полученная удалением первого символа

Например для:

S = †string†

T = †tring†

Θ S = s

Λ S = †tring† = T

Θ T = t

Λ T = †ring†

Поскольку хвост строки – строка, он может служить предметом дальнейшей декомпозиции, например:

Θ (Λ T) = r

Λ(Λ T) = †ing†

Λ (Λ(Λ T)) = †ng†

Θ (Λ (Λ(Λ T))) = n

К-й символ строки может быть извлечен К-1 операциями хвост, к результату которых применена операция голова.

Следует выделить следующие моменты:

Операции голова и хвост не определены на пустых строках Результат операции голова – символ, операции хвост – строка.

Поскольку голова строки – символ, мы можем превратить его в строку с помощью композиции, далее с помощью конкатенации с хвостом получим исходную строку.

Θ †string† = s

Λ †string† = †tring†

Ñ(Θ †string†) = †s†

(Ñ(Θ †string†)) & (Λ †string†) = †s† & †tring† = †string†

Этот пример описывает фундаментальное тождество, связывающее операции конкатенации, композиции и декомпозиции, а именно: для любой непустой строки S справедливо следующее:

(Ñ(Θ S)) & (Λ S) = S

Следующая таблица обобщает наши знания о строковых операциях.

Операция	Символ	Пример
конкатенация	&	†me† & †you† = †meyou†
композиция	Ñ	†plural†Ñs = †plurals†
символ в 1-строку	Ñ	Ñv = †v†
голова	Θ	Θ†feet† = f
хвост	Λ	Λ†rattle† = †attle†