Ефим Карпович · счетовод Монетного двора
Сейф теперь закрывают один раз, спасибо. Но монеты всё равно пропадают из книг, и не из сейфа, а при пересчёте. Пересчёт Касса делает так: перекладывает монеты по одной из мешка в мешок, пока первый не опустеет. Я прогнал его на тридцати мешках, все сошлись. Подрядчик говорит: «значит, программа верна». А я сорок лет считаю монеты и знаю, что тридцать мешков это ещё не все мешки.
Счетовод прав, и спор этот старый. Тесты проверяют программу на тех входах, которые ты придумал. Чтобы сказать «на всех входах», нужно рассуждение о самой программе. В уроке 19 раздела CS ты видел тройку Хоара {P} S {Q} как идею и инвариант цикла как приём для ревью. Сегодня тройки станут суждениями, а приём правилами вывода. Деревья ты строишь с блока F, так что всё знакомо: черта, посылки сверху, заключение снизу. Новое только содержимое суждений.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.