DRAKON.SU

Proofs of correctness.
Для Рифата

Материал по структурному программированию.
я скачал его здесь
https://doczilla.tips/download-pdf-proo ... tness.html

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

Что можно сказать по поводу связи с Драконом? В принципе все эти принципы можно использовать и в Драконе, если ограничиться только некоторыми возможностями Дракона и не использовать другие возможности, тогда будет возможность применять доказательство алгоритмов в Драконе. Основное требование, чтобы у любой "логической" конструкции был один вход и один выход. Что я подразумеваю под "логической" конструкцией: условный оператор, оператор цикла и последовательность операторов. В Драконе бывает сложно выделить "логические" операторы из-за достаточно произвольных правил обращения с ветками (ака. шампурами). Какие возможны случаи:
- ветка содержит целое число только структурных операторов (которые можно разложить на состовные части: последовательности, условия, циклы с одном входом и одним выходом);
- ветка содержит произвольный поток управления (ака. лапша), который никак нельзя разложить на последовательности, условия, циклы с одним входом и одним выходом;
- несколько веток содержат целое число "логических операторов", то есть каждая ветка в отдельности может содержать нецелое число "логических операторов". Этот случай также можно разбить на два, когда объединив ветки можно получить только структурные операторы или же произвольный поток управления. Например, в первой ветке может быть условие и сразу два выхода из ветки, каждая из которых переходит на другие ветки. В этих других ветках по одному действию, а переходят они оба к завершающему действию. В этом случае во всей схеме один "логический" оператор верхнего уровня - условие, которое распадается на 3 ветки. Это пример структурной схемы. Но, различными переходами на разные ветки, очень легко создать неструктурный алгоритм, который нельзя будет разложить на последовательности, условия и циклы с одним входом и одним выходом.

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

Рифат, спасибо и давайте забудем про дракон.

Мне интересно ваше мнение по поводу
"Proofs of correctness".

Вы согласны с содержанием этого материала?

Или там есть спорные моменты?

Как вы считаете?

Детальный анализ этой презентации займет много времени.
А так вкратце могу сказать, что все что Миллз рассказывает о чужих открытиях, к этому нет претензий.
К тому, что Миллз рассказывает о своих изысканиях, есть определенные претензии:
- Для верификации вводит какие-то функции. Когда для этого есть тройки Хоара или слабейшие предусловия Дейкстры.
- Вводит новый термин "Чистая комната", когда можно было бы просто сказать, что разработка велась методом структурного программирования.
- Вводит свой формат записи предусловий и постусловий в программе.

Рифат, это совсем не Миллз.
Это анонимный материал.

Неизвестный автор опубликовал и свои собственные изыскания, пожелав остаться неузнанным

Хорошо, не Миллз создал эту презентацию. Но Harlan Mills там фигурует. В общем, где говорится о его наработках, я не со всем согласен.

P.S. Сейчас посмотрел в интернете про Харлана Милса. Он умер в 1996 году, когда ему было 76 лет.