DRAKON.SU

Текущее время: Четверг, 15 Ноябрь, 2018 22:47

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 6 ] 
Автор Сообщение
СообщениеДобавлено: Среда, 20 Июнь, 2018 18:40 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 3806
Откуда: Москва
Proofs of correctness.
Для Рифата

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

Вложение:
Mills Harlan doczilla.tips_proofs-of-correctness.pdf [1.16 МБ]
Скачиваний: 107


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 21 Июнь, 2018 19:40 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 217
Откуда: Казань
Доказательство программ - это правильно, это гораздо лучше, чем программирование по интуиции. Структурное программирование - это тоже правильно, кто бы что ни говорил.

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 21 Июнь, 2018 20:03 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 3806
Откуда: Москва
Рифат, спасибо и давайте забудем про дракон.

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

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 21 Июнь, 2018 23:59 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Июнь, 2018 09:01 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 3806
Откуда: Москва
Рифат, это совсем не Миллз.
Это анонимный материал.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 22 Июнь, 2018 10:56 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 217
Откуда: Казань
Хорошо, не Миллз создал эту презентацию. Но Harlan Mills там фигурует. В общем, где говорится о его наработках, я не со всем согласен.

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


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 6 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2008-2018, участники конференции «DRAKON.SU», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB