ΑZ
небесплатно оборачивать все либы которые юзаешь
Size: a a a
2020 August 24
CD
зачем мне это делать
CD
я могу конфигурировать вычислители над прослойкой над ними
CD
прослойка над любой либой - почти что обязательное требование
CD
если мы не прототипчик на Rust лабаем, который завтра выбросим
p
есть некоторая новость, что в плюсах человека, который не может соблюдать такие правила, лучше не пускать в проект
Все люди ошибаются. То есть у вас на проекте нет людей? Ну да, ты же плюсовик, у вас только киборги могут работать.
CD
Все люди ошибаются. То есть у вас на проекте нет людей? Ну да, ты же плюсовик, у вас только киборги могут работать.
Есть очень разные ошибки
p
это значит, что им не важен тип ошибки
Как это? Конечно важен.
CD
Все люди ошибаются. То есть у вас на проекте нет людей? Ну да, ты же плюсовик, у вас только киборги могут работать.
И существуют средства, которые приводят к WA#1/OK с очень большой вероятностью, то есть либо работает никогда, либо всегда
p
ничто не спасает от необходимости тестирования
Верификация спасает от необходимости тестирования логики
CD
Верификация спасает от необходимости тестирования логики
нет, конечно
p
нет, конечно
Конечно, да
CD
Конечно, да
верификация утверждает только непротиворечивость описания
EG
Верификация спасает от необходимости тестирования логики
Нет, конечно.
p
верификация утверждает только непротиворечивость описания
Верификация утверждает что тело функции выполняет условия сигнатуры.
EG
Верификация спасает от необходимости тестирования той части логики, которая выражена в сигнатуре.
p
А любые тесты можно выразить в сигнатуре либо в лемме
EG
Выразить всю логику в сигнатуре неоправданно дорого, даже на предназначенных для этого языках типа идриса.
CD
Верификация утверждает что тело функции выполняет условия сигнатуры.
Именно
EG
А любые тесты можно выразить в сигнатуре либо в лемме
В теории — да. На практике это может быть очень дорого/сложно.