Принцип индукции по неподвижной точке
Пусть есть некоторое утверждение о программах, — непрерывное отображение множества в себя, — наименьшая неподвижная точка отображения или, что то же самое, наименьшее решение уравнения .
Тогда, если истинно и для каждого из истинности следует истинность , то истинно . (Под понимается i-е приближение наименьшей неподвижной точки: .)
Проиллюстрируем применение этого принципа на примере анализа простейшей программы на языке MILAN. Рассмотрим программу вычисления факториала:
Здесь предполагается, что все переменные принимают целые значения. Букву следует понимать не как переменную программы, а как условное обозначение произвольного натурального числа, "засылаемого" в "ячейку" . Мы вынуждены прибегать к столь неэстетичному (с программистской точки зрения) вводу исходного значения, так как наш простенький язык не имеет средств ввода/вывода.
Докажем следующее утверждение об этой программе: если после выполнения программы состояние памяти а таково, что и , то .
Заметим, что мы не определяли в языке операторов ввода и вывода и, следовательно, начальное состояние памяти задается априори (некоторым "оракулом"), а вопрос, как это состояние сформировано, остается за пределами формализации. В нашем примере речь идет о задании начального значения переменной .
Проанализируем теперь, что означает в данном случае индукция по неподвижной точке.
Ясно, что перед выполнением цикла состояние памяти таково, что всегда . Нам нужно доказать, что если выполнение цикла заканчивается после конечного числа итераций, то в результирующем состоянии а будем иметь .
Нам будет удобно определить операцию p-дизъюнкции преобразователей состояний памяти, где — некоторое условие языка MILAN.
Определение 8.19. Назовем p-дизъюнкцией преобразователей состояний памяти и преобразователь, обозначаемый и определяемый следующим образом:
(через обозначено значение условия, или предиката, в состоянии ).
В соответствии с тем, как мы определили выше, Преобразователь состояний , соответствующий циклу, есть наименьшая неподвижная точка уравнения , где функция может быть представлена в виде
(для условия и тела цикла ).
Согласно алгоритму вычисления наименьшей неподвижной точки, , где — стирающий преобразователь.
Вычисляя первое приближение наименьшей неподвижной точки, получаем
, где — тело цикла.
Очевидно, что для произвольного состояния неравенство имеет место тогда и только тогда, когда определено и равно 0. Тогда .
Таким образом, первое приближение соответствует нулевому числу повторений тела цикла. Для второго приближения имеем
Точно так же легко видеть, что тогда и только тогда, когда определено и равно 0 или когда , но . Таким образом, второе приближение соответствует не более чем однократному числу повторений тела цикла. Методом математической индукции несложно доказать, что i-е приближение наименьшей неподвижной точки для семантики цикла соответствует не более чем (i-1)-кратному повторению тела цикла, если для произвольного состояния .
Следовательно, индукция по неподвижной точке сводится в данном случае к индукции по числу повторений цикла, и нам для данного конкретного примера нужно доказать, что выполнение тела цикла сохраняет соотношение значений переменных и : для любого , такого, что , имеем где — тело цикла в программе вычисления факториала.
В самом деле (что и требовалось доказать),
Теперь остается заметить, что поскольку условие выхода из цикла имеет вид , то, задав переменной некоторой значение из множества натуральных чисел , после выполнения нашей программы достигнем требуемого результата.
Мы рассмотрели простейший случай денотационного определения для языка, не содержащего даже блоков и процедур. При появлении последних возникают локальные определения переменных и необходимо модифицировать понятие состояния памяти. Это может быть реализовано с помощью понятия среды, которая формально определяется как декартово произведение множества переменных на множество "адресов", а состояние памяти при этом понимается как отображение вида .
Денотационное определение, как уже упоминалось, не является единственным в рамках экстенсионального подхода. Кроме него наиболее употребительными являются операциональное и трансформационное определения. При операциональном определении в качестве экстенсионала программы рассматривается множество последовательностей состояний памяти, генерируемых при выполнении программы. Трансформационное определение сопоставляет программе преобразователь вида "состояние памяти → пара (программа, состояние памяти)". А именно если программа начинает работать над некоторым исходным состоянием памяти , то все операторы, которые могут быть выполнены, выполняются, а все операторы, которые не могут быть выполнены (из-за неопределенности значений переменных) "складываются" в новую программу (называемую остаточной): таким образом возникает пара (остаточная программа, частичный результат = новое состояние ). Подобное вычисление, называемое смешанным, позволяет определять различные преобразования (трансформации) программ.
Семантика языков программирования в настоящее время является бурно развивающейся областью теории формальных языков, используемой при разработке и реализации языков программирования и программных продуктов (в частности, при разработке надежного программного обеспечения).
Если заметили ошибку, опечатку или есть предложения, напишите в комментариях.
|