2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3, 4
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение25.07.2024, 08:29 
Заслуженный участник
Аватара пользователя


28/09/06
10834
StepV в сообщении #1647246 писал(а):
Заказчик никогда не формирует требования к отдельным алгоритмам (только очень крайний случай, когда требуется что-то специализированное). Заказчик формирует требования к задаче: вход, выход, перечисление функций.

А я о чём? Определяет входы, выходы и действия (функции - слишком многозначное слово, которое может означать разное в зависимости от контекста). И всё это - только для типовых сценариев использования продукта. А алгоритм - это тот продукт, который будет разработан.

StepV в сообщении #1647246 писал(а):
Все вами перечисленное входит в обязанности программистов и алгоритмистов, которые по договору нанялись решать задачу.

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

 Профиль  
                  
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение25.07.2024, 14:57 
Заслуженный участник
Аватара пользователя


28/09/06
10834
EminentVictorians в сообщении #1647105 писал(а):
Интересно. Я тоже думал, что там доказательное программирование, а не тесты.

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

Но вот незадача: Если аргумент достаточно большой (далеко до упоминавшегося ранее миллиарда), то программа вылетает даже не по переполнению основного регистра, а по банальному stack overfow, ибо на деле выполняется рекурсивный вызов одной и той же простой подпрограммы. Вот как мы должны так "доказательно программировать", чтобы пользователь в ответ на ввод аргумента получал всегда разумные ответы, т.е., например, "Введённое число слишком большое", а не "Переполнение стека в строке 5678 модуля fig.ego.znaet.gde"?

 Профиль  
                  
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение25.07.2024, 18:56 


22/10/20
1185
epros в сообщении #1647324 писал(а):
Кстати, а что это за штука такая?
К самой программе добавляем её верификацию на чем-нибудь типа Coq. Я, если что, здесь и близко не специалист; за всю жизнь посмотрел только 1 курс лекций по Coq на ютубе, немного потыкал этот язык и всё. Не моя тема.

 Профиль  
                  
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение25.07.2024, 19:37 


14/01/11
3019
epros в сообщении #1647324 писал(а):
Но вот незадача: Если аргумент достаточно большой (далеко до упоминавшегося ранее миллиарда), то программа вылетает даже не по переполнению основного регистра, а по банальному stack overfow, ибо на деле выполняется рекурсивный вызов одной и той же простой подпрограммы.

Разве там не используется хвостовая рекурсия?

 Профиль  
                  
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение25.07.2024, 21:28 
Заслуженный участник
Аватара пользователя


20/08/14
8484
EminentVictorians в сообщении #1647343 писал(а):
К самой программе добавляем её верификацию на чем-нибудь типа Coq.
Никогда не имел дела с Coq, но если я правильно понимаю, как это устроено, то сложность верификации растет намного быстрее, чем сложность программы. То есть верифицировать программу управления космической ракетой почти невозможно.

 Профиль  
                  
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение25.07.2024, 22:35 


14/01/11
3019
Если работу некоторого программного/аппаратного модуля можно свести к конечному автомату, его можно формально проверить, для этого есть множество средств, и они бурно развиваются.
https://en.wikipedia.org/wiki/Model_checking

 Профиль  
                  
 
 Re: Трудновыявляемые ошибки в алгоритмах
Сообщение26.07.2024, 10:54 
Заслуженный участник
Аватара пользователя


28/09/06
10834
EminentVictorians в сообщении #1647343 писал(а):
К самой программе добавляем её верификацию на чем-нибудь типа Coq.

Это я к тому, что программа на Прологе - сама по себе "доказательство". Там записывается не порядок выполнения действий, а непосредственно рекурсивное определение факториала. Так что как-то дополнительно "доказывать", что этот код считает именно факториал, было бы несколько странно.

Однако то, что этот подсчёт аварийно не завершится из-за недостаточности каких-то ресурсов доказывать, наверное, как-то надо. Но как?

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 52 ]  На страницу Пред.  1, 2, 3, 4

Модератор: Модераторы



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

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


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

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group