Стандартные схемы программ в линейной и графовой формах. Инварианты и ограничения циклов. Анализ сетей Петри на основе дерева достижимости. Доказательство полной правильности программы. Суммы элементов диагоналей, параллельных главной диагонали матрицы.
Аннотация к работе
в сети Петри Основные определения Анализ сетей Петри ЛИНЕЙНАЯ СХЕМА ПРОГРАММ ССП в графовой форме Интерпретация Инварианты и ограничения циклов Доказательство частичной и полной правильности программы Анализ сетей Петри на основе дерева достижимости Сеть Петри Дерево достижимости Выводы по работе Список литературы Задание к курсовой работе 1. СПП в линейной форме представляет собой последовательность инструкций, которая строится следующим образом: 1. если выходная дуга начальной вершины с оператором start(х1,..., хn) ведет к вершине с меткой L, то начальной вершине соответствует инструкция: 0: start(х1,..., хn) goto L; 2. если вершина схемы S с меткой L - преобразователь с оператором присваивания х:=?, выходная дуга которого ведет к вершине с меткой L1, то этому преобразователю соответствует инструкция: L: x: =? goto L1; 3. если вершина с меткой L - заключительная вершина с оператором stop(?1,...?m), то ей соответствует инструкция L: stop(?1,..., ?m); 4. если вершина с меткой L - распознаватель с условием р(?1,...?k), причем 1-дуга ведет к вершине с меткой L1, а 0-дуга - к вершине с меткой L0, то этому распознавателю соответствует инструкция L: if р(?1,...?k) then L1 else L0; 5. если вершина с меткой L - петля, то ей соответствует инструкция L: loop.