Метод индуктивных утверждений

Метод индуктивных утверждений независимо сформулирован К. Флойдом и П. Науром. Суть этого метода состоит в следующем:

) формулируются входное и выходное утверждения: входное утверждение описывает все необходимые входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат;

) предполагая истинным входное утверждение, строится промежуточное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями); такое утверждение называется выведенным утверждением;

) формулируется теорема (условия верификации): из выведенного утверждения следует выходное утверждение;

) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента).

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

Программа полностью правильна, если она частично правильна и заканчивается при всех данных удовлетворяющих предположению А. [1]

Доказательство правильности программ с помощью индуктивных утверждений

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

) Построить структуру программы.

) Выписать входное и выходное утверждения.

) Сформулировать для всех циклов индуктивные утверждения.

) Составить список выделенных путей.

) Построить условия верификации.

) Доказать условие верификации.

) Доказать, что выполнение программы закончится. [1]

Cети Петри

сеть петри модель программа

Сети Петри это инструмент для математического моделирования и исследования сложных систем. Цель представления системы в виде сети Петри и последующего анализа этой сети состоит в получении важной информации о структуре и динамическом поведении моделируемой системы. Эта информация может использоваться для оценки моделируемой системы и выработки предложений по ее усовершенствованию. Впервые сети Петри предложил немецкий математик Карл Адам Петри. [2]

Теоретико-множественное определение сетей Петри

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

Сеть ПетриN является четверкой N=(P,Т,I,O), где = {p1, p2,..., pn} - конечное множество позиций, n ³ 0;= {t1, t2,..., tm} - конечное множество переходов, m ³ 0;: T ® P* - входная функция, сопоставляющая переходу мультимножество его входных позиций;

О: T ® P* - выходная функция, сопоставляющая переходу мультимножество его выходных позиций.

Позиция pÎP называется входом для перехода tÎT, если pÎI(t). Позиция pÎP называется выходом для перехода tÎT, если pÎO(t). Структура сети Петри определяется ее позициями, переходами, входной и выходной функциями.

Маркировка сетей Петри

Маркировка - это размещение по позициям сети Петри фишек, изображаемых на графе сети Петри точками. Фишки используются для определения выполнения сети Петри. Количество фишек в позиции при выполнении сети Петри может изменяться от 0 до бесконечности.

Маркировка m сети Петри N=(P,T,I,О) есть функция, отображающая множество позиций P во множествоNat неотрицательных целых чисел. Маркировка m, может быть также определена как n-вектор m=<m(p1), m(p2),…, m(pn)>, где n- число позиций в сети Петри и для каждого 1 £ i £ n m(pi) Î Nat - количество фишек в позиции pi.

Маркированная сеть Петри N=(P,Т,I,О,m) определяется совокупностью структуры сети Петри (P,T,I,О) и маркировки m.

Анализ сетей Петри

Моделирование систем сетями Петри, прежде всего, обусловлено необходимостью проведения глубокого исследования их поведения. Для проведения такого исследования необходимы методы анализа свойств самих сетей Петри. Этот подход предполагает сведения исследования свойств реальной системы к анализу определенных свойств моделирующей сети Петри.

Свойства сетей Петри

Позиция pÎP сети Петри N=(P,Т,I,O) c начальной маркировкой m является k-ограниченной, если m’(p)£k для любой достижимой маркировки m’ÎR(N,m). Позиция называется ограниченной, если она является k-ограниченной для некоторого целого значения k. Сеть Петри ограниченна, если все ее позиции ограниченны.

Позиция pÎP сети Петри N=(P,Т,I,O) c начальной маркировкой m является безопасной, если она является 1-ограниченной.Сеть Петри безопасна, если безопасны все позиции сети.

Сеть Петри N=(P,Т,I,O) с начальной маркировкой m является сохраняющей, если для любой достижимой маркировки m’ÎR(N,m) справедливо следующее равенство.

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

Уровень 0: Переход t обладает активностью уровня 0 и называется мёртвым, если он никогда не может быть запущен.

Уровень 1: Переход t обладает активностью уровня1 и называется потенциально живым, если существует такаяm’ÎR(N,m), что t разрешён в m’.

Уровень 2: Переход t, обладает активностью уровня2 и называется живым, если для всякой m’ÎR(N,m) переход t является потенциально живым для сети Петри N с начальной маркировкой m’.

Сеть Петри называется живой, если все её переходы являются живыми.

Задача достижимости: Для данной сети Петри с маркировкойm и маркировки m’ определить: m’ÎR(N,m)?

Задача покрываемости: Для данной сети Петри N с начальной маркировкой m и маркировки m’ определить, существует ли такая достижимая маркировка m”ÎR(N,m), что m">³m’.

(Отношение m"³m’ истинно, если каждый элемент маркировки m" не меньше соответствующего элемента маркировки m’.)

Сети Петри присуще некоторое поведение, которое определяется множеством ее возможных последовательностей запусков переходов или ее множеством достижимых маркировок. Понятие эквивалентности сетей Петри определяется через равенство множеств достижимых маркировок.

Сеть Петри N=(P,Т,I,O) с начальной маркировкой m и сеть Петри N’=(P’,Т’,I’,O’) с начальной маркировкой m’ эквивалентны, если справедливо R(N,m)=R(N’,m’).

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

Более слабым, по сравнению с эквивалентностью, является свойство включения, определение которого совпадает с определением эквивалентности, с точностью до замены = на Í.

Анализ свойств сетей Петри на основе дерева достижимости

Анализ безопасности и ограниченности. Сеть Петри ограниченна тогда и только тогда, когда символ w отсутствует в ее дереве достижимости.

Присутствие символа w в дереве достижимости (m[х](p)=w для некоторой вершины x и позиции p) означает, что для произвольного положительного целого k существует достижимая маркировка со значением в позиции p, большим, чем k (а также бесконечность множества достижимых маркировок). Это, в свою очередь, означает неограниченность позиции p, а следовательно, и самой сети Петри.

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

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

Анализ покрываемости. Задача покрываемости требуется для заданной маркировки m' определить, достижима ли маркировкаm"³m'. Такая задача решается путём простого перебора вершин дерева достижимости. При этом ищется такая вершина х, что m[x]³m'. Если такой вершины не существует, то маркировка m' не является покрываемой. Если она найдена, то m[x] определяет покрывающую маркировку для m' Если компонента маркировки m[x], соответствующая некоторой позиции p совпадает с w, то конкретное её значение может быть вычислено. В этом случае на пути от начальной маркировки к покрывающей маркировке имеется повторяющаяся последовательность переходов, запуск которой увеличивает значение маркировки в позиции p. Число таких повторений должно быть таким, чтобы значение маркировки в позиции p превзошло или сравнялось с m'(p).

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

Доказательство очевидно.

Ограниченность метода дерева достижимости. Как видно из предыдущего, дерево достижимости можно использовать для решения задач безопасности, ограниченности, сохранения и покрываемости. К сожалению, в общем случае его нельзя использовать для решения задач достижимости и активности, эквивалентности. Решение этих задач ограничено существованием символа w. Символ w означает потерю информации: конкретные количества фишек отбрасываются, учитывается только существование их большого числа.[2]