Недостатки Дракона:

Нет взаимозаменяемости (симметричности) между примитивом и силуэтом. Если на силуэте отображена неструктурная схема, то в примитиве её уже не получится отобразить.

Нет взаимозаменяемости (симметричности) между примитивом и силуэтом.

Если на силуэте отображена [сложная] схема, то в примитиве её уже не получится отобразить.

Роберт Андерсон подчеркивает: «целью многих исследований в области доказательства правильности программ является... механизация таких доказательств» [8].

Дэвид Грис указывает, что «доказательство должно опережать построение программы» [9].

Объединив оба требования, получим, что автоматическое доказательство правильности должно опережать построение алгоритма. Нетрудно убедиться, что предлагаемый метод обеспечивает частичное выполнение этого требования.

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

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

В начале главы мы задали смешной вопрос: если шампур-схемы – это теоремы, кто должен их доказывать? Ответ прост.

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

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

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

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

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

Соедините середину ветки силуэта с любой точкой в середине соседней ветки... Сделайте в дракон-схеме пересечение линий.

МАТЕМАТИКА и доказательное программирование

Примитив и силуэт — это две аксиомы, которые называются:
1. аксиома-примитив
2. аксиома-силуэт

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

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

До этого у меня было другое понимание, что один и тот же алгоритм можно представить или примитивом или силуэтом.

Цикл с двумя входами (один вход в середину цикла) и двумя выходами (один выход из середины цикла) можно описать в силуэте, но скорее всего нельзя описать в примитиве.

И вообще эти аксиомы мне кажутся недостаточно математическими.

Цикл с двумя входами (один вход в середину цикла) и двумя выходами (один выход из середины цикла) можно описать в силуэте, но скорее всего нельзя описать в примитиве.

§9. СЕМАНТИКА ШАМПУР-СХЕМ

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

В исчислении икон семантика тривиальна. Различные визуальные формулы (блок-схемы) могут быть истинными или ложными.

Визуальная формула называется истинной, если она – либо аксиома, либо выводится из аксиом с помощью правил вывода (то есть является теоремой). И ложной в противном случае.

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

Примеры ложных схем показаны на рис. 156, 158, 160, 162, 164.

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

Визуальная формула называется истинной, если она – либо аксиома, либо выводится из аксиом с помощью правил вывода (то есть является теоремой). И ложной в противном случае.

Что же такое ШАМПУР-СХЕМА?