OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Четверг, 19 Сентябрь, 2019 08:04

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




Начать новую тему Эта тема закрыта, вы не можете редактировать и оставлять сообщения в ней.  [ 1 сообщение ] 
Автор Сообщение
СообщениеДобавлено: Пятница, 29 Октябрь, 2010 12:52 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9139
Откуда: Россия, Орёл
Хотелось бы зафиксировать понимание так называемого "доказательного", "убедительного" программирования.
Не раз уже здесь мы проводили сравнения с другими отраслями инженерного дела, где с помощью различного математизированного аппарата конструктор может изучать, проверять и убеждать других в свойствах создаваемых им конструкций.

В связи с доказательным программированием, бывают две проблемы: - непринятия его целей и методов; - непонимание того, что есть доказательность.
Говоря простыми словами, доказательность, в любой сфере, - это представление рассматриваемого явления в такой форме, что утверждения относительно него (например, о его правильности) становятся очевидными, для любого человека, но при условии определённой (зависящей от применённого представления) теоретической/методической подготовки.

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

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

(ветка закрыта для обсуждения как флеймоопасная, желающие дискутировать могут завести свою ветку во Флейме или в Опять-25. Важное и по делу перенесём сюда).


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Эта тема закрыта, вы не можете редактировать и оставлять сообщения в ней.  [ 1 сообщение ] 

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


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

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


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

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