Типичный программист | IT, программирование, разработка, ИИ
IT и технологии · 11 октября 2026 г.
Модель C-интерфейса в Quint помогла найти больше десяти ошибок в SQLite
Модель C-интерфейса в Quint помогла найти больше десяти ошибок в SQLite SQLite должна отклонить десериализацию базы, пока идёт транзакция чтения. Но в тесте вместо ошибки SQLITE_BUSY, означающей, что база занята, произошло падение. Паван Намби из сообщества Turso моделировал в Quint отдельные контракты C-интерфейса SQLite: что операции должны делать по документации. Quint генерировал последовательности состояний, которые переводили в небольшие программы на C и запускали на настоящей базе. Сравнение ожиданий с поведением SQLite выявило ошибки, пропущенные прежними проверками. В разборе Намби и команды Turso показаны шаги, приведшие к падению, и подход к проверке отдельных контрактов без моделирования всей базы данных. #инструменты