Исследуем AI-first разработку, кодовые ограждения и архитектуру одноразовости.
Large language models — неплохие партнёры для brainstorming при открытии test oracles, но они hallucinate свойства и упускают domain constraints. Вот как использовать их, не выкатывая фиктивные тесты.
Вам нужно протестировать функцию, где правильный вывод невозможно знать заранее. Оптимизатор маршрутов. Классификатор sentiment. Физическая симуляция. Вы…
Не все metamorphic relations ловят баги. Слабые соотношения дают ложную уверенность, а сильные находят реальные дефекты. Вот как отличить их и построить набор соотношений, который реально работает.
Вы написали двенадцать metamorphic relations для вашего pricing engine. Каждый тест проходит. Вы довольны своим покрытием. Затем клиент сообщает, что bulk…
Metamorphic testing позволяет проверять корректность кода, не зная точного ожидаемого вывода. Вот как это работает, когда чего-то не хватает, и как начать использовать.
Вы выкатываете модель машинного обучения, которая маркирует тикеты поддержки. Ваш test suite зелёный. Каждый тест пройден. Ни один из этих тестов на самом деле…
Как использовать phantom types и параметры `this`, чтобы превращать недопустимые переходы протокола в ошибки компиляции вместо runtime-багов.
В каждом клиенте API прячется конечный автомат. Сначала handshake. Потом аутентификация. Затем отправка данных. Закрытие в конце. Нарушьте этот порядок —…
Спецификации OpenAPI описывают схемы запросов и ответов, но не задают допустимые последовательности сообщений. Вот как извлечь то, что можно, и где всё ещё нужно заполнять пробелы.
Спецификации OpenAPI говорят, как выглядит корректный запрос и как выглядит корректный ответ. Они не говорят, можно ли вызывать до , или что произойдёт, если…
Типы сессий кодируют коммуникационные протоколы в системе типов, превращая runtime-ошибки протоколов в ошибки компиляции. Вот почему они провели тридцать лет в исследовательских статьях, прежде чем продакшн-код смог их использовать.
Типы сессий были изобретены в 1993 году. Тридцать лет спустя большинство сетевых сервисов всё ещё валидируют состояние протокола с помощью ручных…
Типы сессий кодируют коммуникационные протоколы в вашей системе типов, превращая несоответствия передачи сообщений в ошибки компилятора до того, как ваш код запустится.
Deadlocks должны быть проблемой времени выполнения. Именно это их так раздражает. Ваш код компилируется чисто, ваши тесты проходят, а затем он застревает в…
Как запускать формальный статический анализ в CI-пайплайне с помощью Infer, с рабочими конфигами и реалистичными компромиссами.
Abstract interpretation — это тот термин, от которого инженеры закрывают вкладку. Звучит так, будто нужен семестр теории решёток, чтобы понять. Большинство…
Большие языковые модели могут помочь в триаже ложноположительных срабатываний статического анализа, но они не понимают семантику программ так, как это делает abstract interpretation. Вот как совместить оба подхода.
Ваш статический анализатор только что выдал 847 предупреждений в пятничный полдень. Вы знаете статистически, что где-то между 5% и 15% из них — настоящие баги.…
Как Facebook использовал abstract interpretation и намеренную unsoundness для поиска race conditions в масштабе миллионов строк Android-кода.
У приложения Facebook для Android была проблема с производительностью. UI-thread тонул в работе, но перенос кода в фоновые потоки означал race conditions.…