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

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

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

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

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

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

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

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

Харель также пишет, что более общее название было предложено Х.Д. Миллсом как «Структурная теорема» в начале 1970-х годов.

одним циклом

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

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

p := 1
while p > 0 do
    if p = 1 then
        perform step 1 from the flowchart
        p := resulting successor step number of step 1 from the flowchart (0 if no successor)
    end if
    if p = 2 then
        perform step 2 from the flowchart
        p := resulting successor step number of step 2 from the flowchart (0 if no successor)
    end if
    ...
    if p = n then
        perform step n from the flowchart
        p := resulting successor step number of step n from the flowchart (0 if no successor)
    end if
end while

Якопини

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

Двусторонняя версия

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

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

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

Доказательство Бема-Якопини не решило вопроса о том, следует ли использовать структурное программирование для разработки программного обеспечения, отчасти потому, что такая конструкция скорее затеняла программу, чем улучшала ее. Напротив, это сигнализировало о начале дебатов. Эдсгера Дейкстры В 1968 году последовало знаменитое письмо « Перейти к заявлению, считающемуся вредным ».

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

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

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

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

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

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

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

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

Вплоть до 1990 года было предложено довольно много методов исключения gotos из существующих программ с сохранением большей части их структуры. Различные подходы к этой проблеме также предлагали несколько понятий эквивалентности, которые более строгие, чем просто эквивалентность Тьюринга, чтобы избежать вывода, подобного народной теореме, обсуждавшейся выше. Строгость выбранного понятия эквивалентности диктует минимальный набор необходимых структур потока управления. 1988 года Статья Лайла Рэмшоу в JACM исследует область до этого момента, а также предлагает свой собственный метод. Алгоритм Рамшоу использовался, например, в некоторых декомпиляторах Java , поскольку код виртуальной машины Java имеет инструкции ветвления с целями, выраженными как смещения, но язык Java высокого уровня имеет только многоуровневые инструкции. break и continue заявления. Аммаргуеллат (1992) предложил метод трансформации, основанный на обеспечении единого выхода.

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

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

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

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

См. также

• Структурированное программирование
• Полнота по Тьюрингу

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

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

• ДеМилло, Ричард А. (1980). «Пространственно-временные компромиссы в структурированном программировании: улучшенная теорема комбинаторного вложения» . Журнал АКМ . 27 (1): 123–127. дои : 10.1145/322169.322180 . S2CID   15669719 .
• Девьен, Филипп (1994). «Одного двоичного предложения достаточно». Стакс 94 . Конспекты лекций по информатике. Том. 775. стр. 19–32. CiteSeerX   10.1.1.14.537 . дои : 10.1007/3-540-57785-8_128 . ISBN  978-3-540-57785-0 .