Здесь даны примеры визуализации импер-знаний на техноязыке и других типов знаний на иных языках, рассмотренных в документе. В каждом примере используется только один язык.
Содержание
Примитивы, силуэты и переходы между ними
Перевод разветвлённо-циклического визуала в ЦД
Графит-визуализация автоматной спецификации системы управления клапанами
Визуализация абстрактных типов
Абстрактные типы в Компонентном Паскале
Схемы оборудования исполнителей
Этот докэлемент находится здесь.
Этот докэлемент находится здесь.
Пример содержит выделенную графическую часть, доступную здесь. Для отсылки к иллюстрациям ГЧ в текст включены подрисуночные подписи.
Введение в предмет. Цикл Дейкстры (ЦД) — базовая циклическая конструкция структурной алгоритмики (в некоторых алго/прогязыках — единственная допустимая); определение ЦД в текстовой форме дано в ряде классических и современных работ1.
В информатической теории ЦД относят к классу т.н. универсальных программ — структур управления, через которые м.б. выражены любые другие структуры. Также ЦД используется в т.н. доказательном программировании (алгоритмизации). Так, ЦД является единственной конструкцией в языке Promela, используемом для спецификации систем совместно исполняемых программ по методу ModelChecking.
Языки, использующие ЦД, достаточно распространены сегодня. В частности, язык Promela является входным в ModelChecking-системе Spin. В связи с этим представляет интерес установления соотношения между ЦД и дракон-силуэтом.
Предварительные рассуждения. Вначале покажем структуру силуэта без упрощений, принятых в классическом техноязыке.
Визуализация дракон-силуэта (без упрощений, обобщённая)
В данном случае структура силуэта обобщена для переменного числа веток с использованием графических сокращений.
Прежде чем обсуждать свойства дракон-силуэта, определим термины и обозначения.
Введём нумерацию вершин схемы структурой, значения числовых элементов которой принадлежат множеству натуральных чисел, как показано на схеме.
Полученный индекс вершины будет отражать её координату в схеме; при этом первые два элемента определяют «абсциссу», а два следующих - «ординату» вершины. Оба измерения иерархически структурированы на «главный-побочный», поэтому для вершин главной вертикали побочные элементы индекса отсутствуют. Последний элемент индекса указывает порядок вершины по вертикали среди вершин своего типа.
Отметим, что порядок вертикали определяется по числу предшествующих развилок, которым не соответствуют точки слияния на той же вертикали (как бы открывающие скобки без закрывающих). Это становится существенно, в частности, для инверсной записи сложных ветвлений; в этом случае также меняется правило назначения вертикалей осям на обратное (наименее удалённая логически вертикаль ставится на самую дальнюю ось), чтобы избежать пересечений маршрутов.
Можно вводить нумерацию вершин по-разному, напр, как многоуровневый индекс вида:
i{.j}<t>k , где:
i — номер главной вертикали ветки цикла (справа налево);
J — номер побочной вертикали на оси удаления от главной (вправо) в порядке следования по оси (сверху вниз);
k - номер вершины в порядке следования по вертикали (сверху вниз).
Однако принятый синтаксис более нагляден и запись в нём легче контролируется человеком.
Индекс можно использовать как литер (абстракцию текста) иконы.
Можно задавать нумерацию вершины по-разному; так, можно указывать длину пути (в звеньях вертикали, т.е. без учёта точек ввода и изломов) до данной вершины от доминатора, т.е. начальной вершины вертикали; можно определять уровень вершины как нормированную длину пути (когда длины всех путей до данной вершины выравнены по максимальной из длин добавлением «пустых» номеров).
Упрощения техноязыка состоят в том, что структуры «разбора» и «сбора» на схемах показываются без обозначения т.н. древесных точек - вершин-узлов двоичных деревьев, каковыми эти структуры реально являются.
Мы показали эти вершины, т.к. это имеет значение для дальнейших рассуждений.
Совокупность рёбер, исходящих из точек слияния, в упрощённом начертании силуэта образует нижнюю горизонталь, далее называемую «землёй» (по аналогии с электросхемами).
Используемые здесь определения простого и сложного шампур-блока, шампур- и нешампур- икон см. /3, п/р 2.1/.
Для дальнейшего существенны следующие свойства силуэта:
1. Выбор текущего маршрута в петле силуэта задан иконами-границами Имя ветки и Адрес ветки , имеющими следующую семантику:
Адрес ветки имеет смысл команды безусловного перехода (БП) по координате, определяемой текстом иконы;
Имя ветки имеет смысл вычисления координаты вершины (дракон-иконы), следующей за этим оператором и подстановки координаты как текста каждой иконы Адрес ветки с совпадающим именем; фактически икона является меткой БП на следующую вершину.
Петля силуэта обобщает все возможные БП между ветками через «шапку» и «подвал». Для полной определённости реальных построений изначально считается, что ветки составляют цепочку; первой является левая ветка, а каждая последующая исполняется за соседней справа.
В техноязыке принято, что по умолчанию ветки исполняются слева направо.
Считаем, что текст икон-границ служит символическим (удобным для чтения человеком) значением адреса БП; предметным (реальным для введённой нумерации вершин) адресом служит номер ветки (точнее, первой вершины после имени, напр. по введённой выше нумерации).
При проходе каждой разветвительной вершины в петле действует неявное правило: если выход вниз не ведёт к нужной ветке, он игнорируется, а выбирается выход вправо.
Переходы из тела ветки в другую ветку не допускаются; топологически это значит, что не существует рёбер из вершины, лежащей внутри данной вертикали, к вершине, лежащей не на этой вертикали, т.е. индексы допустимых рёбер дракон-силуэта имеют одинаковое i для начальной и конечной вершин.
2. Силуэт показан обычным, или незацикленным. В таком силуэте крайняя правая ветка является конечной (обозначена индексом Z); ею завершаются маршруты схемы. Остальные ветки (1...N) являются полными, включёнными в «подвал» силуэта.
Полные ветки имеют один вход и один выход; такой силуэт называется линейным, или одноадресным.
Абстрагируясь от текста икон, можно полагать адреса БП любыми; в частности, адрес может указывать на имя более левой ветки, т.е. участок между разадресованными т.о. иконами «зацикливается».
Теперь введём на базе икон-границ ветки визуальные операторы Имя вертикали и Адрес вертикали (далее — просто Имя и Адрес) такие, что:
обе иконы включаются в схему парно цепочкой «Адрес-Имя» (т.е. в смысле шампур-метода образуют макроикону, которую будем называть Безусловный переход, или БП);
иконы м.б. вставлены в любое ребро дракон-схемы (в отличие от классического шампур-метода, где вставка возможна только в точку ввода звена вертикали);
между иконами БП не м.б. икон других типов;
возможно вложение БП, т.е. между иконами одного БП может находиться другой БП и т.д. (своего рода скобки, которые надо раскрывать по совпадению текстов имени и адреса);
возможно запараллеливание БП, т.е. тексты икон Адрес с разных маршрутов могут совпадать, указывая тем самым на одно имя.
Вложение БП, а также следование БП друг за другом м.б. сокращено (заменено на естественные переходы-звенья), если ни один из переходов не запараллелен с какими-то ещё БП.
Тексты икон в макроиконе БП (значения адреса) совпадают и уникальны в пределах схемы.
Переход на одно имя с разных адресов будем называть кратным.
Если визуализировать кратный БП «в лоб», то икона Адрес дублируется на обоих входящих вертикалях с одним именем, а икона Имя дублируется под каждой иконой Адрес с присоединением к одной и той же точек исходящей вертикали слияния. Однако дублирование иконы Имя здесь логически неоправданно и м.б. устранено; тогда два и более ребра БП с одноимённых адресов ведут к единственной иконе Имя.
Если считать адреса БП (тексты икон Адрес и Имя) константами (что справедливо для готового к исполнению перехода), то вложенные некратные БП м.б. непосредственно сокращены до одного БП (напр., внешнего). Вложение кратных БП, возможно, допускает сокращения, исходя из логики структуры маршрутов схемы, в которую такое вложение входит.
Если адреса БП считаются переменными, то это означает, что икона Имя помещает адрес в ячейку памяти, а икона Адрес берёт значение из одноимённой ячейки. При этом, очевидно, допустимо задать значение ячейки памяти адреса как присваивание результата некоторого арифметического выражения, включающего как переменные адреса, так и иные числовые величины алгоритма (программы). Такое выражение д.б. вычислено для исполнения перехода.
Макроикона БП м.б. подставлена вместо древесной точки слияния (соединительной вершины); рассмотрим эту возможность.
Результат подстановки показан на схеме справа в вынесенных областях (туннелями указано включение в силуэт).
Здесь в результате подстановки образуется повтор БП по вертикали, который также устраняется. Для этого необходимо сложное сокращение с участием всех БП, заменяющих точки слияния икон Адрес.
Кратные БП показаны несокращёнными (с дублированием имени). Это даёт возможность легко обосновать сокращение всей структуры «сбора»; достаточно оторвать БП, запараллеленный с более левой вертикалью, и включить его параллельно ветвям БП Цикл, изменив текст икон на принятый в этом переходе (в данном случае — Начало); очевидно, что после этого вышележащие переходы с этой вертикали (если они есть) можно убрать. Процедура повторяется для каждой вертикали правее, вплоть до правой крайней (для примера показан разрыв вертикалей 1 и 2 и подлежащий переносу БП12). В результате БП Цикл становится многократным; его иконы Имя сокращаются.
Схема показана уже с учётом устранения; области помечают те же участки, что вынесены.
Иконы Адрес внутри веток в объединении не участвуют, т.к. они логически относятся к охватывающей структуре переходов, связанной через «шапочный разбор». Однако эта связь неявная, через несформулированные условия разветвления; по сути, мы имеем в этой части чисто математический, неинформатизованный объект.
Также примем за аксиому следующую визуализацию цикла Дейкстры на классическом (в рамках определения Паронджанова в /1/) техноязыке (дракон-ЦД, далее — просто ЦД):
Визуализация цикла Дейкстры (ДРАКОН-1, обобщённая)
Структура ЦД показана с обобщениями, аналогичными силуэту. В данном случае структура ЦД обобщена для переменного числа ветвей цикла с использованием графических сокращений.
Обратим внимание, что конечная ветвь цикла, как и конечная ветка силуэта, ненагружена (имеет пустое тело); при этом условии мы и проводим наши рассуждения.
Одновременно справа показан результат сокращения представления «подвального сбора» через макроиконы БП; это представление м.б. отнесено и к силуэту, т.к. очевидно, что эта структура одинакова в обоих видах схем.
Видно, что дерево слияния на базе БП в цикле Дейкстры представляется так же, как в линейном силуэте выше.
Перепишем силуэт с подстановкой макроикон БП вместо точек слияния:
Визуализация дракон-силуэта (без упрощений, с нелинейностью тел веток)
На примере последней полной ветви также показаны случаи нелинейной структуры тела, существенные для дальнейшего рассмотрения.
Структура подвала также дана в уже сокращённом представлении через БП.
Очевидно, что на базе БП точка слияния перед шапкой представляется кратным БП, а каждая точка слияния м.б. представлена иконой Адрес с переходом на этот БП.
На схеме силуэта также можно трактовать иконы-границы веток как макроиконы БП. При этом адрес перехода (текст иконы Адрес в подвале силуэта) может иметь значение имени любой ветки того же силуэта (т.е. совпадать с текстом любой из икон Имя, входящей в шапку силуэта).
Видно, что при некоторых условиях можно перенести слияние из нелинейного тела ветки в подвал силуэта, создав переход по петле; это преобразование называется заземлением.
Силуэт с заземлениями (при любых допустимых значениях адресов БП) называется разветвлённым, или многоадресным. Полная ветка с заземлениями также называется многоадресной.
Очевидно, что у всех точек слияния многоадресной ветки есть общая вершина-доминатор на главной вертикали ветки из числа икон Вопрос. Эта вершина и вся часть ветки донизу образуют макроструктурный блок, называемый в техноязыке адресным. Понятно, что у адресного макроблока один вход (по шампуру) и несколько выходов (один по шампуру и одна или более по заземлённым вертикалям).
В зависимости от проведённых заземлений доминатор может оказаться первой иконой Вопрос в ветке; если перед ней ещё и отсутствуют другие иконы, то всё содержимое ветки становится адресным макроблоком. Не нарушая общности, можно считать тело многоадресной ветки адресным блоком в любом случае.
Если абстрагироваться от текста икон, то адрес БП м.б. любым. Для полной определённости операции изначально считается, что БП с заземлённой вертикали дублирует переход с конца главной вертикали (на начало той же ветки, что и БП с главной). Впоследствии адрес дублирующего БП (текст его иконы Адрес) м.б. изменён на текст любой иконы Имя, входящей в шапку силуэта.
Если адрес не изменён, то полученный БП считается кратным.
На схеме мы показываем тела других полных веток как шампур-блоки; конечно, в общем случае любая ветка может стать многоадресной (а её тело — адресным блоком), как только в ней заземлена хотя бы одна вертикаль.
На схеме также показаны (толстым штрихпунктиром) результаты допустимых заземлений для нелинейной структуры тела ветки; тем самым получаем «квазидинамическую» схему.
Видно, что заземление одних вертикалей открывает путь к заземлению других (охватываемых) вертикалей. Очереди выполнения обозначены разной яркостью линий (второочередное заземление показано более блёклым). Также индексы точек слияния, связанных со второй очередью заземления, показаны смещёнными вправо, чтобы выделить их.
Заземление без пересечения маршрутов (запрещённого в техноязыке) возможно, если точку слияния побочной вертикали не отделяют от точки слияния веток операторные вершины (иконы) и/или точки слияния охватывающих (лежащих правее, т.е. на оси порядка с большим номером) вертикалей.
Интуитивно ясно, что при заземлении создаётся ребро на оси порядка, которой принадлежит заземляемая вертикаль, и точка слияния этого ребра с «землёй» силуэта, а в подвал добавляется икона Адрес ветки, через которую ребро сращивается с этой вертикалью. Т.о. дерево «сбора» наращивается по оси порядка заземляемой вертикали.
Имеются и топологические особенности выполнения операции. Так, если вертикаль на оси не нижняя, то для неё создаётся новая ось порядка (а вершины вертикали и всех, лежащих правее, если таковые имеются, перенумеруются). Если заземляемая вертикаль не крайняя (т.е. правее уже есть хотя бы одна заземлённая вертикаль), то точка слияния делит ребро «земли», ведущее к этой вертикали; если заземляемая вертикаль крайняя, то точка слияния включается в вертикальное ребро левее.
Какова бы ни была структура тела ветви до и после заземления вертикали, вне тела эффект этой операции всегда одинаков и состоит в ветвлении дерева «подвального сбора» . Собственно, именно этот эффект мы и должны учитывать в наших рассуждениях.
Вообще для выполнения заземлений в нелинейной шампур-структуре с учётом введённой индексации вершин можно сформулировать следующие общие правила:
если на одной оси порядка находятся две и более вертикали, не разделённые петлями цикла, то их заземление независимо друг от друга, т.е. равно возможно или невозможно;
если осей порядка в теле ветки более двух, то заземление каждой более левой побочной вертикали возможно, только если уже заземлены все охватывающие (более правые и с точкой слияния ниже по уровню, чем у данной) вертикали и нет петли цикла, начинающейся на оси левее и от развилки ниже по уровню, чем точка слияния, участвующая в заземлении;
без изменения структуры маршрутов возможно заземлить только такую вертикаль, между исходной точкой слияния которой и линией «земли» нет икон (и не м.б. точки слияния других вертикалей во избежание пересечения).
Понятно, что шампур (главная вертикаль) считается изначально заземлённым; его точка слияния как раз лежит на линии «земли» силуэта.
Преобразуем схему ЦД к виду, где вертикали ограничены сверху и снизу безусловными переходами. Для этого в начало и конец каждой вертикали ветви включим макроикону БП; при этом началом побочной вертикали считаем точку излома с побочного выхода предшествующей иконы Вопрос, концом, как и выше для силуэта — древесную точку слияния. В качестве адреса начального БП используем номер начинаемой им ветви ЦД. Вершины занумеруем также, как ранее в силуэте. Полученная структура показана на схеме:
Цикл Дейкстры с введением БП-границ вертикалей и нелинейностью тел ветвей
В данном случае мы показали концевые БП уже сокращёнными (включая границы заземлённых вертикалей).
В последней ветви ЦД воспроизведена разветвлённая структура, аналогичная показанной в силуэте. Заземления вертикалей, там лишь намеченные, здесь показаны как осуществлённые.
Также показано, что можно «разземлить» ранее заземлённую вертикаль; это разновидность операции, в техноязыке называемой пересадкой.
Содержание этой операции для нас несущественно; отметим лишь, что вертикаль снова м.б. перемещена на другую ось порядка. Если исходная ось при этом станет пустой, то она подлежит сокращению, а все более правые оси и лежащие на них вершины — перенумерации.
Часть схемы, начинающаяся доминатором развилки пересаженной вертикали и заканчивающаяся точкой слияния вертикали, куда произведена пересадка, с вертикалью, на которой выделен доминатор, является также макроструктурным блоком особого типа; в техноязыке он назывется лианным. В пределе лианный макроблок выделяется по шампуру.
Любой шампур-блок, в котором не было пересадок и заземлений, является т.н. структурным макроблоком; можно также называть его атомарным, т.к. он образуется исключительно операциями над атомами шампур-метода.
Может показаться, что наличие заземлений нарушает логику цикла Дейкстры. Однако все переходы по слиянию замыкаются на БП Цикл, т.е. остаются в петле цикла. Формально мы можем считать, что все точки слияния побочных вертикалей одной ветви входят в тело этой ветви. Можно рассматривать полученную конструкцию как обычный ЦД, тело ветви которого завершается развилкой; каждая ветвь развилки, соответствующая заземлённой вертикали, в свою очередь, содержит переход на закрывающую операторную скобку ЦД.
Также проведём следующие очевидные сокращения БП в полученной схеме. Дело в том, что ЦД со введёнными границами оказывается операторно избыточен; иконы Адрес <ИмяСлВет*> в конце тел выполняют ту же роль, что условия «Повторить ветвь * ?» — выбор нужной ветви. Поэтому можно сократить эту часть схемы следующим образом:
Убрать икону Имя ветки <ИмяВетки1> в БП Цикл.
Внести БП Цикл (икону Адрес <Начало>) на место убранной.
Убрать иконы Адрес <ИмяСлВет*> над «подвальным сбором», которые в роли границ ветвей теперь избыточны (заменяются переходами по <Начало>); в роли же представления точек разветвления заменяются выбором по условию.
Кратный БП Цикл тем самым оказывается частично принадлежащим первой ветви (на схеме сокращаемые иконы имеют пунктирный контур).
Полученная структура показана на схеме:
Цикл Дейкстры с сокращёнными БП-границами вертикалей
Здесь мы уже не показываем пересадку.
Следствие. Если преобразовать т.о. схему ЦД (и вообще любую нелинейную дракон-схему) полностью (т.е. ввести макроиконы БП как границы в каждую вертикаль схемы), то полученная схема допускает размещение по одной координате с сохранением структуры управления. Для этого ограниченные иконами БП вертикали выкладываются по одной оси порядка, а затем в качестве адресов БП используются координаты (линейные порядковые номера) икон Имя вертикали по этой оси (каждой иконе отводится один номер).
Результирующую схему будем называть лиоформой визуального алгоритма; очевидно, что она является визуализацией алгоритма на уровне команд абстрактной машины для переработки данных (модели информатической машины), имеющей линейно адресуемую память; примером м.б. машина Тьюринга. В этом случае каждая шампур-икона должна представлять одну команду машины, за исключением рассмотренных ниже случаев:
1. Икона Имя вертикали трактуется как метка, устанавливаемая на икону-команду, следующую за ней по шампуру.
2. Икона Адрес вертикали в комбинации с иконой Вопрос, выделенной для примера в ветви 1 схемы, интерпретируется как команда ветвления (условного перехода) либо на следующую по шампуру икону-команду, либо на икону Имя вертикали с совпадающим текстом (т.е. по адресу, указанному в иконе Адрес); в иных случаях икона Адрес трактуется самостоятельно как команда безусловного перехода.
Сформулируем теперь следующее утверждение.
Утверждение. Любой силуэт с ненагруженной конечной веткой м.б. преобразован в цикл Дейкстры с чисом ветвей, равным числу полных веток силуэта, с сохранением структуры управления (множества возможных маршрутов).
Доказательство. Выделим в цикле Дейкстры команды ветвления, как показано на схеме выше. Очевидно, что каждая команда ветвления представляет древесную точку разветвления с явно сформулированным условием ветвления; однако условие теперь д.б. информатизовано так, чтобы выбирать нужный маршрут, не опираясь на безусловные переходы.
Примем логическим критерием выбора очередной ветви маршрут выхода из предыдущей ветви (т.е. ось порядка, через которую проследовали в «подвал»). В связи с этим введём переменную ИмяВетви, значением которой будет имя (номер) ветви, подлежащей выбору при очередной итерации ЦД. Также установим, что значение ИмяВетви формируется оператором присваивания номера ветви, подлежащей выбору; данный оператор входит в вертикаль текущей итерации, заземлённую на подвал ЦД, перед точкой её слияния с «землёй».
При этих условиях условие выбора ветви в каждой иконе Вопрос шапки ЦД можно сформулировать в виде:
ИмяВетви = <ИмяСлВет>i ? ,
где i — номер вертикали по введённой индексации вершин.
Полученная структура показана на схеме:
Цикл Дейкстры с выбором ветви по переменной ИмяВетви
Здесь мы также условно показываем заземления вертикалей.
Число показываемых ветвей сокращено до трёх (включая ветвь-эллипсис), чтобы схема была менее громоздкой.
Также проведём следующие очевидные сокращения БП в полученной схеме. Дело в том, что ЦД со введёнными границами оказывается операторно избыточен; иконы Адрес <ИмяСлВет*> в конце тел выполняют ту же роль, что условия совместно с присваиваниями по ИмяВетви — выбор нужной ветви. Однако они требуются для линейной выкладки — границ снизу по БП Цикл (адресу <Начало>) недостаточно. Поэтому можно сократить эту часть схемы следующим образом:
Заменить значение иконы Адрес <Начало> в «подвальном сборе» и в БП Цикл на <ИмяВетки1>.
Убрать икону Имя ветки <Начало> в БП Цикл.
Убрать иконы Адрес <ИмяСлВет*> под присваиваниями, которые в роли представления точек разветвления теперь заменяются выбором по присвоенному значению, а в роли границ ветвей — переходами по <ИмяВетки1>.
Кратный БП Цикл тем самым оказывается частично принадлежащим первой ветви (на схеме сокращаемые иконы имеют пунктирный контур).
Полученная структура показана на схеме:
Цикл Дейкстры по переменной ИмяВетви с сокращением БП-границ вертикалей
Понятно, что мы просто сделали выбор ветви явным, зависящим от одной конкретной переменной алгоритма.
Теперь возьмём ранее показанный разветвлённый силуэт и подставим на место каждой точки разветвления команду ветвления из предыдущей схемы ЦД (только переменную назовём ИмяВетки). Одновременно включим операторы присваивания номеров переменной ИмяВетки также, как для переменной ИмяВетви в ранее рассмотренном ЦД.
Полученная структура показана на схеме:
Дракон-силуэт с подстановкой команд ветвления по ИмяВетки
Число рассматриваемых веток также сокращено до трёх, как для ЦД по ИмяВетви.
Полученную схему теперь преобразуем по следующим направлениям.
1. Видно, что икона Имя <Имя ветки*> на шампуре каждой полной ветки повторяется, что создаёт неопределённость перехода; оставим икону только перед командой ветвления.
Возникает вопрос: каковы основания такого решения? Дело в том, что значение данной иконы — пометить начало ветки. В то же время каждая заменяемая нами точка расщепления и топологически сопоставлена конкретной ветке (предшествуя ей по шампуру), и функционально реализует её выбор или невыбор и ничего более; следовательно, не будет ошибкой логически объединить её с этой веткой; тогда и начало ветки можно принять перед командой ветвления, заменяющей точку (а по сути, информатизующей эту точку).
Можно получить тот же результат и иначе, включив икону в содержание подстановки перед командой ветвления и одновременно определив областью подстановки и точку расщепления, и следующую за ней икону Имя <Имя ветки*>.
2. Заменим в дереве «сбора» точки слияния на иконы БП, как обсуждалось ранее. Адреса в иконах концевых БП в рассматриваемых ЦД и силуэте задаются аналогично по определению.
Полученная структура показана на схеме:
Дракон-силуэт с подстановкой команд ветвления и заменой точек слияния
Видно, что тем самым в каждой ветке силуэта образуется начальный БП, как в ветви ЦД; заменим адреса переходов в макроиконах этих БП по тому же правилу, что для ЦД.
3. По выполнении п. 2 в схеме возникает операторная избыточность по БП, как в ЦД по переменной ИмяВетви; иконы Адрес <ИмяСлВет*> в конце тел выполняют ту же роль, что условия совместно с присваиваниями по ИмяВетви — выбор нужной ветви. Сократим избыточность, как обсуждалось для схемы ЦД по ИмяВетви.
На схеме подлежащие сокращению иконы имеют пунктирный контур.
Полученная структура показана на схеме:
Дракон-силуэт с заменой точек разветвления и слияния и сокращением БП-границ
Видно, что получена структура цикла Дейкстры по переменной ИмяВетки (значениями которой здесь являются номера веток силуэта); тем самым утверждение доказано для данного случая. В свою очередь этот случай введён как обобщение любых возможных ситуаций формирования структуры управления и в ЦД, и в дракон-силуэте.
Процедура доказательства одновременно есть процедура преобразования силуэта в цикл Дейкстры. Очевидно, что возможно и обратное преобразование.
Этот докэлемент находится здесь.
Этот докэлемент находится здесь.
Этот докэлемент находится здесь.
Этот докэлемент находится здесь.
Этот докэлемент находится здесь.
В начало страницы | Оглавление | Главная | Версия для печати
Copyright © Жаринов В.Н.
1См., напр: Вирт Н., 2010. - Приложение С; Карпов Ю.Г. Model Checkng. Верификация параллельных и распределённых программных систем. - СПб.: БХВ-Петербург, 2010. - С.200.