XIX Белоусов А.И., Ткачев СБ. Дискретная математика (1081422), страница 111
Текст из файла (страница 111)
Таким образом, семантика цикла определяется как решение уравнения. Это определение корректно, так как правая часть уравнения есть непрерывное отображение множества (Е -+ Е) в себя (что следует из доказанной выше непрерывности композиции преобразователей состояний и очевидной непрерывности тождественного отображения). 4. Семантика последовательности операторов: ДЯ1 Я2Д = ДЯ1ДоДЯ2Д. Определенная таким образом формальнзл семантика языка МП,АХ становится базой для семантического анализа программ, т.е.
для строгого математического доказательства утверждений о программах. Этот анализ, проводимый технологически после синтаксического анализа программы и получения ее дерева вывода, основан на результате, известном под Д.8.2. Семаатвяа формааьимх .еамааа 707 названием принципа индукции по неподвижной точке'. Приведем формулировку этого принципа без доказательства. Принцип индукции по неподвижной точке. Пусть Р есть некоторое утверждение о программах, У вЂ” непрерывное отображение множества (Š— ь Е) в себя, у — наименьшая ненодеижнаа шочка отиображеннл У или, что то же самое, наименьшее решение уравнения Х = У(Х). Тогда, если Рф~)) истинно и для каждого а из истинности Р(у(0) следует истинность Рф'+Ц), то истинно РЦ).
(Под ~~0 понимается а-е приближение наименьшей неподвижной точки: у(е) = О, у(0 = Р(у(*'-'>) ( . 1.8).) Проиллюстрируем применение этого принципа на примере анализа простейшей программы на языке МП АИ. Рассмотрим программу вычисления факториала: Ьедан х змп; р:=0; х:= 11 шЫе (р ~ х) до р:= у+1~ х:=лар; ети1 етЫ Здесь предполагается, что все переменные принимают целые значения. Букву п следует понимать не как переменную программы, а как условное обозначение произвольного натурального числа, „зась|лаемогоа в „ячейку" х. Мы вынуждены прибегать к столь неэстетичному (с программистской точки зрения) вводу исходного значения, так как наш простенький язык не имеет средств ввода/вывода.
Докажем следующее утверждение Р об этой программе: если после выполнения программы состояние памяти о таково, что о(х) ф О л о(х) ~ О, то о(х) = п(х)! 'См:. Доноаоу П. 708 8. КОНТЕКСТНО-СВОБОДНЫЕ ЯЗЫКИ Заметим, что мы не определяли в языке операторов ввода и вывода и, следовательно, начальное состояние памяти задается априори (некоторым „оракулом"), а вопрос, как это состояние сформировано, остается за пределами формализации. В нашем примере речь идет о задании начального значения переменной п. Проанализируем теперь, что означает в данном случае индукция по неподвижной точке.
Ясно, что перед выполнением цикла состояние памяти ое таково, что всегда сне(з) = сге(д)!. Нам нужно доказать, что если выполнение цикла заканчивается после конечного числа итераций, то в результирующем состоянии и будем иметь 0'(2) = 0 (х)! = (7(д) !. Нам будет удобно определить операцию р-дизъюнкции преобразователей состояний памяти, где р($Н...,Ф„) — некоторое условие языка МП АХ. Определение 8.19. Назовем р-диэъюмициеб преобразователей состояний памяти у' и д преобразователь, обозначаемый я(~ Ч д) и определяемый следующим образом: О, значение предиката р в состоянии и не определено; 1(.), р„=1; д(и), р~ = О, (через р„обозначено значение условия, или предиката, р в состоянии ьч р =р(11,".,~')).
В соответствии с тем, как мы определили вьппе, Преобразователь состояний у, соответствующий циклу, есть наименьшая неподвижная точка уравнения ~ = г'(у), где функция г' может быть представлена в виде г'(д)(и) = р(1Р Ч '1о))од)(и) (для условия р и тела о цикла шЬ11е). Д.В.2. Семавтвка формальвмк лэмкоа 709 Согласно алгоритму вычисления наименьшей неподвижной точки (см. 1.8), у = вар (~~'): 1 > 0 ), где ~~о) = Π— стирающий преобразователь. Вычисляя первое приближение наименьшей неподвижной точки, получаем У~ц = (пэуЮ 0), где Я вЂ” тело цикла.
Очевидно, что для произвольного состояния и ~ О неравенство ~О)(и) ф О имеет место тогда и только тогда, когда р„ определено и равно О. Тогда ~~Ц(и) = и. Таким образом, первое приближение соответствует нулевому числу повторений тела цикла. Для второго приближения имеем р(П) Ч ((Я)) р(1РЧ ~[Я)~ 0)). Точно так же легко видеть, что ~~2>(и) ~ О тогда и только тогда, когда р„определено и равно 0 ф2>(и) = и) или когда рв =1, но р(яи„1 =0 ф2)(и) =181(и)). Таким образом, второе приближение соответствует не более чем однократному числу повторений тела цикла.
Методом математической индукции несложно доказать, что а-е приближение наименьшей неподвижной точки для семантики цикла соответствует не более чем (1 — 1)-кратному повторению тела цикла, если ~<О(и) ~ О для произвольного состояния р ~ О.
Следовательно, индукцвл по неподвижной точке сводится в данном случае к индукции по числу повторений цикла, и нам длв данного конкретного примера нужно доказать, что выполнение тела цикла сохраняет соотношение значений переменных у и ю для любого и, такого, что и(к) = и(у)!, ~[Я)(и)(к) = = '182(и)(у)!, где Я вЂ” тело цикла в программе вычисления факториал а. 710 8.
КОНТЕКСТНО-СВОБОДНЫЕ ЯЗЫКИ В самом деле, ага(.п ) =а"=".л(а.:=.+ д(.))() = =~Ь)1 ( (р)+1) =( Ы+1)'=М$(~)Ы' что и требовалось доказать. Теперь остается заметить, что поскольку условие выхода из цикла имеет вид р ~ х, то, задав переменной и некоторой значение из 1ч,после выполнения нашей программы достигнем требуемого результата. Мы рассмотрели простейший случай денотационного определения для языка, не содержащего даже блоков и процедур. При появлении последних возникают локальные определения переменных и необходимо модифицировать понятие состояния памяти. Это может быть реализовано с помощью понятия среды, которая формально определяется как декартово произведение 1 х Ьос множества переменных на множество „адресов", а состояние памяти при этом понимается как отображение вида и: 1х Ьос-> Р.
Денотационное определение, как уже упоминалось, не является единственным в рамках зкстенсионального подхода. Кроме него наиболее употребительными являются операциональное и трансформационное определения. При операциональном определении в качестве зкстенсионзла программы рассматривается множество последовательностей состояний памяти, генерируемых при выполнении программы. Трансформационное определение сопоставляет программе преобразователь вида „состояние памяти -+ пара (программа, состояние памяти ) ".
А именно если программа начинает работать над некоторым исходным состоянием памяти <т, то все операторы, которые могут быть выполнены, выполняются, а все операторы, которые не могут быть выполнены (из-за неопределенности значений переменных) „складываютсл" в новую программу (нвзывземую остаточной): таким образом возникает пара (остаточная црограмма, частичный результат = новое состояние <т').
Подобное д.В.З. у'рвфовов представление МП-автоматов 711 вычисление, называемое смешанным, позволяет определять различные преобразования (трансформации) программ. Семантика языков программирования в настоящее время является бурно развивающейся областью теории формальных языков, используемой при разработке и реализации языков программирования и программных продуктов (в частности, при разработке надежного программного обеспечения).
Дополнение 8.3. Графовое представление МП-автоматов Как и конечные автоматы, МП-автоматы также допускают графовое представление, которое, конечно, является более сложным, чем графовое представление конечных автоматов. Так, МП-автомату М = (Я, т', Г, ов, Р, ов, б) сопоставляется ориентированный муяьтиграур (в отличие от обычного ориентированного графа в мультиграфе допускается несколько дуг для одной и той же упорядоченной пары вершин, т.е. несколько дуг, начало и конец которых совпадают), множество вершин которого есть множество состояний автомата, а каждая дуга которого имеет метку в виде упорядоченной тпройки (Я, а, у), где Я вЂ” магазинный символ, ив входной символ или пустпая цепочка, у — магазинная цепочка.
По определению, дуга е, ведущая из вершины (состояния) о в вершину (состояние) т имеет метку (Я, а, у), если и только если в системе команд 6 находится команда оаЯ ~ гу. Замечание 8.16. Более формально ориентированный мультиграф может быть определен как упорядоченная тройка С = (т', Е, ~р), где У вЂ” множество вершин, Š— множество дуг, а у — отображение множества Е в множество У х 'т', называемое урункцией инциденпьностпи.
Таким образом, если для различных дуг ец ..., еь все значения у(е1), 712 8. КОНТЕКСТНО-СВОБОДНЫЕ ЯЗЫКИ ~р(еь) равны, то возникает „множественная", или „кратная", дуга, т.е. множество дуг, отображаемых в одну и ту же упорядоченную пару вершин (и, е). Графически зто можно изобразить так, как показано на рис. 8.40. В том случае, когда функция инцидентности есть иньекиил, мультиграф превращается в обычный ориентированный граф.
В мулътиграфе, представляющем МП-автомат, множество дуг для заданной упорядоченной пары состояний (д, г) находится во взаимно однозначном соон3вен3с1нвии с~ с множеством всех команд даЯ -+ г у для различных а Е р 0 (А), Е Е Г, у Е Г'. Можно было бы задавать МП-автомат и Рис. 8.40 обычным ориентированным графом, но тогда пришлось бы по-иному вводить метки дуг. Технически удобнее каждой команде сопоставлять отдельную дугу и строить таким образом ориентированный мультиграф. Введем понятие магазинной меп3ки пути в мультиграфе МП-автомата.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
