CD
А любые тесты можно выразить в сигнатуре либо в лемме
А любую императивную программу можно проверить на корректность на всех тестах)
Size: a a a
2020 August 24
p
Выразить всю логику в сигнатуре неоправданно дорого, даже на предназначенных для этого языках типа идриса.
А ты пишешь для функций тесты на ту логику которая тебе нужна, или для всей логики?
CD
Она же использует конечную память
CD
А ты пишешь для функций тесты на ту логику которая тебе нужна, или для всей логики?
Я не пишу тесты для функций*
*кроме определенного множества
*кроме определенного множества
EG
А ты пишешь для функций тесты на ту логику которая тебе нужна, или для всей логики?
Для нетривиальной логики тесты написать гораздо проще, чем доказать, что она корректна.
p
Я не пишу тесты для функций*
*кроме определенного множества
*кроме определенного множества
А для чего?
CD
А для чего?
У меня вот есть тесты, которые берут входные данные из папочки и определенные результаты запуска на них укладывают в git
EG
Кроме того, при переписывании функции, блэкбокс-тесты сохраняются, а доказательство нужно переделывать.
CD
У меня вот есть тесты, которые берут входные данные из папочки и определенные результаты запуска на них укладывают в git
И они мне говорят, что я конченый долбоеб
CD
Они не указывают конкретное место ошибки
CD
Только что результат вот этого изменился
CD
Если у меня есть какой-то хороший пример, я добавляю в эту папочку
p
А любую императивную программу можно проверить на корректность на всех тестах)
Тесты доказывают что на определенном наборе данных функция имеет определенное поведение. То что происходит на остальных данных неизвестно. Можно конечно благодаря индукции считать что функция работает на всех данных но ничего не мешает добавить if input == 269 { panic!() }
CD
Тесты доказывают что на определенном наборе данных функция имеет определенное поведение. То что происходит на остальных данных неизвестно. Можно конечно благодаря индукции считать что функция работает на всех данных но ничего не мешает добавить if input == 269 { panic!() }
Именно так. Вопрос в том, что такого в коде не будет, и редко срабатывающих ошибок - тоже, не писать их - как раз квалификация
CD
Либо OK либо WA#1
CD
Работает как надо всегда или никогда
p
Для нетривиальной логики тесты написать гораздо проще, чем доказать, что она корректна.
Напиши мне тест который гарантирует что после реверса списка в списке остаются те же самые элементы что и до реверса.
CD
Напиши мне тест который гарантирует что после реверса списка в списке остаются те же самые элементы что и до реверса.
Зачем
EG
Напиши мне тест который гарантирует что после реверса списка в списке остаются те же самые элементы что и до реверса.
Лол, стандартные фпшные примеры
p
Зачем
Он сказал про сложную логику