Содержание
-
Стандартные схемы программ
Дисциплина «Теория вычислительных процессов»
-
Программы и схемы программ
Схема программы – это абстрактная модель программы, которая описывает только структуру программы и не задает никаких типов данных, никаких конкретных функций и предикатов, и никаких конкретных значений переменных и констант.
-
Пример:
begin integerx, y; begin integerx, y; ввод(x); ввод(x); y:=1; y:=е; L: ifx=0 thengotoL1 L: ifx=0 thengoto y:=x*y; y:=CONSCAR(x, y); x:=x-1; x:=CDR(x); gotoL; goto L1: вывод(y); L1: вывод(y); end end
-
Базис класса стандартных схем программ
Базис В класса стандартных схем состоит: 1)Множества символов полного базиса: 1. Х = {x, х1, х2..., у, у1 у2..., z, z1, z2...} - множество символов, называемых переменными; 2. F = {f(0), f(1), f(2)..., g(0), g(1), g(2)..., h(0), h(1), h(2)...} - множество функциональных символов; верхний символ задает местность символа; нульместные символы называют константами и обозначают начальными буквами латинского алфавита a, b, c...; 3. Р = {р(0), р(1), р(2)...; q(0), q(1), q(2)...; } - множество предикатных символов; р(0), q(0) - ; нульместные символы называют логическими константами; 4. {start, stop, ..., := и т. д.} - множество специальных символов.
-
2)Термами (функциональными выражениями) : 1. односимвольные слова, состоящие из переменных или констант; 2. слово τ вида f(n)(τ1, τ2, ..., τn), где τ1, τ2, ..., τn - термы; Примеры термов: х, f(0), а, f(1)(х), g(2)(x, h(3)(y, a)).
-
3)Тестами (логическими выражениями) называются логические константы и слова вида р(n)(τ1, τ2,..., τn). Примеры: p(0), p(0)(х), g(3)(x, y, z), p(2)(f(2)(x, y)). 4)Множество операторов включает пять типов: 1. начальный оператор- слово вида start(х1, х2...хк), где k ≥0, а х1, х2...хк - переменные, называемые результатом этого оператора; 2. заключительный оператор- слово вида stop(τ1, τ2,..., τn), гдеn ≥ 0, а τ1, τ2,..., τn- термы; вхождения переменных в термы τ называются аргументами этого оператора;
-
3. оператор присваивания- слово вида х := τ, где х – переменная (результат оператора), а τ - терм; вхождения переменных в термы называются аргументами этого оператора; 4. условный оператор (тест) - логическое выражение; вхождения переменных в логическое выражение называются аргументами этого оператора; 5. оператор петли- односимвольное слово loop.
-
Способы представления ССП
Линейная форма стандартной схемы Для использования линейной формы СПП множество специальных символов расширим дополнительными символами
-
Графовая форма Стандартной схемой в базисе В называется конечный (размеченный ориентированный) граф без свободных дуг и с вершинами следующих пяти видов: 1. Начальная вершина (ровно одна). 2. Заключительная вершина (может быть несколько). 3. Вершина-преобразователь. 4. Вершина-распознаватель. 5. Вершина-петля. Конечное множество переменных схемы S составляют ее память ХS.
-
-
Способы представления ССП
Интерпретация стандартных схем программ Состоянием памяти программы (S,I) называют функцию W: XS D, которая каждой переменной x из памяти схемы S сопоставляет элемент W(x) из области интерпретации D.
-
Значение терма τ при интерпретации I и состоянии памяти W (обозначим τI(W)) определяется следующим образом: 1) если τ = х, x – переменная, то τI(W) = W(x); 2) если τ = a, a – константа, то τI(W) = I(a); 3) если τ = f(n)(τ1, τ2..., τn), то τI(W) = I(f (n))(τ1I(W), τ2I(W),..., τnI(W)). Аналогично определяется значение теста p при интерпретации I и состоянии памяти W или pI(W): если p = р(n)(τ1, τ2,..., τn), то pI(W) = I(p(n))(τ1I(W), τ2I(W),... τnI(W)), n ≥ 0.
-
Конфигурацией программы называют пару U = (L,W), где L - метка вершины схемы S, а W - состояние ее памяти. Выполнение программы описывается конечной или бесконечной последовательностей конфигураций, которую называют протоколом выполнения программы (ПВП).
-
Пример (вычисление n!):
Интерпретация (S1, I1) задана так: 1. область интерпретации D1 Nat - подмножество множества Nat целых неотрицательных чисел; 2. I1(x)=4; I1(y)=0; I1(a)=1; 3. I1(g)=G, где G - функция умножения чисел, т. е. G(d1,d2)= d1*d2; 4. I1(h)=H, где H - функция вычитания единицы, т. е. H(d)= d - 1; 5. I1(p)=P1, где P1 - предикат «равно 0», т.е. P1(d)=1, если d=0.
-
Вычислительные процессы
Дисциплина «Теория вычислительных процессов»
-
модель
Модель – это объект или описание объекта, системы для замещения одной системы (оригинала) другой системой для лучшего изучения оригинала или воспроизведения каких-либо его свойств. Любая модель строится и исследуется при определенных допущениях, гипотезах!!!
-
Задачи моделирования
Построение модели Исследование модели Использование модели Моделирование – универсальный метод получения описания функционирования объекта и использования знаний о нем.
-
Виды моделей
Статическая (не учитывается временной параметр) Динамическая (отображает систему во времени) Дискретная (отображает поведение системы в дискретные моменты времени) Непрерывная (описывает поведение системы для всех моментов времени некоторого промежутка)
-
Имитационная (изучение возможных путей развития путем варьирования параметров модели) Детерминированная (каждому входному набору параметров соответствует определенный набор выходных параметров) Стохастическая (вероятностная)
-
Вычислительный Процесс
Под процессом понимается программа в стадии выполнения. Процесс есть тройка (Q, f, g), где Q – множество состояний процесса; f – функция действия f : Q Q; g Q – начальное состояние процесса.
-
Свойства процесса
Действия, реализуемые процессом - результат выполнения некоторой программы на реальном (виртуальном) процессоре Процесс не является закрытой системой и может взаимодействовать с другими процессами, воспринимая или изменяя часть среды, которую он с ними разделяет Каждый процесс живет временно В любой момент процесс может быть описан его состоянием. Все параметры (переменные), характеризующие текущее состояние процесса, объединяются в "вектор состояний»
-
Переход процессов из разных состояний
-
Параллельные и последовательные процессы
Параллельные процессы выполняют части задачи, так чтобы не были задействованы одновременно одни и те же ресурсы. Последовательные процессы используют одни и те же ресурсы последовательно друг за другом.
-
Законы, управляющие поведением (P || Q), параллельно развивающихся процессов P и Q.
Первый закон выражает логическую симметрию между процессом и его окружением: L1. P || Q = Q || P. Следующий закон показывает, что при совместной работе трех процессов неважно, в каком порядке они объединены оператором параллельной композиции ||: L2. P || (Q || R) = (P || Q) || R. Процесс, находящийся в тупиковой ситуации, приводит к тупику всей системы. L3. P || СТОПaP = СТОПaP.
-
Модели параллельных вычислений
Процесс/канал Параллельные вычисления состоят из одного или более одновременно выполняющихся процессов, число которых может изменяться с течением времени выполнения программы Обмен сообщениями Модель не накладывает ограничений на динамическое создание процессов, на выполнение нескольких процессов одним процессором, на использование разных программ разными процессорами
-
Параллельность данных Данные и операции централизованно распределяются между всеми процессорами. Одна и та же операция может быть применена к множеству элементов и структур данных Модель общей памяти Все процессы совместно используют общее адресное пространство . Для синхронизации используются механизмы блокировки
-
Трансляция. Компиляция и интерпретация
дисциплина «теория языков программирования и методы трансляции»
-
Трансляция
Трансляция - процесс восприятия компьютером программы, написанной на некотором формальном языке. При всем своем различии формальные языки имеют много общего и эквиваленты с точки зрения потенциальной возможности написать одну и ту же программу на любом из них.
-
Фазы трансляции и выполнения программы
Подготовка программы начинается с редактирования файла, содержащего текст этой программы, который имеет стандартное расширение для данного языка. Затем выполняется его трансляция, которая включает в себя несколько фаз: препроцессор, лексический, синтаксический, семантический анализ, генерация кода оптимизация кода В результате трансляции получается объектный модуль – некий «полуфабрикат» готовой программы, который потом участвует в ее сборке. Файл объектного модуля имеет стандартное расширение obj.
-
Компоновка (сборка) программы заключается в объединении одного или нескольких объектных модулей программы и объектных модулей, взятых из библиотечных файлов и содержащих стандартные функции и другие полезные вещи. В результате получается исполняемая программа в виде отдельного файла (загрузочный модуль, программный файл) со стандартным расширением -".exe", который затем загружается в память и выполняется.
-
Препроцессор
Это предварительная фаза трансляции, которая выполняет обработку текста программы, не вдаваясь глубоко в ее содержание. Он производит замену одних частей текста на другие, при этом сама программа так и остается в исходном виде. Препроцессор - предварительная фаза трансляции на уровне преобразования исходного текста программы. Например, в языке Си директивы препроцессора оформлены отдельными строками программы, которые начинаются с символа "#" #define идентификатор строка_текста #define SIZE 100 Аналогичные средства в других языках программирования носят название макропроцессор, макросредства.
-
Трансляция и ее фазы1. Лексический анализ
Собственно трансляция начинается с лексического анализа программы. Лексика языка программирования - это правила правописания слов» программы, таких как идентификаторы, константы, служебные слова, комментарии. Лексический анализ разбивает текст программы на указанные элементы. Особенность любой лексики –ее элементы представляют собой регулярные линейные последовательности символов. Например, Идентификатор - это произвольная последовательность букв, цифр и символа "_", начинающаяся с буквы или "_".
-
Трансляция и ее фазы2. синтаксис
Синтаксисязыка программирования - это правила составления предложений языка из отдельных слов. Такими предложениями являются операции, операторы, определения функций и переменных. Особенностью синтаксиса является принцип вложенности (рекурсивность) правил построения предложений. Это значит, что элемент синтаксиса языка в своем определении прямо или косвенно в одной из его частей содержит сам себя. Например, в определении оператора цикла телом цикла является оператор, частным случаем которого является все тот же оператор цикла.
-
Трансляция и ее фазы3. семантика
Семантикаязыка программирования - это смысл, который закладывается в каждую конструкцию языка. Семантический анализ - это проверка смысловой правильности конструкции. Например, если мы в выражении используем переменную, то она должна быть определена ранее по тексту программы, а из этого определения может быть получен ее тип. Исходя из типа переменной, можно говорит о допустимости операции с данной переменной.
-
Трансляция и ее фазы4. генерация кода5. оптимизация
Генерация кода- это преобразование элементарных действий, полученных в результате лексического, синтаксического и семантического анализа программы, в некоторое внутреннее представление. Это могут быть коды команд, адреса и содержимое памяти данных, либо текст программы на языке Ассемблера, либо стандартизованный промежуточный код (например, P-код). В процессе генерации кода производится и его оптимизация.
-
Модульное программирование, компоновка
Полученный в результате трансляции объектный модуль включает в себя: готовые к выполнению коды команд адреса и содержимое памяти данных Но это касается только собственных внутренних объектов программы (функций и переменных). Обращение к внешним функциям и переменным, отсутствующим в данном фрагменте программы, не может быть полностью переведено во внутреннее представление и остается в объектном модуле в исходном (текстовом) виде. Но если эти функции и переменные отсутствуют, значит, они должны быть каким-то образом получены в других объектных модулях. Можно написать их на Си и оттранслировать.
-
Модульное программирование
Принцип модульного программирования-представление текста программы в виде нескольких файлов, каждый из которых транслируется отдельно. С модульным программированием можно столкнуться в двух случаях: когда сами пишем модульную программу; когда используем стандартные библиотечные функции.
-
Библиотека объектных модулей
Библиотека объектных модулей- это файл (библиотечный файл), содержащий набор объектных модулей и собственный внутренний каталог. Объектные модули библиотеки извлекаются из нее целиком при наличии в них требуемых внешних функций и переменных и используются в процессе компоновки программы.
-
Формальные языки и грамматики
-
Формальный язык – множество всех слов в алфавите А Конкатенация слов— двухместная операция над словами, заключающаяся в приписывании второго слова к первому. Результат конкатенации слов U и V обозначается UV.
-
Операции над формальными языками
объединение пересечение дополнение (до множества всех слов в рассматриваемом алфавите)
-
Основные определения
Алфавит – конечное непустое множество символов (Σ). Символ – любой знак, рассматриваемый как нечто неделимое - служебное слово языка программирования. Примеры: Σ1 = {a,b,c} Σ2 = {0, 1}
-
Цепочка над алфавитом Σ– произвольная конечная последовательность символов из Σ. Пример: α=abbc β=ab Пустая цепочка – цепочка, не содержащая символов.(ε)
-
Σ* - бесконечное множество всех цепочек над алфавитом Σ. Язык над алфавитом Σ– произвольное множество цепочек, составленных из символов Σ. Обозначается (L(Σ)
-
Примечание: Множество цепочек всегда бесконечно. Множество цепочек, образующих язык может быть конечным. Языки программирования содержат бесконечное множество цепочек.
-
Пример языка:
Язык L2 ={anbncn |n≥0} – множество всех цепочек, содержащих вначале некоторое количество символов a, затем такое же количество символов b, затем столько же символов c. aaabbbccc L2 aaabbbcc L2
-
Порождающие грамматики
Порождающие грамматики являются механизмом, который позволяет задать обширный класс языков, содержащих бесконечное множество цепочек. Порождающие грамматики используются при описании синтаксиса языков программирования.
-
Порождающей грамматикой называется четверка G=(T, N, P, S), где T – конечное множество терминальных символов – основной алфавит, порождаемого языка. Элементы множества Т – символы, из которых состоят цепочки языка, порождаемого данной грамматикой. Терминальный символ («конечный»). Терминалы обозначаются a, b, c.
-
N – конечное множеств нетерминальных (вспомогательных) символов – вспомогательный алфавит. Нетерминалы – это понятия грамматики (языка), которые используются при его описании. Обозначаются А, B, C.
-
P – конечное множество правил вывода, называемых продукциями. Каждое правило имеет вид α→β, где α и β – цепочки нетерминальных символов. Цепочка α не может быть пустой, β – может быть пустой. Правило α→βопределяет возможность подстановки β вместо α в процессе вывода(порождения) цепочек языка.
-
S (S принадлежит N) – начальный символ грамматики – одни из множества нетерминальных символов, начальный (стартовый) нетерминал. Начальный нетерминал – правило соотвествующее правильному предложению языка. Например, начальный нетерминал грамматики выражений обозначает «выражение». Начальный нетерминал грамматики языка Паскаль – «программа».
-
Пример:
Грамматика G: S→aSBc (1) S→abc (2) cB→Bc (3) bB→bb (4) S→ε (5)
-
Формальные методы описания перевода
Дисциплина «Теория языков программирования и методы трансляции»
-
Синтаксический анализ - это процесс, который определяет, принадлежит ли некоторая последовательность лексем языку, порождаемому грамматикой.
-
Синтаксический анализ
Синтаксический разбор (распознавание) является первым этапом синтаксического анализа. При его выполнении осуществляется подтверждение того, что входная цепочка символов является программой, а отдельные подцепочки составляют синтаксически правильные программные объекты.
-
Вслед за распознаванием отдельных подцепочек осуществляется анализ их семантической корректности на основе накопленной информации. Затем проводится добавление новых объектов в объектную модель программы или в промежуточное представление. Разбор предназначен для доказательства того, что анализируемая входная цепочка, записанная на входной ленте, принадлежит или не принадлежит множеству цепочек порождаемых грамматикой данного языка.
-
Синтаксический анализ
Выполнение синтаксического разбора осуществляется распознавателями, являющимися автоматами. Цель доказательства в том, чтобы ответить на вопрос: «Принадлежит ли анализируемая цепочка множеству правильных цепочек заданного языка?» Ответ «да» дается, если такая принадлежность установлена. В противном случае дается ответ «нет». Единственный отказ на любом уровне ведет к общему отказу.
-
Классификация методов синтаксического разбора
-
Методы семантического анализа
Нисходящий разбор заключается в построении дерева разбора, начиная от корневой вершины.
-
Пример нисходящего разбора
Дана грамматика G G8 = ({S}, {a, +, *}, P, S), где P определяется как: 1. S () a 2. S () S + S 3. S () S * S
-
Пример нисходящего разбора слева направо
Например, выражение «a+a*a+a» можно получить следующими способами: 1. S S+S a+Sa+S*S a+ a*S a+a*S+S a+a*a+Sa+a*a+a 2. S S+S S+a S*S+a S*a+a S+S*a+aS+a*a+aa+a*a+a 3. S S*S S+S*S S+S*S+S a+ S*S+S a+a*S+S a+a*S+aa+a*a+a
-
-
Пример нисходящего разбораслева направо
-
Восходящий разбор
При восходящем разборе дерево начинает строиться от терминальных листьев путем подстановки правил, применимых к входной цепочке, опять таки, в общем случае, в произвольном порядке.
-
Комбинированный разбор
Комбинированный разбор может быть реализован тогда, когда процесс распознавания разбивается на два этапа. На одном из них осуществляется нисходящий, а на другом – восходящий разбор. Этапов может быть и больше, а порядок их применения – произвольным. Комбинированным можно считать разбор в любом трансляторе, если фазу лексического анализа принять за первый этап, а синтаксического – за второй.
-
эквивалентности МП-автоматов и КС-грамматик
Теорема Язык является контекстно-свободным тогда и только тогда, когда он допускается МП-автоматом.
-
Преобразование КС-грамматик
Алгоритм 1 Устранение недостижимых символов.
-
Преобразование кс-грамматик
Алгоритм 2 Устранение несводимых символов
-
Устранение бесполезных символов
Чтобы устранить все бесполезные символы, необходимо применить к исходной грамматике сначала Алгоритм 2, а затем Алгоритм 1.
-
Разбор сверху-вниз(предсказывающий разбор)
Пусть дана КС-грамматика G = (N; T; P; S). Главная задача предсказывающего разбора - определение правила вывода, которое нужно применить к нетерминалу.
-
Предсказывающий разбор
Предсказывающий анализатор имеет входную ленту, управляющее устройство (программу),таблицу анализа, магазин (стек) и выходную ленту. Входная лента содержит анализируемую строку, заканчивающуюся символом $- маркером конца строки. Выходная лента содержит последовательность примененных правил вывода.
-
Предсказывающий разбор
Таблица анализа - это двумерный массив M[A; a], где A-нетерминал, и a - терминал или символ $. Значением M[A; a]может быть некоторое правило грамматики или элемент"ошибка". Магазин может содержать последовательность символов грамматики с $на дне. В начальный момент магазин содержит только начальный символ грамматики на верхушке и $на дне.
-
Предсказывающий разбор
Анализатор работает следующим образом: Вначале анализатор находится в конфигурации, в которой магазин содержит S$, на входной ленте w$ ( w- анализируемая цепочка), выходная лента пуста. На каждом такте анализатор рассматривает X- символ на верхушке магазина и a-текущий входной символ. Эти два символа определяют действия анализатора.
-
Варианты действия анализатора:
-
Синтаксически управляемый перевод
Фактически, такая схема представляет собой КС-грамматику, в которой к каждому правилу добавлен элемент перевода. Всякий раз, когда правило участвует в выводе входной цепочки, с помощью элемента перевода вычисляется часть выходной цепочки, соответствующая части входной цепочки, порожденной этим правилом.
-
Схемы синтаксически управляемого перевода
-
Схема синтаксически управляемого перевода
где u (NT)*, v (N)* и вхождения нетерминалов в цепочку v образуют перестановку вхождений нетерминалов в цепочку u, так что каждому вхождению нетерминала B в цепочку u соответствует некоторое вхождение этого же нетерминала в цепочку v; если нетерминал B встречается более одного раза, для указания соответствия используются верхние целочисленные индексы; S - начальный символ, выделенный нетерминал из N.
-
Схема синтаксически управляемого перевода
-
Схема синтаксически управляемого перевода
-
Класс переводов, определяемых магазинными преобразователями, совпадает с классом простых СУ-переводов. Существуют простые СУ-схемы, имеющие в качестве входных грамматик LR(1)-грамматики и не реализуемые ни на каком детерминированном преобразователе с магазинной памятью.
-
Обобщенная СУ-схема
-
Транслирующие грамматики
Построение транслирующих грамматик предполагает применение подхода, который предусматривает использование одной грамматики и разрешает включение как входных, так и выходных символов в каждое правило такой грамматики.
-
Транслирующиеграмматики
Назначение: Позволяют решать задачу перевода в более сложных случаях, чем СУ-схемы. Транслирующие грамматики это разновидность КС-грамматик, где символы (терминалы) разделены на два множества, Σiи Σa(a от action), называемые „входными“ и „операционными“ соответственно. При использовании ТГ, чтобы различать элементы Σiи Σa, чтобы различать последние, они заключаются в фигурные скобки, ‘{’, ‘}’, считая получившиеся на письме три символа одним символом алфавита.
-
Транслирующие грамматики
Определение. Транслирующей грамматикой (Т -грамматикой) называется КС-грамматика, множество терминальных символов которой разбито на множество входных символов и множество выходных символов, которые называются также символами действия.
-
Пример(Т – грамматика):
-
Выходные символы обозначим фигурными скобками. С использованием таких обозначений правила грамматики ГТ4.1 имеют вид:
-
Вывод в транслирующих грамматиках выполняется по тем же правилам, что и в обычных КС - грамматиках. Например, в рассматриваемой грамматике из начального символа может быть выведена следующая цепочка: ==> a{x} ==> a{z}{x} ==> a{z}{x]b{y} Каждый символ или цепочка символов, заключенные в фигурные скобки, должны рассматриваться как единый символ, называемый символом действия.
-
В общем случае цепочки символов, заключенные в фигурные скобки, можно интерпретировать как имена процедур, выполнение которых производит требуемый эффект на выходе. При описании перевода предусматривается, что каждый символ действия представляет собой процедуру, осуществляющую передачу символа, заключенного в фигурные скобки, на выход. Когда нужно подчеркнуть, что используется такая интерпретация символов действия, то Т - грамматику называют грамматикой цепочного перевода.
-
Атрибутные грамматики
В Атрибутной грамматике с каждым символом грамматики может быть связан один или несколько атрибутов. Для каждого синтаксического правила вводятся семантические правила, устанавливающие функциональные зависимости между атрибутами. Дерево, содержащее атрибуты, называется аннотированным. Атрибуты придают смысл синтаксической структуре, описываемой деревом, и потому аннотированное дерево называется также семантическим деревом.
-
Атрибут a(X0) синтезируемый, если одному из правил вывода p:X0 ->X1...Xnp сопоставлено семантическое правило a = fa(...) Атрибут a(Xi) наследуемый, если одному из правил вывода p: X0 -> X1...Xi...Xпр сопоставлено семантическое правило a=fa(...), i[1,пр] Множество синтезируемых атрибутов символа X - S(X) Множество наследуемых атрибутов символа Х - I(X) Значение атрибутов терминальных символов- константы (т.е. их значения определены, но для них нет семантических правил, определяющих их значения)
-
Атрибутная грамматика
-
Атрибутные грамматики
Атрибутная грамматика называется незацикленной, если графы зависимостей деревьев всех цепочек, принадлежащих языку, определяемому грамматикой G, не содержат циклов, Атрибутная грамматика называется зацикленной, если существует хотя бы одна цепочка, принадлежащая языку, для дерева разбора которой граф D(t) содержит ориентированный цикл.
-
Теорема 1 Задача определения того, является ли данная атрибутная грамматика зацикленной, имеет экспоненциальную временную сложность, то есть существует константа c > 0 такая, что любой алгоритм, проверяющий на зацикленность произвольную атрибутную грамматику размера n, должен работать более, чем 2cn/lognшагов на бесконечно большом числе грамматик
-
Алгоритм кнута (Проверка атрибутной грамматики на зацикленность)
-
Атрибутные грамматики
Теорема 2 Атрибутная грамматикаAGнезациклена тогда и только тогда, когда ни один из графовDp[G1 ... Gnp]не содержит ориентированных циклов, то есть когда алгоритм B.1. заканчивается со значениемcycle = false. Теорема 3 Алгоритм Кнута проверки на зацикленность атрибутной грамматики размераnтребует в общем случаеexp(cn2)шагов.
-
Верификация программ
-
Верификация - это процесс определения, выполняют ли программные средства и их компоненты требования, наложенные на них в последовательных этапах жизненного цикла разрабатываемой программной системы. Основная цель верификации состоит в подтверждении того, что программное обеспечение соответствует требованиям. Дополнительной целью является выявление и регистрация дефектов и ошибок, которые внесены во время разработки или модификации программы.Верификация является неотъемлемой частью работ при коллективной разработке программных систем.
-
Правила верификации программ
Основа для исчисления выводов программ - правила К.Хоара (правила верификации) для интерпретации программных конструкций. Правила (аксиомы) К.Хоара определяют предусловия, как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.
-
A1. Аксиома присваивания: { Ro } x := e { R } Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение e, то R будет истинно после выполнения, если результат подстановки e вместо x в R истинен перед выполнением. Таким образом Ro = R(x) при x = e. Для Ro вводится обозначение: Ro=Rxe (у Вирта) или Rx->e (у Дейкстры)что означает, что x заменяется на e.Аксиома присваивания будет иметь вид:{ Rxe} x:=e {R}
-
Сформулируем два очевидных правила. A2. Если известно: { Q } S { P } и { P } => { R }, то { Q } S { R }A3. Если известно: { Q } S { P } и { R } => { Q }, то { R } S { P }Пусть S - это последовательность из двух операторов S1;S2 (составной оператор). A4. Если известно:{ Q } S1 { P1 } и { P1 } S2 { R }, то { Q } S { R }.Очевидно, что это правило можно сформулировать для последовательности, состоящей из n операторов.Сформулируем правило для условного оператора (краткая форма). A5. Если известно:{ Q and B } S1 { R } и{ Q not B } => { R },то { Q } if B then S1 { R }.Правило A5 соответствует интерпретации условного оператора в языке программирования.
-
Сформулируем правило для альтернативного оператора (полная форма условного оператора ).A6. Если известно:{ Q and B } S1 { R } и{ Q not B } S2 { R },то { Q } if B then S1 else S2 { R }. Сформулируем правила для операторов цикла. Предусловия и постусловия цикла until (до) удовлетворяют правилу:A7. Если известно:{ Q andnot B } S1 { Q } , то{ Q } repeat S1 until B { Q andnot B } Правило вводит важное понятие инварианта цикла. Предикат Q, истинный перед выполнением и после выполнения каждого шага цикла, называется инвариантным отношением или просто инвариантом цикла. В математике термин "инвариантный" означает не изменяющийся под воздействием совокупности рассматриваемых математических операций. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.
-
Предусловия и постусловия цикла while (пока) удовлетворяют правилу:A8. Если известно: { Q and B } S1 { Q } ,то { Q } while B do S1 { Q andnot B } Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла. Кроме того, правила можно использовать для анализа результатов выполнения программы, что связано с семантикой программы.
-
Абстрактная интерпретация
Абстрактный синтаксис программ является утончением синтаксиса данных, а именно - выделением подкласса вычислимых выражений (форм), т.е. данных, имеющих смысл как выражения языка и приспособленных к вычислению. Внешне это выглядит как объявление объектов, заранее известных в языке, и представление разных форм, вычисление которых обладает определенной спецификой.
-
Операционная семантика языка определяется как интерпретация абстрактного синтаксиса, представляющего выражения, имеющие значение.
-
интерпретатор
Интерпретатор (interpreter) — программа, выполняющая интерпретацию, а также вид транслятора, осуществляющего пооперационную (покомандную) обработку и выполнение исходной программы или запроса. В отличие от компилятора, который осуществляет трансляцию всей программы высокого уровня в машинные коды один раз без ее выполнения (создает объектную программу), интерпретатор транслирует исходную программу команда за командой каждый раз при выполнении и не создает объектного модуля. За счет такого режима выполнение программы происходит медленнее, чем в случае ее обработки транслятором, однако при обработке интерпретатором программы выполняются сразу, без промежуточной стадии трансляции.
-
Абстрактный интерпретатор
Абстрактный интерпретатор – это сложный интерпретатор, компилирующего типа, перед выполнением производящий компиляцию исходного кода программы в машинный или «промежуточный код». Они быстрее выполняют большие и циклические программы, не занимаются анализом исходного кода в реальном времени.
Нет комментариев для данной презентации
Помогите другим пользователям — будьте первым, кто поделится своим мнением об этой презентации.