ББК 32.973 16 страница

Пересадка лианы узаконивает лишь некоторые, отнюдь не любые передачи управления, поскольку определение данной операции (см. гл. 15, тезис 28) содержит ряд ограничений. Запрет на образование нового цикла вызван тем, что переход на оператор, расположенный выше (раньше) в тексте программы, считается “наихудшим применением оператора goto ” [4]. Указанный запрет вводится, чтобы выполнить требование: использовать goto только для передачи управления вперед по программе, “которое некоторыми организациями принимается в качестве компромиссной версии структурного программирования”.

Запрет на образование второго входа в цикл соответствует требованию структурного кодирования, согласно которому цикл, как и любая простая программа, должен иметь не более одного входа. Лишь третий запрет является оригинальной особенностью шампур-метода: он запрещает передачи управления, изображение которых с помощью лианы ведет к пересечению линий. Таким образом, пересадка лианы разрешает только те переходы вниз по ДРАКОН-программе, которые образуют связи с валентными точками и изображаются легко прослеживаемыми маршрутами, т. е. непересекающимися линиями.

Является ли
текстовое структурное программирование
формальным методом?

Ортодоксальный метод Дейкстры, полностью запрещающий goto и заменители (см. с. 238, табл. 4, вариант 1), безусловно является строгим формальным методом. К сожалению, он полезен лишь как интересная теоретическая идея, которая, как показал всемирный опыт, в чистом виде оказалась непригодной для массового использования.

По мнению специалистов, “правила структурного программирования верны в 95%. Но остаются злополучные 5%” [20]. Чтобы поправить дело, решить проблему пяти процентов и создать метод, пригодный для широкой практики, пришлось пойти на компромисс и дать добро на использование заменителей и так называемое “ограниченное применение goto ” (см. табл. 4, варианты 2—4). Благодаря этому проблема массовой практики программирования была решена. Но какой ценой? Ценой отказа от строгого формализма.

Это нетрудно показать. Например, авторы учебника языка СИ со­ветуют осторожно и редко применять заменители break и continue, “поскольку слишком частое их использование ухудшает читаемость программы, увеличивает вероятность ошибок и затрудняет ее модификацию” [21]. Далее они пишут: избегайте использовать goto, ибо это “чрезвычайно плохое” средство, которое следует применять “как можно реже или не применять совсем” [21].

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

Следовательно, мы вправе сделать существенное замечание. Структурное кодирование, используемое в широкой практике программирования, не является формальным методом, так как к формальным правилам Дейкстры пришлось добавить неформальные правила, касающиеся goto и заменителей.

В шампур-методе аналогом goto и заменителей служат формальные операции “пересадка лианы” и “заземление лианы”, на использование которых не накладывается никаких неформальных ограничений.

Тем самым мы приходим к важному выводу. В отличие от тексто­вого структурного программирования, обладающего лишь частичной формализацией, правила визуального структурного программирования формализованы на 100%, что подтверждается тем фактом, что они реализованы в алгоритмах ДРАКОН-редактора.

ПОЧЕМУ САМОЛЕТ НЕ МАШЕТ КРЫЛЬЯМИ?

Говоря о будущем структурного программирования, необходимо осознать, что текстовое и визуальное программирование опирается на разные системы понятий, которые по-разному расчленяют действительность. Поэтому видеоструктурное программирование нельзя рассмат­ривать как результат механического перевода устоявшихся понятий классического структурного программирования на новый язык.

Поясним сказанное. При визуальном структурном программировании программист работает только с чертежом программы, не обращаясь к ее тексту, подобно тому, как программист, работающий, скажем, на Паскале, не обращается к ассемблеру и машинному коду — они для него просто не существуют! Это значит, что столь тщательно обоснованная Дейкстрой коллекция ключевых слов структурного кодирования (if, then, else, case, of, while, do, repeat, until, begin, end [2]) при переходе к визуальному программированию становится ненужной — для программиста она просто перестает существовать! В равной степени становятся лишними и отмирают и другие ключевые слова, используемые оппонентами Дейкстры в различных вариантах расширения структур­ного кодирования: goto, continue, break, exit и т. д.

Следует специально подчеркнуть: поскольку в визуальном варианте структурного программирования ключевое слово goto не используется, теряют смысл и все споры относительно законности или незаконности, опасности или безопасности его применения, а также обширная литература, посвященная обсуждению этого, некогда казавшегося столь актуальным вопроса.

Предвижу возражения: хотя названные ключевые слова действительно исчезают, однако выражаемые ими понятия сохраняют силу и для визуального программирования. Например, две видеопрограммы на рис. 27 можно построить с помощью понятий if-then-else и goto. Данное возражение нельзя принять, поскольку произошла подмена предмета обсуждения. С помощью указанных понятий можно построить не видеопрограммы, а текстовые программы, эквивалентные видеопрограммам на рис. 27. Что касается собственно видеопрограмм, то они, будучи “выполнимой графикой”, строятся из “выполняемых” икон и “выполняемых” соединительных линий. Причем — подчеркнем еще раз —
в процессе построения (которое реализуется с помощью ДРАКОН-редак­тора) пользователь не применяет понятия if-then-else и goto, ибо в этом нет никакой необходимости.

Нельзя путать задачу и систему понятий, на которую опирается метод ее решения. В обоих случаях — и при текстовом, и при визуальном структурном кодировании — ставится одна и та же задача: улучшить понимаемость программ и обеспечить более эффективный интеллектуальный контроль за передачами управления. Однако система понятий коренным образом меняется: ту функцию, которую в текстовой программе выполняют ключевые слова, в видеопрограмме реализуют совершенно другие понятия: иконы, макроиконы, соединительные линии, шампур, главная вертикаль шампур-блока, лиана, атом, пересадка лианы, запрет пересечения линий и т. д.

Очевидно, что использование понятий, выражаемых ключевыми словами классического структурного программирования, не является самоцелью, а служит лишь для того, чтобы “делать наши программы разумными, понятными и разумно управляемыми” [22]. Указанные понятия решают эту задачу не во всех случаях, а только в рамках текстового программирования. При переходе к визуальному программированию задача решается по-другому, с помощью другого набора понятий. Именно отказ от старого набора понятий и замена его на новый и позволяет добиться новой постановки задачи и более эффективного ее решения. Поэтому высказываемое иногда критическое замечание: “недостаток шампур-метода в том, что он не удовлетворяет требованиям структурного программирования” является логически неправомерным. Нельзя упрекать самолет за то, что он не машет крыльями.

ВЫВОДЫ

1. Визуальное структурное программирование (шампур-метод) и текс­товое структурное программирование несоизмеримы (в куновском смысле слова), они опираются на разные системы понятий, которые по-разному расчленяют действительность.

2. Текстовое структурное программирование решило стоявшие перед ним исторические задачи, исчерпало свои эвристические возмож­ности и, выполнив свою миссию, потеряло актуальность. В настоящее время точкой роста научного знания является визуальное структурное программирование.

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

4. В отличие от текстового структурного программирования шампур-ме­тод является полностью формальным.

5. По эргономическим показателям визуальное структурное програм­мирование существенно превосходит свой текстовый аналог.

6. Широко распространенное мнение о несовместимости блок-схем и структурного программирования является мифом, нелепой ошибкой, основанной на невнимательном прочтении классической работы Э. Дейкстры “Заметки по структурному программированию”.

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

8. Существующая литература по блок-схемам, включая международные и национальные стандарты, на 99% устарела.

9. Современные стандарты на блок-схемы объективно содействуют снижению качества соответствующей интеллектуальной продукции. Указанные стандарты игнорируют три важнейших принципа: структу­ризации, формализации и эргономизации.

10. Актуальной задачей является разработка новой системы международных и национальных стандартов на блок-схемы, свободных от перечисленных недостатков. В основу проекта новых стандартов целесообразно положить изложенные в этой книге правила визуального структурного программирования. Дракон-схемы наследуют все или почти все достоинства блок-схем и устраняют их недостатки.

 

Г Л А В А 17

Исчисление икон и попытка
предсказать будущее

Зрительные образы — плоть и кровь самого мышления.

Рудольф Арнхейм

ВИЗУАЛЬНОЕ ЛОГИЧЕСКОЕ ИСЧИСЛЕНИЕ

Включим еще один “боковой прожектор” и попытаемся взглянуть на визуальный синтаксис языка ДРАКОН с позиций математической ло­гики. Нашему взору откроется необычная картина. Оказывается, любая абстрактная дракон-схема представляет собой теорему, которая строго выводится (доказывается) из двух аксиом, каковыми являются заготовка-примитив и заготовка-силуэт.

— Какие же это аксиомы? — вправе удивиться читатель. — Ведь это просто картинки-слепыши! А дракон-схемы вовсе не похожи на теоремы! Кто и зачем их должен доказывать? Наверно, это шутка или метафора.

— Вовсе нет, отнюдь не метафора. Ниже будет показано, что ви­зуальный синтаксис ДРАКОНА построен как логическое исчисление (назовем его “исчисление икон”). Данное исчисление можно рассмат­ривать как раздел визуальной математической логики. Последнее понятие не является традиционным. Математическая логика и ее основные понятия (исчисление, логический вывод и т. д.) сформировались в рамках текстовой парадигмы. В данной главе, по-видимому, впервые вводятся визуальные аналоги этих понятий и на их основе строится исчисление икон.

ОБЩЕИЗВЕСТНЫЕ
СВЕДЕНИЯ О МАТЕМАТИЧЕСКОЙ ЛОГИКЕ

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

! явной формулировкой исходных положений (аксиом) развиваемой теории (формальной системы);

! явной формулировкой правил логического вывода, с помощью которых из аксиом выводятся теоремы теории;

! использованием формальных языков для изложения теорем рассматриваемой теории [1].

Основным объектом изучения в математической логике являются логические исчисления. В понятие исчисления входят такие основные компоненты, как:

а) формальный язык, который задается с помощью алфавита и син­таксиса,

б) аксиомы,

в) правила вывода [1].

Таким образом, исчисление позволяет, зная аксиомы и правила вывода, получить (т. е. вывести, доказать) все теоремы теории, причем теоремы, как и аксиомы, записываются только на формальном языке.

Напомним, что в рамках математической логики три термина: логическое исчисление, формальная система и теория можно рассматривать как синонимы. Следовательно, теоремы исчисления, теоремы формальной системы и теоремы теории — это одно и то же.

ОБ ОДНОМ РАСПРОСТРАНЕННОМ
ЗАБЛУЖДЕНИИ

Существуют два подхода к формализации человеческих знаний: визуальный (графический, изобразительный) и текстовый. С этой проблемой связано любопытное противоречие. С одной стороны, преимущество графики перед текстом для человеческого восприятия считается общепризнанным, так как человеческий мозг в основном ориентирован на визуальное восприятие и люди получают информацию при рассмотрении графических образов быстрее, чем при чтении текста. И. Вельбицкий совершенно справедливо указывает: “Текст — наиболее общая и наименее информативная в смысле наглядности и скорости восприятия форма представления информации”, а чертеж — “наиболее развитая интегрированная форма представления знаний”.

С другой стороны, теоретическая разработка принципов визуальной формализации знаний все еще не развернута в должной мере. Причину отставания следует искать в истории науки, в частности в особенностях развития математики и логики.

В этих дисциплинах с давних пор (иногда явно, чаще неявно) предполагалось, что результаты математической и логической формализации знаний в подавляющем большинстве случаев должны иметь форму текста (а не изображения). Например, Стефен Клини пишет: «Будучи формализованной, теория по своей структуре является уже не системой осмысленных предложений, а системой фраз, рассматриваемых как последовательность слов, которые, в свою очередь, являются последовательностями букв... В символическом языке символы будут обычно соответствовать целым словам, а не буквам, а последовательности символов, соответствующие фразам, будут называться “формулами”... Теория доказательств... предполагает... построение произвольно длинных последовательностей символов» [2].

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

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

Принцип абсолютизации текста

Суть его можно выразить, например, в форме следующих рассуждений.

Существует ряд работ, косвенным образом доказывающих, что принцип абсолютизации текста является ошибочным и вредным [3, 4 и др.]. Сегодня все больше ученых приходит к выводу, что визуальную фор­мализацию знаний нельзя рассматривать как нечто второстепенное для научного познания, поскольку она входит в саму ткань мысленного процесса ученого и “может опосредовать самые глубинные, творческие шаги научного познания” [3].

Вместе с тем в математической логике визуальные методы, насколько нам известно, пока еще не нашли широкого применения. Иными словами, математическая логика по сей день остается оплотом текстового мышления и текстовых методов формализации знаний. Это обстоятельство играет отрицательную роль, мешая поставить последнюю точку в доказательстве ошибочности “принципа абсолютизации текста”.

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

ВИЗУАЛИЗАЦИЯ
ПОНЯТИЙ МАТЕМАТИЧЕСКОЙ ЛОГИКИ

Нам понадобится определение двух понятий: визуальный логический вывод (видеовывод) и визуальное логическое исчисление (видеоисчис­ление). Чтобы облегчить изучение материала, используем уже знакомый читателю метод очной ставки, помещая в левой графе табл. 6 хорошо известное “текстовое” понятие, а в правой — определение нового, “визуального” понятия.

Таблица 6

Определение понятия “логический вывод” [5]	Определение понятия “видеовывод” (визуальный логический вывод)
Вывод в исчислении V есть последовательность C 1,..., Cn формул, такая, что для любого i формула Ci есть либо аксиома исчисления V, либо непосредственное следствие предыдущих формул по одному из правил вывода. Формула Cn называется теоремой исчисления V, если существует вывод в V, в котором последней формулой является Cn	Видеовывод в видеоисчислении V есть последовательность C 1,... Cn видеоформул, такая, что для любого i видеоформула Ci есть либо видеоаксиома видеоисчисления V, либо непосредственное следствие предыдущих видеоформул по одному из правил видеовывода. Видеоформула Cn называется видеотеоремой видеоисчисления V, если существует видеовывод в V, в котором последней видеоформулой является Cn

Нетрудно заметить, что новое определение (справа) почти дословно совпадает с классическим (слева); разница состоит лишь в добавлении приставки “видео”.

Таблица 7

Определение понятия “логическое исчисление” [6]

Определение понятия “видеоисчисление” (визуальное логическое исчисление)

Логическое исчисление может быть представлено как формальная система в виде четверки V = < И, S 0, A, F > где И — множество базовых элементов (букв алфавита); S 0 — множество синтаксических правил, на основе которых из букв строятся правильно построенные формулы; А — множество правильно построенных формул, элементы которого называются аксиомами; F — правила вывода, которые из множества А позволяют получать новые правильно построенные формулы — теоремы

Видеоисчисление может быть представлено как формальная система в виде четверки V = < И, S 0, A, F > где И — множество икон (букв визуального алфавита); S 0 — множество правил визуального синтаксиса, на основе которых из икон строятся правильно построенные видеоформулы; А — множество правильно построенных видеоформул, элементы которого называются видеоаксиомами; F — правила видеовывода, которые из множества А позволяют получать новые правильно построенные видеоформулы — видеотеоремы. (Множество теорем обозначим через Т.)

Развивая этот подход и опираясь на “текстовое” определение логического исчисления, можно по аналогии ввести понятие “видеоисчис­ление” (табл. 7).

ИСЧИСЛЕНИЕ ИКОН

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

! Множество икон И (букв визуального алфавита) задано тезисом 1 (см. гл. 15) и показано на рис. 1.

! Множество So правил визуального синтаксиса описано в гл. 15 в тезисах 2—37.

! Множество А визуальных аксиом включает всего два элемента: заготовку-примитив и заготовку-силуэт (рис. 115). Далее будем называть их аксиома-примитив и аксиома-силуэт.

! Множество Т, охватывающее все видеотеоремы исчисления V, есть не что иное как множество абстрактных дракон-схем. Заметим, что множество Т не включает аксиомы, так как последние содержат незаполненные критические точки и, следовательно, эквивалентны пустым операторам. Множество Т распадается на две части: множество примитивов Т1и множество силуэтов Т2.

! Множество F правил видеовывода также делится на две части F 1
и F 2. Множество F 1позволяет выводить все теоремы-примитивы, принадлежащие множеству Т1, из единственной аксиомы-прими­тива. Оно содержит пять правил вывода: ввод атома, добавление
варианта, пересадка лианы, боковое присоединение, удаление кон­ца примитива. Эти правила описаны в тезисах 10, 21, 28, 30, 31, 34 гл. 15.

! Множество F 2дает возможность выводить все теоремы-силуэты множества Т2из единственной аксиомы-силуэта. Оно содержит восемь правил вывода: ввод атома, добавление варианта, добавление ветки, пересадка лианы, заземление лианы, боковое присоединение, удаление последней ветки, дополнительный вход. Правила вывода для силуэта описаны в тезисах 10, 21, 28—33, 35 гл. 15.

На этом построение исчисления икон заканчивается.

Известно, что изучение исчислений составляет синтаксическую часть математической логики. Кроме того, последняя занимается семантическим изучением формальных языков, причем основным понятием семантики служит понятие истинности [1].

В исчислении икон семантика тривиальна. Различные видеоформулы (блок-схемы) могут быть истинными или ложными. Видеоформула называется истинной, если она — либо аксиома, либо выводится из аксиом с помощью правил вывода (т. е. является теоремой), и ложной
в противном случае. Таким образом, все правильно построенные абстрактные дракон-схемы (теоремы) истинны. И наоборот, неправильно построенные схемы, не удовлетворяющие визуальным правилам языка ДРАКОН, считаются ложными. Примеры ложных схем показаны на рис. 131 и 132 в левой графе.

ЕЩЕ РАЗ О ШАМПУР-МЕТОДЕ

Ранее мы определили шампур-метод как теорию визуального структурного программирования. В этой главе появилась возможность значительно обогатить это понятие и рассматривать его как исчисление икон, включая вопросы интерпретации последнего.

Чтобы подчеркнуть теоретический характер шампур-метода, целесообразно слегка изменить терминологию. В частности, использование названия ДРАКОН, связанного с практической разработкой конкретных языков программирования, для теоретических целей представляется неуместным. Поэтому произведем замену терминов.

Шампур-схема — абстрактная дракон-схема. Подчеркнем, что шампур-схема по определению является абстрактной, т. е. полностью лишенной текста.

Шампур-язык — язык шампур-схем. Для шампур-языка задан только визуальный синтаксис, текстовый синтаксис не определен.

ШАМПУР-СХЕМА КАК АБСТРАКТНАЯ
МОДЕЛЬ ПРОГРАММЫ

Уже говорилось, что для видеопрограммирования характерно “расщепление синтаксиса”. Синтаксис S распадается на визуальный синтаксис S 0, определяющий правила построения шампур-схем, и текстовый синтаксис S 1, задающий алфавит текстоэлементов и правила записи текстовых операторов внутри икон. Исходя из этого, можно сказать, что шампур-программа В состоит из двух частей: В 0и В 1, где В 0— шампур-схема с синтаксисом S 0; B 1— текстовая часть программы, т. е.
совокупный текст, находящийся во всех иконах программы, определяемый синтаксисом S 1.

Бросается в глаза несомненное сходство между шампур-схемами и схемами программ. Заметив эту аналогию и повторяя — с некоторыми, почти очевидными изменениями — общую канву рассуждений, принятую в схематологии [7], можно сделать вывод, что шампур-схема В0описывает уже не одну программу, а целый класс программ, т. е. является полипрограммой, а шампур-язык служит мультиязыком — языком полипрограммирования [8].

Класс шампур-схем является подклассом класса крупноблочных схем, по степени абстрактности занимающий промежуточное положение где-то между схемами Мартынюка и стандартными схемами. Связь между шампур-схемами и схемами программ имеет фундаментальный характер и порождает ряд интересных проблем, связанных, в частности, с тем, что “задача эффективизации транслируемых программ перерастает в задачу автоматизации конструирования качественных программ” [8].

С точки зрения теории видеопрограммирования, граф-схемы, используемые в (текстовом) теоретическом программировании, обладают недостатком — как и обычные блок-схемы прикладного программирования, они являются неформальными. Хотя в работах А. Ершова сделан определенный шаг к формализации граф-схем, однако предложенное им решение [9] нельзя признать удовлетворительным, ибо использованный Ершовым визуальный синтаксис граф-схем не позволяет получить однозначную, строго детерминированную визуальную конфигурацию (топологию) граф-схем и, следовательно, не дает единственного решения визуальной задачи.

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

ПРЕОБРАЗОВАНИЕ ШАМПУР-СХЕМЫ
В ШАМПУР-ПРОГРАММУ

Подчеркнем еще раз, что построенный нами язык (шампур-язык) — это не язык программирования, а язык крупноблочных схем программ, т. е. язык полипрограммирования. Однако его можно легко превратить
в язык программирования, причем сделать это многими способами.
Для этого необходимо дополнительно задать текстовый синтаксис S 1и семантику Q 1текстовых операторов, помещаемых в иконах шампур-схемы. Например, если взять текстовый синтаксис и семантику, соответствующие языку ПАСКАЛЬ, получим язык визуального программирования, который можно назвать “шампур-паскаль”. Аналогично можно построить языки шампур-бейсик, шампур-си и т. д.

Используя терминологию схематологии, можно сказать, что шампур-программа есть интерпретированная шампур-схема, однако понятие интерпретации в нашем случае заметно отличается от классического [7]. Детальное рассмотрение вопроса выходит за рамки книги, ограничимся лишь кратким замечанием. Чтобы задать интерпретацию шампур-схемы и превратить ее в шампур-программу, необходимо, во-первых, доопределить шампур-язык и превратить его в язык программирования, описав синтаксис S 1и семантику Q 1текстовых операторов. Во-вторых, следует указать конкретные текстовые операторы, записанные в соответствии с синтаксисом S 1и размещенные в иконах шампур-схемы В 0.Тем самым будет задана текстовая часть В 1шампур-программы В. Таким образом, интерпретация шампур-схемы определяется как тройка < S 1, Q 1, B 1 >.

Отсюда вытекает следующее очевидное замечание. Поскольку шампур-язык есть абстрактная модель любого императивного языка программирования (импер-языка), постольку импер-язык есть интерпретированный шампур-язык. При этом интерпретация шампур-языка, превращающая его в конкретный импер-язык, определяется как пара < S 1, Q 1 >.

ШАМПУР-МЕТОД И ДОКАЗАТЕЛЬСТВО
ПРАВИЛЬНОСТИ ПРОГРАММ

Согласно Р. Андерсону, “целью многих исследований в области доказательства правильности программ является... механизация таких доказательств” [10]. Д. Грис указывает, что “доказательство должно опережать построение программы” [11]. Объединив оба требования, получим, что автоматическое доказательство правильности должно опережать построение программы. Нетрудно убедиться, что шампур-метод обеспечивает частичное выполнение этого требования. В самом деле, в начале главы было показано, что любая правильно построенная шампур-схема является строго доказанной теоремой. В алгоритмах ДРАКОН-редактора закодировано исчисление икон, поэтому любая шампур-схема, построенная с его помощью, является истинной, т. е. правильно построенной. Это означает, что ДРАКОН-редактор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса. Поскольку шампур-схема является частью шампур-программы, сказанное равносильно доказательству частичной правильности шампур-программы.

В начале главы мы задали смешной вопрос: если дракон-схемы — это теоремы, кто должен их доказывать? Ответ прост. Их никто не должен доказывать, так как все они раз и навсегда доказаны благодаря тому, что работа ДРАКОН-редактора построена как реализация исчисления икон.

А теперь добавим ложку дегтя в бочку меда. К сожалению, данный метод позволяет доказать правильность шампур-схемы и только. Это составляет лишь малую часть от общего объема работы, которую нужно выполнить, чтобы доказать правильность программы на все 100%. Правда, есть небольшое утешение: частичное доказательство правильности программы с помощью ДРАКОН-редактора осуществляется без какого-либо участия человека и достигается совершенно бесплатно, так как дополнительные затраты труда, времени и ресурсов не требуются. А дареному коню в зубы не смотрят.

ВОЗМОЖНА ЛИ ТЕОРИЯ ВИЗУАЛЬНОГО ПРОГРАММИРОВАНИЯ?

Хотя видеопрограммирование — сравнительно молодое направление, в этой области уже имеется значительное число интересных прикладных разработок. Однако теоретическое визуальное программирование только зарождается. В доступной литературе автору удалось обнаружить всего несколько строк, которые можно в какой-то степени трактовать как программу будущих исследований в области теории видеопрограммирования: “Для визуального программирования необходимо провести строгие научные обоснования, математические определения и модели — большинство разработок в этой области носит пока эмпирический
характер. Перспективным может быть применение при графическом интерфейсе техники искусственного интеллекта, которая обычно используется для описания прикладной области. Система представления знаний может включать набор визуальных примитивов, их символические описания и правила вывода заключений” [12].

Как, вероятно, заметил читатель, в настоящей работе, решая сходную проблему (проблему вывода заключений путем выполнения формальных операций над визуальными примитивами, в качестве которых использовались иконы шампур-схем), мы пошли несколько иным путем. Отличие заключается в следующем. Авторы цитированной работы говорят о “символических описаниях” визуальных примитивов, подразумевая текстовые правила вывода заключений, принятые в традиционной текстовой математической логике. Однако еще А. Ершов при построении исчисления равносильных преобразований схем Янова предпринял первую попытку отойти от “чисто текстовой” математической логики, используя в формулах правил вывода не только символические описания, но и графические изображения [9, 13]. Вместе с тем метод Ершова из-за дефектов визуального синтаксиса нельзя считать полностью формальным.