OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 25 Сентябрь, 2020 07:38

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




Начать новую тему Ответить на тему  [ Сообщений: 5 ] 
Автор Сообщение
 Заголовок сообщения: Формальные методы на практике
СообщениеДобавлено: Понедельник, 23 Июль, 2007 11:19 
Аватара пользователя

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2352
Откуда: Россия, Томск
У меня вдруг родилась вот какая идея. Известно, что корректную программу написать проще, если сначала формально вывести алгоритм, доказать его правильность (т.е. достижимость конечной цели и отсутствие нежелательных побочных эффектов), а затем вывести из формального определения алгоритма конкретный исходный текст программы. На этом пути есть несколько моментов, допускающих человеческую ошибку:
- доказательство правильности алгоритма может быть проведено некорректно;
- в процессе перевода алгоритма из формальной спецификации в текст на конкретном языке программирования могут быть допущены неточности или ошибки;
- особенности языка программирования могут давать побочные эффекты или вносить коррективы, не учтенные в формальной спецификации, потенциально нарушая целостность программы и её соответствие алгоритму (например, переполнение INTEGER в некоторых промежуточных вычислениях).
Почему бы нам не автоматизировать процесс перевода формальной спецификации в текст программы?

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

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

Такие товарищи как Т. Хоар пытаются создать верифицирующий компилятор. Это очень большая и сложная задача, особенно если компилировать Си или ассемблер. А что, если пойти не со стороны анализа, а со стороны синтеза? Не искать смысл в написанном коде, а писать смысл, который будет автоматически отображаться в соответствующий код.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы на практике
СообщениеДобавлено: Понедельник, 23 Июль, 2007 12:09 
Модератор
Аватара пользователя

Зарегистрирован: Среда, 16 Ноябрь, 2005 00:53
Сообщения: 4593
Откуда: Россия, Орёл
Эта идея, насколько мне известно, не нова :) И работы в этом направлении проводились. С несколько более глобальной идеей столкнулся в книге "Концептуальное программирование", автор Тыугу Э.Х. - 1980-х годов:

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы на практике
СообщениеДобавлено: Понедельник, 23 Июль, 2007 12:17 
Аватара пользователя

Зарегистрирован: Пятница, 25 Ноябрь, 2005 18:55
Сообщения: 2272
Откуда: Россия, Нижний Новгород
Александр Ильин писал(а):
...а писать смысл...

Это и есть самая большая трудность присущая программированию. Сотворить смысл труднее всего. Именно из-за этой трудности Фредерик Брукс и заявил, что серебрянной пули нет.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы на практике
СообщениеДобавлено: Понедельник, 23 Июль, 2007 12:33 
Аватара пользователя

Зарегистрирован: Вторник, 19 Сентябрь, 2006 21:54
Сообщения: 2352
Откуда: Россия, Томск
Книжку поищу, спасибо! А названия языков не припомните? Желательно, в open-source-реализациях : )))


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы на практике
СообщениеДобавлено: Понедельник, 23 Июль, 2007 13:16 
Модератор
Аватара пользователя

Зарегистрирован: Среда, 16 Ноябрь, 2005 00:53
Сообщения: 4593
Откуда: Россия, Орёл
Александр Ильин писал(а):
А названия языков не припомните? Желательно, в open-source-реализациях : )))

Про языки читал в самой книжке. Там даже и примеры программ были. Языки нашего, советского производства, так что насчет open-source вопрос...


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

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


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

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


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

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