Теоретическое исследование моделей программы, решающей заданную задачу
Дипломная работа - Компьютеры, программирование
Другие дипломы по предмету Компьютеры, программирование
?ндуктивных утверждений независимо сформулирован К. Флойдом и П. Науром. Суть этого метода состоит в следующем:
) формулируются входное и выходное утверждения: входное утверждение описывает все необходимые входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат;
) предполагая истинным входное утверждение, строится промежуточное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями); такое утверждение называется выведенным утверждением;
) формулируется теорема (условия верификации): из выведенного утверждения следует выходное утверждение;
) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента).
Пусть А - утверждение, описывающее предполагаемые свойства данных в программе, аС - утверждение, описывающее то, что по предположению требуется получить в результате выполнения программы (утверждение о правильности). Программа частично правильна, если при каждом ее выполнении с данными, удовлетворяющими предположению А, будет справедливо утверждение С при условии, что программа закончится.
Программа полностью правильна, если она частично правильна и заканчивается при всех данных удовлетворяющих предположению А. [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* - выходная функция, сопоставляющая переходу мультимножество его выходных позиций.
Позиция pP называется входом для перехода tT, если pI(t). Позиция pP называется выходом для перехода tT, если pO(t). Структура сети Петри определяется ее позициями, переходами, входной и выходной функциями.
Маркировка сетей Петри
Маркировка - это размещение по позициям сети Петри фишек, изображаемых на графе сети Петри точками. Фишки используются для определения выполнения сети Петри. Количество фишек в позиции при выполнении сети Петри может изменяться от 0 до бесконечности.
Маркировка m сети Петри N=(P,T,I,О) есть функция, отображающая множество позиций P во множествоNat неотрицательных целых чисел. Маркировка m, может быть также определена как n-вектор m=, где n- число позиций в сети Петри и для каждого 1 i n m(pi) Nat - количество фишек в позиции pi.
Маркированная сеть Петри N=(P,Т,I,О,m) определяется совокупностью структуры сети Петри (P,T,I,О) и маркировки m.
Анализ сетей Петри
Моделирование систем сетями Петри, прежде всего, обусловлено необходимостью проведения глубокого исследования их поведения. Для проведения такого исследования необходимы методы анализа свойств самих сетей Петри. Этот подход предполагает сведения исследования свойств реальной системы к анализу определенных свойств моделирующей сети Петри.
Свойства сетей Петри
Позиция pP сети Петри N=(P,Т,I,O) c начальной маркировкой m является k-ограниченной, если m(p)k для любой достижимой маркировки mR(N,m). Позиция называется ограниченной, если она является k-ограниченной для некоторого целого значения k. Сеть Петри ограниченна, если все ее позиции ограниченны.
Позиция pP сети Петри N=(P,Т,I,O) c начальной маркиров