Development and substantiation of algorithms based on semantic properties

Development and substantiation of algorithms based on semantic properties

Examples of the development and validation of algorithms based on the use of the domain properties are shown. These properties are formulated in terms of semantic relationships that characterize the subject area of the developed algorithm.Prombles in programming 2014; 2-3: 151-159

Gespeichert in:
Bibliographische Detailangaben
Datum:2025
Hauptverfasser: Kryvyi, S.L., Maksymets, O.M.
Format: Artikel
Sprache:Russian
Veröffentlicht: PROBLEMS IN PROGRAMMING 2025
Schlagworte:
UDC 51.681.3
Online Zugang:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/706
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Institution

Problems in programming
id pp_isofts_kiev_ua-article-706
record_format ojs
resource_txt_mv ppisoftskievua/14/0c7ff4895d8bd3bbf7d8e4079afb7514.pdf
spelling pp_isofts_kiev_ua-article-7062025-04-09T22:22:32Z Development and substantiation of algorithms based on semantic properties Разработка и обоснование алгоритмов на основе семантических свойств Kryvyi, S.L. Maksymets, O.M. UDC 51.681.3 УДК 51.681.3 Examples of the development and validation of algorithms based on the use of the domain properties are shown. These properties are formulated in terms of semantic relationships that characterize the subject area of the developed algorithm.Prombles in programming 2014; 2-3: 151-159 Приводятся примеры разработки и обоснования алгоритмов на основе использования свойств предметной области. Эти свойства формулируются в виде семантических соотношений, характеризующих предметную область разрабатываемого алгоритма.Prombles in programming 2014; 2-3: 151-159 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-04-09 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/706 PROBLEMS IN PROGRAMMING; No 2-3 (2014); 151-159 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 2-3 (2014); 151-159 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 2-3 (2014); 151-159 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/706/758 Copyright (c) 2025 PROBLEMS IN PROGRAMMING
institution Problems in programming
baseUrl_str https://pp.isofts.kiev.ua/index.php/ojs1/oai
datestamp_date 2025-04-09T22:22:32Z
collection OJS
language Russian
topic
UDC 51.681.3
spellingShingle
UDC 51.681.3
Kryvyi, S.L.
Maksymets, O.M.
Development and substantiation of algorithms based on semantic properties
topic_facet
UDC 51.681.3

УДК 51.681.3
format Article
author Kryvyi, S.L.
Maksymets, O.M.
author_facet Kryvyi, S.L.
Maksymets, O.M.
author_sort Kryvyi, S.L.
title Development and substantiation of algorithms based on semantic properties
title_short Development and substantiation of algorithms based on semantic properties
title_full Development and substantiation of algorithms based on semantic properties
title_fullStr Development and substantiation of algorithms based on semantic properties
title_full_unstemmed Development and substantiation of algorithms based on semantic properties
title_sort development and substantiation of algorithms based on semantic properties
title_alt Разработка и обоснование алгоритмов на основе семантических свойств
description Examples of the development and validation of algorithms based on the use of the domain properties are shown. These properties are formulated in terms of semantic relationships that characterize the subject area of the developed algorithm.Prombles in programming 2014; 2-3: 151-159
publisher PROBLEMS IN PROGRAMMING
publishDate 2025
url https://pp.isofts.kiev.ua/index.php/ojs1/article/view/706
work_keys_str_mv AT kryvyisl developmentandsubstantiationofalgorithmsbasedonsemanticproperties
AT maksymetsom developmentandsubstantiationofalgorithmsbasedonsemanticproperties
AT kryvyisl razrabotkaiobosnovaniealgoritmovnaosnovesemantičeskihsvojstv
AT maksymetsom razrabotkaiobosnovaniealgoritmovnaosnovesemantičeskihsvojstv
first_indexed 2025-07-17T10:08:35Z
last_indexed 2025-07-17T10:08:35Z
_version_ 1850411372324585472
fulltext Формальні методи програмування © С.Л. Крывый, А.Н. Максимец, 2014 ISSN 1727-4907. Проблеми програмування. 2014. № 2–3. Спеціальний випуск 151 УДК 51.681.3 РАЗРАБОТКА И ОБОСНОВАНИЕ АЛГОРИТМОВ НА ОСНОВЕ СЕМАНТИЧЕСКИХ СВОЙСТВ С.Л. Крывый, А.Н. Максимец Киевский национальный университет им. Тараса Шевченко, 03680, Киев, проспект Глушкова, 2, корпус 6, E-mail: maksymets@gmail.com Приводятся примеры разработки и обоснования алгоритмов на основе использования свойств предметной области. Эти свойства формулируются в виде семантических соотношений, характеризующих предметную область разрабатываемого алгоритма. Examples of the development and validation of algorithms based on the use of the domain properties are shown. These properties are formulated in terms of semantic relationships that characterize the subject area of the developed algorithm. Введение Проблема разработки и обоснования алгоритмов и создания на их основе эффективных программ являет- ся одной из основных на пути построения надежного программного обеспечения. Актуальность этой проблемы особенно остро встала в последние десятилетия в связи с постоянным возрастанием сложности и объемов про- граммного обеспечения. Такой интерес к данной проблеме связан еще и с тем, что программирование становит- ся индустрией, в которой задействовано огромное количество людей. Одно из центральных мест среди задач решения данной проблемы занимает проблема обоснования правильности функционирования алгоритмов. Ко- гда речь заходит о построении надежного программного обеспечения, то это значит, что оно правильно решает поставленную задачу. Однако, очень часто эффективность сильно влияет на прозрачность и понятность про- граммного обеспечения. Это связано с тем, что эффективность, как правило, достигается за счет более глубоких и потому менее очевидных свойств предметной области. В общем случае эти проблемы решить невозможно из- за их алгоритмической неразрешимости, но ввиду их актуальности появились многочисленные направления частичного решения этой проблемы: тестирование [1], абстрактные интерпретации [2, 3], проверка на моделях [4], сетевые методы [5], логические методы (программные динамические логики и логика Хоара) [6] и т. д. Предварительные сведения Абстрактные типы данных. Хорошо известно, что процесс разработки программного обеспечения в упрощенном виде можно схематически представить (рисунок). Рисунок. Схема процесса разработки В неформальном описании алгоритма решения прикладной задачи приходится использовать типы дан- ных присущие рассматриваемой математической модели. Данные такого типа не всегда принадлежат языку программирования и называются абстрактным типом данных (АТД). В программировании различают понятия АТД, структура данных и тип данных. Под АТД понимают некоторую формальную математическую модель вместе с операциями, функциями и предикатами, определенными на этой модели. Примером такого типа дан- ных могут служить множества, вместе с операциями объединения, пересечения и дополнения. В модели АТД операторы могут иметь операндами не только данные, которые определяются этим АТД, но и операнды языка программирования и операнды, определяемые другими АТД. Результатом выполнения оператора тоже может быть тип данных, который не определяется данным АТД. Но в рамках данного АТД предполагается, что по крайней мере один операнд или результат выполнения любого оператора имеет тип данных, определенный в данной модели АТД. Отсюда следует, что математическая модель предметной области представляет собой мно- гоосновную алгебраическую систему. АТД отличаются от структур данных языков программирования тем, что при использовании АТД аб- страгируются от способа их реализации и учитывают только их свойства. Использование АТД позволяет разра- батывать алгоритмы и программы, базируясь на свойствах их операций и предикатов с последующим выбором наиболее эффективного способа их реализации. Формальні методи програмування 152 Например, при построении алгоритмов манипуляции с полиномами как АТД одной из основных опера- ций на полиномах является операция сложения полиномов и . Для реализации этой операции можно выбрать представление полиномов в памяти компьютера в виде массивов коэффициентов. Могут быть выбраны и дру- гие интересные способы представления полиномов, но независимо от этого представления свойства операции сложения такие, как коммутативность, ассоциативность и свойства операции умножения полинома на констан- ту, не изменяются, какой бы способ представления не был выбран. Другими известными примерами АТД явля- ются множества, графы, матрицы, векторы, отображения и т. д. Семантические свойства. Из приведенной на рисунке схемы следует, что процесс разработки состоит из двух этапов: на первом строится алгоритм, а на втором – программа по этому алгоритму. Учитывая это бу- дем различать семантические свойства двух типов: – свойства предметной области (ПО), – свойства реализации АТД, с помощью которых построен алгоритм. Заметим, что разделение свойств осуществляется и на этапе компиляции и отладки программ [7]. Сформулируем понятие семантического свойства, относящегося к той или иной предметной области. Семантические свойства носят первичный характер в том смысле, что они должны выполняться независимо от способов реализации АТД. Следовательно эти свойства должны согласовываться с семантикой языка програм- мирования, в котором будет реализовываться программа. А отсюда следует, что семантические свойства ПО должны быть вычислимыми. Таким образом, приходим к такому определению. Определение 1. Под семантическим свойством предметной области nDDDD  21= будем пони- мать соотношение DzyxR ),,,(  , которое выполняется (возможно при некоторых ограничениях) для любых значений переменных zyx ,,,  из области D (удовлетворяющих этим ограничениям) и которое согласовано с семантикой реализации АТД, с помощью которых представлено это свойство. Например, упомянутая выше операция сложения полиномов имеет семантические свойства коммутатив- ности и ассоциативности сложения. А представление АТД "полином" в виде векторов коэффициентов со свой- ствами этой реализации, относятся к семантическим свойствам реализации этого АТД. Эти свойства будут дру- гими в случае реализации полиномов значениями в заданных точках nczcycx =,,=,= 21  из области D . Учитывая, что процесс разработки алгоритмов и программ носит творческий характер, общих рекомен- даций для реализации этого процесса не существует. Однако, часто из удачно сформулированного семантиче- ского свойства непосредственно вытекает алгоритм. Примерами таких свойств являются рекурсивные опреде- ления и рекуррентные соотношения. Если такие определения и соотношения найдены, то возникает вопрос об эффективности получаемого алгоритма. Далее рассматриваются три известных алгоритма с обоснованием их правильности на основе свойств предметной области. Первый из них – это алгоритм вычисления наибольшего общего делителя двух чисел. Второй – алгоритм построения топологической сортировки, эффективность которого достигается путем пере- хода в другую предметную область. Третий рекурсивный алгоритм обхода неориентированного графа в глуби- ну и его модификации на основе семантических свойств и свойств реализации АТД граф. Алгоритм вычисления наибольшего общего делителя Примером семантического соотношения, из которого непосредственно получается алгоритм, является семантическое свойство функции вычисления наибольшего общего делителя (НОД) двух натуральных чисел. Пусть Nnm , и существует Nx такое, что m и n кратны x . В таком случае число x называется общим делителем чисел m и n . Наибольший среди всех общих делителей называется наибольшим общим де- лителем чисел m и n (НОД( nm, )). Следующие свойства отношения делимости хорошо известны: i1) НОД( nm, ) = НОД( mn, ), i2) НОД( nm, ) = n , если nm = , i3) НОД( nm, ) = НОД( nnm , ), если nm > и i4) НОД( nm, ) = НОД( mmn , ), если nm < . Свойства i3) и i4) можно записать более компактно: i5) НОД( nm, ) = НОД( ),(min|,| nmnm ), если nm = . Это соотношение и составляет одно из семантических свойств ПО N . Из него видно, что функция НОД является частично рекурсивной (она даже примитивно рекурсивная), т.е. она вычислима, и из него непосред- ственно следует алгоритм вычисления НОД двух натуральных чисел, написанный в псевдокоде, для этого АТД. НОД( nm, ) Вход: integer nm, . Формальні методи програмування 153 Выход: НОД ).,( nm Метод: 1. ma := ; nb := ; 2. while ba = do 2.1. if ba > then baa := else abb := od 3. return ( a ). Вышеприведенные свойства функции НОД гарантируют правильность этого алгоритма. Этот алгоритм эффективный в случае относительно небольших значений аргументов при использовании десятичной системы счисления. В случае больших значений аргументов более эффективным является так называемый бинарный алгоритм вычисления НОД Название этого алгоритма обосновывается тем, что как его аргументы, так и опера- ции над ними представляются в двоичной системе счисления. Бинарный-НОД( nm, ) Вход: integer nm, . Выход: НОД ).,( nm Метод: 1. 1:=d ; 2. while m and n are even do 2.1. ( ddnnmm 2:=/2;:=/2;:= ); od 3. while 0=m do 3.1. while m is even do /2:= mm ; od 3.2. while n is even do /2:= nn ; od 3.3. /2|:=| nmt  ; 3.4. if nm  then tm := else tn := ; od 4. return ( nd  ). Этот алгоритм уже требует обоснования правильности, поскольку выполнение основных свойств НОД не очевидны. Для этого воспользуемся свойствами НОД, которые непосредственно вытекают из вышеприве- денных: пусть 11 =,= npnmpm lk , где 0=p , тогда i6) НOД( nm, ) = lp НOД( 11,nmp lk ) = = lp НOД( 11,nm ), если kl < , i7) НOД( nm, ) = kp НOД( 11, npm kl ) = = kp НOД( 11,nm ), если lk < . В нашем случае 2=p и после выполнения оператора 2 возникает две возможности: а) ld 2= , 11 2= mm lk  и 11 = nn  ; б) kd 2= , 11 = mm  и 11 2= nn kl  . В силу свойств i6) и i7) в обоих случаях получаем НОД( 11 ,  nm ) = НОД( 11,nm ). Уничтожение множителей l2 и k2 выполняют операторы 3.1 и 3.2, после чего для новых значений 1m и 1n необходимо вычислить их НОД. Это вычисление выполняется в теле оператора 3. После выполнения операторов 3.3 о 3.4 для новых значений 1m и 1n имеем: НОД( 11 ,  nm )=НОД( 111 | ,| nnm  ) = НОД( 11,nm ), если 11 > nm ; НОД( 11 ,  nm )=НОД( 111 | ,| mnm  ) = НОД( 11,nm ), если 11 < nm . Следовательно, соотношение НОД( 11,nm ) = НОД( 11 ,  nm ) является инвариантом цикла, который реали- зует оператор 3. Остается заметить, что когда 0=1m , то это будет тогда и только тогда, когда 0|==| 11   nmt на предыдущем шаге, т. е. когда 11 =  nm . Но в силу i2) НОД( 111 =),  nnm , а после выполнения оператора 4 окон- чательно получаем НОД( nm, ) = d НОД( 11,nm ) = 1nd , что и нужно было доказать (таблица). Формальні методи програмування 154 Таблица Шаг m n Шаг m n d 1 1424 850 1 1424 850 1 2 574 850 2 712 425 2 3 574 276 3 89 425 2 4 298 276 4 89 336 2 5 22 276 5 89 21 2 6 22 254 6 17 21 2 7 22 232 7 17 1 2 8 22 210 8 16 1 2 9 22 188 9 1 1 2 10 22 166 10 НОД 2=),( nm 11 22 144 12 22 122 13 22 100 14 22 78 15 22 56 16 22 34 17 22 12 18 10 12 19 10 2 20 8 2 21 6 2 22 4 2 23 2 2 НОД( nm, )=2 Пример 1. Приведем результаты вычисления НОД первым и вторым алгоритмами в предположении представления чисел в двоичной системе исчисления. Первый алгоритм требует выполнения 46 сравнений и вычитаний, а второй – 18 сравнений и вычитаний, поскольку деление на 2 в двоичной системе представления чисел выполняется за константу, которая не зависит от величин чисел-аргументов. Алгоритм топологической сортировки Рассмотрим второй пример алгоритма, который использует другие АТД для своей реализации. Это алго- ритм топологической сортировки, который вкладывает частичный порядок в линейный. В отличие от преды- дущего алгоритма для этого алгоритма нельзя сформулировать семантическое свойство, из которого бы он вы- текал. Для того чтобы сформулировать семантические свойства ПО, необходимо выходить в область теории графов. Приведем необходимые пояснения. Определение 2. Отношение линейного порядка  на конечном множестве A называется топологиче- ской сортировкой отношения частичного порядка 1 на этом множестве, если для любых элементов Aba , из ba 1 следует ba  . Из определения вытекает такое семантическое соотношение baba 1 , используя которое можно построить такой алгоритм топологической сортировки: найти минимальный элемент в множестве A и занести его в список линейно упорядоченных элементов; удалить минимальный элемент из множества A и повторить предыдущий шаг, если оставшееся множество A не пусто. Однако, анализ сложности такого алгоритма пока- зывает его низкую эффективность с точки зрения времени выполнения. Поиск более эффективной реализации приводит к необходимости перехода в другую предметную область – область ациклических графов. Известно, что отношение частичного порядка на конечном множестве A представляется в виде диаграммы Гассе, которая Формальні методи програмування 155 является ациклическим орграфом ),(= EVG (DAG – directed acyclic graph). Тогда топологическая сортировка сводится к линейному упорядочению вершин ациклического орграфа таким образом: если существует дуга из вершины v в вершину u в графе G , то в искомом линейно упорядоченном списке вершин орграфа вершина v предшествует вершине u . Это и есть трансформация семантического отношения baba 1 в терминах нового АТД, которым является ациклический граф. В терминах этого АТД алгоритм топологической сортировки принимает вид: TOPSORT( ),(= EVG ) begin for each Vv do }),(|{=)( EvuVuvInbuild  ; od VV := ;  :=V ; while  =V do Vfromutake  ; if =)(uIn then }{\:= uVV  ; }{:= uVV  ; for each Vv do }{\)(:=)( uvInvIn ; od else (STOP: G is not DAG) (* добавленная часть *) fi od end Независимо от того, как будут реализованы множества, фигурирующие в этом алгоритме, сам алгоритм остается неизменным. Но реализация АТД "множество" сильно влияет на эффективность данного алгоритма. Простой анализ показывает, что множества V  и V  следует реализовывать в виде очередей. Причем, вершины с пустыми множествами )(vIn лучше размещать на одном из концов очереди, а множества )(vIn реализовывать с помощью хеш-таблиц. Покажем правильность алгоритма и приведем оценку его временной сложности. Пусть множества V  и V  реализованы в виде очередей, причем вершина Vv  переносится на левый конец очереди V  , как только )(vIn становится пустым множеством. Выбор элементов из очереди V  выполня- ется слева, а добавление элементов в очередь V  выполняется с правого конца. Для доказательства правильности алгоритма необходимо показать: а) что когда uv 1 (т. е. из вершины v к вершине u существует путь в графе G ), то в множестве V  вершина v предшествует вершине u ; б) что все вершины графа G присутствуют в списке V  . Доказательство пункта а) достаточно очевидно, поскольку если vv 1 , то это значит, что )(uIn вклю- чает вершину v . Но тогда вершина u не попадет в список V  до тех пор, пока из множества )(uIn не будут удалены все вершины (а, значит, и вершина v ). Следовательно, вершина v появится в списке V  раньше вер- шины u , а это значит, что uv  . Доказательство пункта б) связано с анализом ситуации, когда некоторая вершина u не попадает в спи- сок V  . Это возможно только тогда, когда =)(uIn , что значит наличие цикла в исходном графе G . Действи- тельно, если =)(uIn , то существует вершина v в графе G принадлежащая к )(uIn и не удаляемая из этого множества в процессе выполнения алгоритма. Но это означает, что и =)(vIn и тогда вершины u и v связа- ны между собой маршрутом, который образует цикл. Таким образом, для правильности работы алгоритма TOPSORT необходимо внести в алгоритм проверку ацикличности исходного графа. При заданной организации выбора элементов из очереди V  из этого множе- ства всегда выбирается вершина u с пустым множеством )(uIn . Если такого элемента не окажется, то это и будет означать наличие цикла в исходном графе. С этой целью в алгоритм добавлена часть else в условный оператор, входящий в тело цикла while . Пример 2. Применим этот алгоритм к решению такой задачи. Пусть hgfedcba ,,,,,,, означают курсы, которые должны быть прочитаны лекторами кафедры. Формальні методи програмування 156 Порядок зависимости курсов определяется с помощью ациклического орграфа ),(= EVG , который по- казан на рис. 1. Необходимо найти последовательность чтения курсов с учетом их зависимости. Рис. 1. Порядок зависимости курсов После выполнения оператора for получаем такую последовательность множеств )(vIn : =)(hIn , }{=)( hcIn , }{=)( cbIn , }{=)( baIn , }{=)( cdIn , }{=)( cgIn , }{=)( efIn , },{=)( gdeIn . Согласно расположению элементов в очереди V  первым элементом в ней всегда должна быть вершина v , у которой =)(vIn . Дальнейшее выполнение алгоритма TOPSORT дает такую последовательность чтения курсов: feagdbch ,,,,,,, . Это одна из возможных последовательностей, поскольку на некоторой итерации цикла while возможен выбор. Например, после обработки вершин h и c , кандидатами на выбор стают вершины gdb ,, (алгоритм выбрал вершину b ). Если применить модифицированный алгоритм TOPSORT к орграфу 1G , то он обнаруживает что орграф 1G не ациклический. Алгоритм обхода графа в глубину Рассмотрим третий способ построения алгоритмов с помощью рекурсии, а именно – алгоритм обхода вершин графа в глубину. Этот алгоритм хорошо известен и называется DFS-алгоритмом (DFS – depth first search). Перед представлением этого алгоритма, напомним некоторые определения из теории графов. Неориен- тированный граф называется связным, если между произвольными его вершинами существует маршрут. Оче- видно, что в случае неориентированных графов отношение "между вершинами существует маршрут" является отношением эквивалентности. Тогда за этим отношением множества вершин V и ребер E разбиваются на классы эквивалентности kVVV ,,, 21  и kEEE ,,, 21  такие, что пары ),,(= 111 EVG =2G ),(=,),,(= 22 kkk EVGEV  образуют связные подграфы графа ),(= EVG . Эти подграфы называются компо- нентами связности графа G и задача проверки связности графа состоит в том, чтобы найти количество этих компонент. Работа алгоритма сводится к тому, что сначала все вершины графа ),(= EVG размечаются как не прой- денные (для этого служит массив visited – массив логических размерности ||V ), строятся списки смежных вершин (список )(vAdj вершины v ). Дальше обработка вершин графа алгоритмом начинается с произвольной вершины, которая считается начальной. При первом попадании в вершину она размечается как пройденная ( visited ) и к ней рекурсивно применяется DFS -алгоритм. В псевдокоде DFS -алгоритм имеет вид: )(GDFS Вход: граф ),(= EVG , где nV |=| и )(vAdj – множество вершин, смежных с вершиной v . Выход: граф G со всеми помеченными вершинами. Формальні методи програмування 157 Метод: for 1:=v to n do 0:=)(vvisited od for 1:=v to n do if 0=)(vvisited then )(vDfs fi od Procedure )(vDfs 1:=)(vvisited ; for each )(vAdjw do if 0=)(wvisited then )(wDfs fi od End Dfs Для доказательства правильности работы данного алгоритма необходимо знать представление графа в памяти компьютера. Наиболее часто используется представление графа в виде матрицы смежности или списка- ми смежности. Более экономным с точки зрения используемой памяти является представление графа списками смежности. Например, граф G из рис. 2 имеет представление в виде мультисписка смежных вершин приведено на рис. 3. Рис. 2. Несвязный граф Рис. 3. Представление графа мультисписками смежности Формальні методи програмування 158 Дальше предполагается, что граф представляется в виде мультисписков смежностей. Для удобства пер- вый список, включающий все вершины орграфа, будем называть вертикальным списком, а списки смежных вершин – горизонтальными списками. Заметим, что операции удаления ребра и введение ребра сводятся к уда- лению и добавлению соответствующего элемента в горизонтальном списке смежности соответственно. Опера- ции введения вершины и удаления вершины в этом случае сводятся к добавлению в конец вертикального спис- ка нового элемента и удаления всего горизонтального списка смежности данной вершины. Доказательство правильности работы DFS -алгоритма сводится к доказательству наличия пометок у всех вершин графа. В силу рекурсивности данного алгоритма достаточно доказать правильность одного рекур- сивного вызова и корректность завершения этого вызова. Пусть граф G связный, тогда, начиная с начальной вершины G , DFS -алгоритм начинает с разметки всех его вершин как не помеченные путем присваивания значения 0 всем вершинам (для этого служит первый цикл for и массив visited ). Второй цикл, начиная с начальной вершины вертикального списка рекурсивно обрабатывает эту вер- шину при условии её непомеченности. Эта обработка начинается с пометки вершины в массиве visited и ре- курсивной обработки первой непомеченной вершины w , смежной с вершиной v . Здесь возможны два случаи: а) вершина w не имеет смежных вершин, кроме вершины v и б) вершина w смежна не только с v , но и с не- которой вершиной vu = . В случае а) Dfs -процедура заканчивает обработку вершины w , поскольку }{=)( vwAdj и v уже была помечена. Рекурсия возвращается к следующей непомеченной вершине w , смежной с вершиной v . А это означает, что вершина w была помечена и к ней Dfs -процедура уже не будет применяться. Что говорит о том, что обработка была выполнена правильно. В случае б) Dfs -процедура начинает рекурсивную обработку вершины u , присваивая ей пометку 1 в массиве visited . Теперь ситуация с обработкой u повторяется в точно так, как и с вершиной w . В результате вершина u получает пометку, что свидетельствует о правильности работы DFS -алгоритма. Если DFS -алгоритм применить к графу из рис. 2, то Dfs -процедура порождает путь 1,2,4,3,5,6 и за- канчивает свою работу. Однако, цикл for DFS -алгоритма выполнит очередной вызов Dfs -процедуры, которая начнет обработку вершины 7. Эта ситуация означает существование новой компоненты связности. Отсюда сле- дует, что можно модифицировать DFS -алгоритм так, чтобы он находил количество компонент связности и указатели на начальные вершины этих компонент. В результате выполнения DFS -алгоритма генерируются DFS -деревья, которые соответствуют компо- нентам связности (для сохранения DFS -дерева служат списки )(vparent ), а значение переменной c указывает на количество этих компонент. Модифицированный DFS -алгоритм. Таким образом, модифицированный алгоритм принимает вид: DFS - CONNECTED- )(GCOMPONENT begin 1. 0;:=c 2. ;doVvallfor  3. 0;:=)(vvisited 4. ;:=)( NILvparent /* NIL - пустой список */ 5. ;od 6. ;doVvallfor  7. thenvvisitednotif )( 8. 1;:= cc 9. );,( cvDFS 10. ;fi 11. ;od end ),( cvDFS begin 1. 1;:=)(vvisited 2. cvcomponent :=)( ; 3. ;)( dovAdjwallfor  Формальні методи програмування 159 4. thenwvisitednotif )( 5. ;:=)( vwparent 6. );,( cwDFS 7. ;fi 8. ;od end Если в результате выполнения алгоритма DFS -CONNECTED- COMPONENT получаем 1=c , то исход- ный граф ),(= EVG связный, иначе – несвязен. Пример 3. Пусть ),(= EVG – граф, приведен на рис. 2. Если начальной вершиной есть 1, то значение 2=c (граф G несвязен) и деревья, порождаемые DFS -алгоритмом, имеют вид (рис. 4). Рис. 4. Деревья, порождаемые DFS -алгоритмом ( 2=c ) Известно, что временная сложность DFS -алгоритма выражается величиной | )||(| EVO  . Заметим, что DFS -деревья (указатели на начальные вершины этих деревьев находятся в списке )(vcomponent ), которые строит DFS -алгоритм, зависят от порядка обхода вершин, смежных с текущей верши- ной. Отсюда следует, что не всегда некоторое ребро будет ребром такого дерева. Ребра, которые принадлежат DFS -дереву, называются прямыми ребрами, а остальные рёбра графа называются обратными. Очевидно, что при помощи DFS -алгоритма можно находить не только прямые, но и обратные рёбра в процессе обхода его вершин. Выше на рисунке выпуклыми кривыми показаны обратные рёбра (5,4)(4,1),(3,1), и (9,7) , найденные DFS -алгоритмом. Вывод Отметим, что необходимость поиска семантических свойств предметной области возникает в связи с тем, что информации, извлеченной из текста алгоритма или программы (например, в виде инвариантных соотноше- ний), как правило, недостаточно для обоснования их правильности. Многие свойства, особенно семантического характера, явно не фигурируют в алгоритме и тем более в программе его реализации. Поиск семантических свойств сопряжен с трудностями как теоретического, так и практического характера и его успех зависит прежде всего от индивидуальных качеств разработчика программного обеспечения. В этом, наверное, и состоит глав- ная сложность проблемы построения качественного и надежного програмного обеспечения. Такой подход к построению и обоснованию эффективных алгоритмов описывался в работах [9, 10]. 1. Калниньш А.А., Борзов Ю.В. Инвентаризация идей тестирования программ. Рига: ЛГУ им. Стучки. – 1981. – 54 с. 2. Cousot P. Abstract Interpretation Based Formal Methods and Future Challenges. http://www.di.ens.fr/ cousot/. – 2003. – P. 131–151. Chap. 10. – P. 303–342. 3. Cousot P. Verification by abstract Interpretation. – Lecture Notes in Comp. Science. – 2003. – N 2772. – P. 243–268. 4. Clarke E.M., Grumberg Jr. O., Peled D. Model Checking. The MIT Press: Cambridge, Massachusetts, London, England. – 2001. – 356 p. 5. Penczek W., Pólrola A. Advanced in Verification on Time Petri Nets and Timed Automata. Springer-Verlag Berlin Heidelberg. – 2006. – 258 p. 6. Ben-Ari M. Mathematical Logic for Computer Science. Springer-Verlag London Limited. – 2001. – 345 p. 7. Nielson F. Two-level semantics and abstract interpretation // Theor. Comp Scien. (Fundamental Studies). – 1989. – N 69. – P. 117–242. 8. Кривий С.Л. Вступ до методiв створення програмних продуктiв. Чернiвцi: "Букрек". – 2012. – 424 с. 9. Годлевский А.Б., Кривой С.Л. Трансформационный синтез эффективных алгоритмов с учетом дополнительных спецификаций // Ки- бернетика. – 1986. – № 6. – C. 34–43. 10. Годлевский А.Б., Кривой С.Л. О проектировании эффективных алгоритмов приведения автоматов для некоторых отношений эквива- лентности // Кибернетика и системный анализ. – 1989. – № 6. – C. 54–61.

Ähnliche Einträge