Правила корректности и разрешимости КМ ВП.

В КМ ВП предусматривается проведение логического анализа ее корректности и разрешимости. Логический анализ классифицируется на:

статический анализ, под которым понимается проверка правильности синтаксических конструкций модели и обнаружение логических противоречий между структурами отношений различного типа;

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

Определение корректности структур отношений выполняется в ходе статического анализа (рис. 1):

рис. 1.

Анализ корректности имен объектов. Для любых двух объектах модели справедливо:

"o_i, "o_j, n_o(o_i) = n_o(o_j) ® t_ho(o_i) = t_ho(o_j) &

& "o_x , o_x Îh_o(o_i), $o_y , o_y Îh_o(o_j) & n_o(o_x) = n_o(o_y).

(если совпадают имена объектов, то должны совпадать типы их отношений иерархии и имена подчиненных им объектов).

Анализ корректности имен процессов. Для любых двух процессов модели справедливо:

"p_i, "p_j , n_p(p_i) = n_p(p_j) ® t_hp(p_i) = t_hp(p_j) &

& "p_x , p_x Îh_p(p_i), $p_y , p_y Îh_p(p_j) & n_p(p_x) = n_p(p_y) &

& "o_x , o_x Îin(p_i), $o_y , o_y Îin(p_j) & n_o(o_x) = n_o(o_y) &

& "o_z , o_z Îout(p_i), $o_w , o_w Îout(p_j) & n_o(o_z) = n_o(o_w).

(если совпадают имена процессов, то должны совпадать типы их отношений иерархии, имена подчиненных им процессов, входных и выходных по отношению к ним объектов).

Анализ корректности типов объектов. Если совпадают типы объектов, то должны совпадать типы их отношений иерархии, типы подчиненных им объектов (подобъектов), а также мощности множеств однотипных подобъектов.

Анализ корректности типов процессов. Если совпадают типы процессов, то должны совпадать типы их отношений иерархии, типы подчиненных им процессов (подпроцессов), мощности множеств однотипных подпроцессов, типы их входных и выходных объектов, а также мощности множеств однотипных входных и выходных объектов.

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

Анализ отношений взаимодействия. В модели не допускаются циклы, содержащие различные уровни иерархии процессов.

Анализ отношений следования. В модели отношения следования не могут:

связывать процессы, подчиненные друг другу отношениями иерархии;

задаваться "перекрестно" и противоречить друг другу.

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

Шаблоном КМ ВП относительно некоторого выбранного процесса p_i называется следующий набор множеств:

{p_j | p_jÎh_p(p_i)} – подчиненные p_i процессы;

{o_i | o_iÎin(p_i)} – входные объекты процесса p_i;

{o_j | o_jÎin(p_i)} – выходные объекты процесса p_i;

{o_k | o_kÎh_o(o_i), o_iÎin(p_i)} – компоненты входных объектов процесса p_i;

{o_l | o_lÎh_o(o_j), o_jÎout(p_i)} – компоненты выходных объектов процесса p_i;

{o_m | o_mÎin(p_k) V o_mÎout(p_k), p_kÎh_p(p_i)} – входные и выходные данные процессов, подчиненных p_i;

множества {o_i},{o_j},{o_k},{o_l},{o_m} могут частично пересекаться.

Шаблон КМ ВП называется корректно построенным, если он удовлетворяет условиям правилам статического анализа.

Модель, состоящая из корректно построенных шаблонов, обладает важным свойством: в ней каждому логическому уровню обработки данных соответствует свой логический уровень представления данных. В такой модели невозможны структуры, когда некоторый объект связывает процессы двух различных иерархических уровней обработки.

Введенное понятие позволяет сводить динамический анализ модели к анализу образующих ее шаблонов.

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