Теорема о структурированной программе

Графы потока управления с 3 типами структур управления могут вычислить любую вычислимую функцию

Теорема о структурированной программе , также называемая теоремой Бёма–Якопини , [1] [2] является результатом в теории языков программирования . Она утверждает, что класс графов потока управления (исторически называемых блок-схемами в этом контексте) может вычислить любую вычислимую функцию , если он объединяет подпрограммы только тремя определенными способами ( структуры управления ). Это

  1. Выполнение одной подпрограммы, а затем другой подпрограммы (последовательность)
  2. Выполнение одной из двух подпрограмм в соответствии со значением логического выражения (выбор)
  3. Повторное выполнение подпрограммы до тех пор, пока логическое выражение остается истинным (итерация)

Структурированная диаграмма, подчиняющаяся этим ограничениям, в частности, ограничению цикла, подразумевающему единственный выход (как описано далее в этой статье), может, однако, использовать дополнительные переменные в форме битов (хранящихся в дополнительной целочисленной переменной в исходном доказательстве) для того, чтобы отслеживать информацию, которую исходная программа представляет по местоположению программы. Конструкция была основана на языке программирования Бёма P′′ .

Теорема составляет основу структурного программирования — парадигмы программирования, которая избегает команд goto и использует исключительно подпрограммы, последовательности, выбор и итерацию.

Графическое представление трех основных шаблонов теоремы о структурированной программе — последовательности, выбора и повторения — с использованием диаграмм NS (синего цвета) и блок-схем (зеленого цвета).

Происхождение и варианты

Теорема обычно приписывается [3] : 381  статье 1966 года Коррадо Бёма и Джузеппе Якопини  [it] . [4] Дэвид Харел писал в 1980 году, что статья Бёма–Якопини пользовалась «всеобщей популярностью», [3] : 381  особенно среди сторонников структурного программирования. Харел также отметил, что «из-за своего довольно технического стиля [статья Бёма–Якопини 1966 года], по-видимому, чаще цитируется, чем читается подробно» [3] : 381  и, после обзора большого количества статей, опубликованных до 1980 года, Харел утверждал, что содержание доказательства Бёма–Якопини обычно неверно представлялось как народная теорема , которая по сути содержит более простой результат, результат, который сам по себе можно проследить до зарождения современной теории вычислений в статьях фон Неймана [5] и Клини . [3] : 383 

Харель также пишет, что более общее название было предложено HD Mills как «Структурная теорема» в начале 1970-х годов. [3] : 381 

Одинарный цикл while, народная версия теоремы

Эта версия теоремы заменяет весь поток управления исходной программы одним глобальным whileциклом, который имитирует счетчик программ, проходящий по всем возможным меткам (блокам блок-схемы) в исходной неструктурированной программе. Харел проследил происхождение этой народной теоремы до двух статей, знаменующих начало вычислений. Одна из них — описание архитектуры фон Неймана 1946 года , в котором объясняется, как работает счетчик программ в терминах цикла while. Харел отмечает, что один цикл, используемый народной версией теоремы о структурном программировании, в основном просто обеспечивает операционную семантику для выполнения блок-схемы на компьютере фон Неймана. [3] : 383  Другим, еще более старым источником, который Харел проследил для народной версии теоремы, является теорема Стивена Клини о нормальной форме 1936 года. [3] : 383 

Дональд Кнут раскритиковал эту форму доказательства, которая приводит к псевдокоду, подобному приведенному ниже, указав, что структура исходной программы полностью теряется в этом преобразовании. [6] : 274  Аналогично, Брюс Ян Миллс писал об этом подходе, что «Дух блочной структуры — это стиль, а не язык. Симулируя машину фон Неймана, мы можем воспроизвести поведение любого спагетти-кода в пределах блочно-структурированного языка. Это не мешает ему быть спагетти». [7]

p := 1 while p > 0 do if p = 1 then выполнить шаг 1 из блок -схемы p := результирующий последующий шаг номер шага 1 из блок -схемы ( 0 , если нет последователя ) end if if p = 2 then выполнить шаг 2 из блок -схемы p := результирующий последующий шаг номер шага 2 из блок -схемы ( 0 , если нет последователя ) end if ... if p = n then выполнить шаг n из блок -схемы p := результирующий последующий шаг номер шага n из блок - схемы ( 0 , если нет последователя ) end if end while                                                                                               

Доказательство Бёма и Якопини

Доказательство в статье Бёма и Якопини проводится методом индукции по структуре блок-схемы. [3] : 381  Поскольку оно использовало сопоставление с образцом в графах , доказательство Бёма и Якопини не было по-настоящему практичным в качестве алгоритма преобразования программ , и, таким образом, открыло дверь для дополнительных исследований в этом направлении. [8]

Реверсивная версия

Теорема об обратимой структурированной программе [9] является важной концепцией в области обратимых вычислений . Она утверждает, что любое вычисление, достижимое обратимой программой, может быть также выполнено с помощью обратимой программы, использующей только структурированную комбинацию конструкций потока управления, таких как последовательности, выборки и итерации. Любое вычисление, достижимое традиционной необратимой программой, также может быть выполнено с помощью обратимой программы, но с дополнительным ограничением, что каждый шаг должен быть обратимым и иметь некоторые дополнительные выходные данные. [10] Более того, любая обратимая неструктурированная программа также может быть выполнена с помощью структурированной обратимой программы с помощью только одной итерации без каких-либо дополнительных выходных данных. Эта теорема закладывает основополагающие принципы построения обратимых алгоритмов в рамках структурированного программирования.

Для теоремы о структурированной программе известны как локальные [4] , так и глобальные [11] методы доказательства. Однако для ее обратимой версии, хотя глобальный метод доказательства и признан, локальный подход, аналогичный подходу, предпринятому Бемом и Якопини [4], пока не известен. Это различие является примером, подчеркивающим проблемы и нюансы в установлении основ обратимых вычислений по сравнению с традиционными вычислительными парадигмами.

Последствия и уточнения

Доказательство Бёма–Якопини не решило вопрос о том, следует ли принимать структурное программирование для разработки программного обеспечения, отчасти потому, что конструкция скорее запутывала программу, чем улучшала ее. Напротив, оно положило начало дебатам. Знаменитое письмо Эдсгера Дейкстры « Go To Statement Considered Harmful » последовало в 1968 году . [12]

Некоторые ученые придерживались пуристского подхода к результату Бёма–Якопини и утверждали, что даже инструкции вроде breakи returnиз середины циклов являются плохой практикой, поскольку они не нужны в доказательстве Бёма–Якопини, и поэтому они выступали за то, чтобы все циклы имели одну точку выхода. Этот пуристский подход воплощен в языке программирования Pascal (разработанном в 1968–1969 годах), который до середины 1990-х годов был предпочтительным инструментом для преподавания вводных классов программирования в академических кругах. [13]

Эдвард Йордон отмечает, что в 1970-х годах существовала даже философская оппозиция преобразованию неструктурированных программ в структурированные с помощью автоматизированных средств, основанная на аргументе, что нужно было думать в стиле структурного программирования с самого начала. Прагматический контрапункт состоял в том, что такие преобразования приносили пользу большому количеству существующих программ. [14] Среди первых предложений по автоматизированному преобразованию была статья Эдварда Эшкрофта и Зохара Манны 1971 года . [15]

Прямое применение теоремы Бёма–Якопини может привести к введению дополнительных локальных переменных в структурированную схему, а также может привести к некоторому дублированию кода . [16] Последняя проблема в этом контексте называется проблемой цикла и половины. [17] Pascal подвержен обеим этим проблемам, и согласно эмпирическим исследованиям, на которые ссылается Эрик С. Робертс , студенты-программисты испытывали трудности с формулированием правильных решений на языке Pascal для нескольких простых задач, включая написание функции для поиска элемента в массиве. Исследование Генри Шапиро 1980 года, на которое ссылается Робертс, показало, что при использовании только управляющих структур, предоставляемых Pascal, правильное решение было дано только 20% испытуемых, в то время как ни один испытуемый не написал неправильный код для этой задачи, если ему было разрешено написать возврат из середины цикла. [13]

В 1973 году С. Рао Косараджу доказал, что можно избежать добавления дополнительных переменных в структурном программировании, если разрешены произвольной глубины многоуровневые разрывы из циклов. [1] [18] Кроме того, Косараджу доказал, что существует строгая иерархия программ, в настоящее время называемая иерархией Косараджу , в которой для каждого целого числа n существует программа, содержащая многоуровневый разрыв глубины n , которая не может быть переписана как программа с многоуровневыми разрывами глубиной меньше n (без введения дополнительных переменных). [1] Косараджу ссылается на конструкцию многоуровневого разрыва в языке программирования BLISS . Многоуровневые разрывы в виде ключевого слова были фактически введены в версии BLISS-11 этого языка; в оригинальном BLISS были только одноуровневые разрывы. Семейство языков BLISS не предоставляло неограниченного goto. Язык программирования Java позже также следовал этому подходу. [19] : 960–965 leave label

Более простой результат из статьи Косараджу заключается в том, что программа сводится к структурированной программе (без добавления переменных) тогда и только тогда, когда она не содержит цикла с двумя различными выходами. Сводимость была определена Косараджу, грубо говоря, как вычисление той же функции и использование тех же «примитивных действий» и предикатов, что и исходная программа, но, возможно, с использованием других структур потока управления. (Это более узкое понятие сводимости, чем то, что использовал Бём–Якопини.) Вдохновленный этим результатом, в разделе VI своей часто цитируемой статьи, в которой было введено понятие цикломатической сложности , Томас Дж. МакКейб описал аналог теоремы Куратовского для графов потока управления (CFG) неструктурированных программ, то есть минимальных подграфов , которые делают CFG программы неструктурированной. Эти подграфы имеют очень хорошее описание на естественном языке. Они таковы:

  1. ответвление от цикла (кроме теста цикла цикла)
  2. разветвление в петлю
  3. ветвление в решение (т.е. в «ветвь» if)
  4. ответвление от решения

Маккейб фактически обнаружил, что эти четыре графа не являются независимыми, когда появляются как подграфы, что означает, что необходимым и достаточным условием для того, чтобы программа была неструктурированной, является то, чтобы ее CFG имел в качестве подграфа один из любого подмножества трех из этих четырех графов. Он также обнаружил, что если неструктурированная программа содержит один из этих четырех подграфов, она должна содержать еще один отличный от набора из четырех. Этот последний результат помогает объяснить, как поток управления неструктурированной программы становится запутанным в том, что обычно называют « спагетти-кодом ». Маккейб также разработал численную меру, которая, учитывая произвольную программу, количественно определяет, насколько она далека от идеала быть структурированной программой; Маккейб назвал свою меру существенной сложностью . [20]

Характеристику Маккейба запрещённых графов для структурного программирования можно считать неполной, по крайней мере, если рассматривать структуры Дейкстры D в качестве строительных блоков. [21] : 274–275  [ необходимо разъяснение ]

До 1990 года было предложено довольно много методов для устранения goto из существующих программ, сохраняя при этом большую часть их структуры. Различные подходы к этой проблеме также предлагали несколько понятий эквивалентности, которые являются более строгими, чем просто эквивалентность Тьюринга, чтобы избежать вывода, подобного обсуждаемой выше народной теореме. Строгость выбранного понятия эквивалентности диктует минимальный набор необходимых структур потока управления. Статья JACM 1988 года Лайла Рэмшоу рассматривает область до этого момента, а также предлагает свой собственный метод. [22] Алгоритм Рэмшоу использовался, например, в некоторых декомпиляторах Java , поскольку код виртуальной машины Java имеет инструкции ветвления с целями, выраженными как смещения, но высокоуровневый язык Java имеет только многоуровневые breakи continueоператоры. [23] [24] [25] Аммаргуэлла (1992) предложил метод преобразования, который восходит к обеспечению единственного выхода. [8]


Применение к Коболу

В 1980-х годах исследователь IBM Харлан Миллс курировал разработку COBOL Structuring Facility, которая применяла алгоритм структурирования к коду COBOL . Преобразование Миллса включало следующие шаги для каждой процедуры.

  1. Определите основные блоки процедуры.
  2. Назначьте уникальную метку входному пути каждого блока и пометьте выходные пути каждого блока метками входных путей, с которыми они соединены. Используйте 0 для возврата из процедуры и 1 для входного пути процедуры.
  3. Разбейте процедуру на основные блоки.
  4. Для каждого блока, который является пунктом назначения только одного пути выхода, повторно подключите этот блок к этому пути выхода.
  5. Объявите новую переменную в процедуре (назовем ее L для справки).
  6. На каждом оставшемся неподключенном пути выхода добавьте оператор, который устанавливает L равным значению метки на этом пути.
  7. Объедините полученные программы в оператор выбора, который выполняет программу с меткой пути входа, обозначенной L.
  8. Постройте цикл, который выполняет этот оператор выбора до тех пор, пока L не равно 0.
  9. Постройте последовательность, которая инициализирует L значением 1 и выполняет цикл.

Эту конструкцию можно улучшить, преобразовав некоторые случаи оператора выбора в подпроцедуры.

Смотрите также

Ссылки

  1. ^ abc Декстер Козен и Вэй-Лунг Дастин Ценг (2008). "Математика построения программ - Теорема Бёма–Якопини ложна, пропозиционально" (PDF) . MPC 2008 . Заметки лекций по информатике. 5133 : 177– 192. CiteSeerX  10.1.1.218.9241 . doi :10.1007/978-3-540-70594-9_11. ISBN 978-3-540-70593-2.
  2. ^ "CSE 111, осень 2004 г., ТЕОРЕМА БЁМА-ЯКОПИНИ". Cse.buffalo.edu. 2004-11-22 . Получено 2013-08-24 .
  3. ^ abcdefgh Харель, Дэвид (1980). "О народных теоремах" (PDF) . Сообщения ACM . 23 (7): 379– 389. doi :10.1145/358886.358892. S2CID  16300625.
  4. ^ abc Бём, Коррадо ; Якопини, Джузеппе [на итальянском] (май 1966). «Схемы потоков, машины Тьюринга и языки только с двумя правилами формирования». Сообщения ACM . 9 (5): 366–371 . CiteSeerX 10.1.1.119.9119 . doi :10.1145/355592.365646. S2CID  10236439. 
  5. ^ Беркс, Артур В .; Голдстайн, Герман ; фон Нейман, Джон (1947), Предварительное обсуждение логического проектирования электронного вычислительного прибора , Принстон, Нью-Джерси: Институт перспективных исследований
  6. ^ Дональд Кнут (1974). «Структурное программирование с операторами перехода». Computing Surveys . 6 (4): 261– 301. CiteSeerX 10.1.1.103.6084 . doi :10.1145/356635.356640. S2CID  207630080. 
  7. ^ Брюс Ян Миллс (2005). Теоретическое введение в программирование . Springer. стр. 279. ISBN 978-1-84628-263-8.
  8. ^ ab Ammarguellat, Z. (1992). «Алгоритм нормализации потока управления и его сложность». IEEE Transactions on Software Engineering . 18 (3): 237– 251. doi :10.1109/32.126773.
  9. ^ Ёкояма, Тетсуо; Аксельсен, Хольгер Бок; Глюк, Роберт (январь 2016 г.). «Основы языков обратимых блок-схем». Теоретическая информатика . 611 : 87–115 . doi : 10.1016/j.tcs.2015.07.046 .
  10. ^ Беннетт, CH (ноябрь 1973 г.). «Логическая обратимость вычислений». IBM Journal of Research and Development . 17 (6): 525– 532. doi :10.1147/rd.176.0525.
  11. ^ Купер, Дэвид С. (август 1967 г.). «Сокращение схем потоков Бёма и Якопини». Сообщения ACM . 10 (8): 463. doi :10.1145/363534.363539.
  12. ^ Дейкстра, Эдсгер (1968). «Перейти к заявлению, считающемуся вредным». Сообщения ACM . 11 (3): 147– 148. doi : 10.1145/362929.362947 . S2CID  17469809.
  13. ^ Робертс, Э. [1995] «Выходы из циклов и структурное программирование: возобновление дебатов», ACM SIGCSE Bulletin, (27)1: 268–272.
  14. ^ EN Yourdon (1979). Классика в программной инженерии . Yourdon Press. С. 49–50. ISBN 978-0-917072-14-7.
  15. ^ Эшкрофт, Эдвард; Зохар Манна (1971). «Трансляция go to программ в 'while' программы». Труды Конгресса IFIP .Статья, которую трудно получить в оригинальных трудах конференции из-за их ограниченного распространения, была переиздана в книге Йордона 1979 года, стр. 51-65.
  16. ^ Дэвид Энтони Уотт; Уильям Финдли (2004). Концепции дизайна языка программирования . John Wiley & Sons. стр. 228. ISBN 978-0-470-85320-7.
  17. ^ Кеннет К. Лоуден; Кеннет А. Ламберт (2011). Языки программирования: принципы и практика (3-е изд.). Cengage Learning. стр. 422–423. ISBN 978-1-111-52941-3.
  18. ^ KOSARAJU, S. RAO. "Анализ структурированных программ", Proc. Fifth Annual ACM Syrup. Теория вычислений, (май 1973 г.), 240-252; также Kosaraju, S. Rao (1974 г.). "Анализ структурированных программ". Journal of Computer and System Sciences . 9 (3): 232– 255. doi :10.1016/S0022-0000(74)80043-7.цитируется Дональдом Кнутом (1974). «Структурное программирование с операторами перехода». Computing Surveys . 6 (4): 261– 301. CiteSeerX 10.1.1.103.6084 . doi :10.1145/356635.356640. S2CID  207630080. 
  19. ^ Брендер, Рональд Ф. (2002). «Язык программирования BLISS: история» (PDF) . Программное обеспечение: практика и опыт . 32 (10): 955– 981. doi :10.1002/spe.470. S2CID  45466625.
  20. Оригинальная статья — Thomas J. McCabe (декабрь 1976 г.). «Мера сложности». IEEE Transactions on Software Engineering . SE-2 (4): 315– 318. doi :10.1109/tse.1976.233837. S2CID  9116234.Для вторичного изложения см. Paul C. Jorgensen (2002). Software Testing: A Craftsman's Approach, Second Edition (2nd ed.). CRC Press. стр.  150–153 . ISBN 978-0-8493-0809-3.
  21. ^ Уильямс, МХ (1983). «Схемы блок-схем и проблема номенклатуры». The Computer Journal . 26 (3): 270– 276. doi : 10.1093/comjnl/26.3.270 .
  22. ^ Ramshaw, L. (1988). «Устранение переходов при сохранении структуры программы». Журнал ACM . 35 (4): 893–920 . doi : 10.1145/48014.48021 . S2CID  31001665.
  23. ^ Годфри Нолан (2004). Декомпиляция Java . Apress. стр. 142. ISBN 978-1-4302-0739-9.
  24. ^ "Krakatoa: Декомпиляция на Java" (PDF) . www.usenix.org .
  25. ^ «Эффективный алгоритм декомпиляции байт-кодов Java» (PDF) . www.openjit.org .

Дальнейшее чтение

Материалы, еще не рассмотренные выше:

  • ДеМилло, Ричард А. (1980). «Пространственно-временные компромиссы в структурном программировании: улучшенная комбинаторная теорема о вложении». Журнал ACM . 27 (1): 123– 127. doi : 10.1145/322169.322180 . S2CID  15669719.
  • Devienne, Philippe (1994). «Одного бинарного предложения Horn достаточно». Stacs 94. Lecture Notes in Computer Science. Vol. 775. pp.  19– 32. CiteSeerX  10.1.1.14.537 . doi :10.1007/3-540-57785-8_128. ISBN 978-3-540-57785-0.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Structured_program_theorem&oldid=1271042726"