Данная статья является адаптированной русскоязычной версией моей статьи: Handling fold_left in proofs.Функция fold_left , сворачивающая список, довольно популярна во многих (функциональных и не очень) языках программирования. Она есть и в Haskell, и в OCaml и в Rust. Используется чаще, чем fold_right, вероятно потому, что с ее помощью проще писать эффективный код.fold_left и fold_right из библиотеки OCaml library: List. Читать далее
Данная статья является адаптированным переводом моей статьи: Formalization of code in Coq - tactics, написанной в период работы над проектом coq-tezos-of-ocaml. Суть проекта: часть исходного кода протокола криптовалюты Tezos была переведена на Coq, а затем верифицирована с помощью математических методов и…
Продолжаем серию статей о CAP-теореме и языке Coq. В предыдущей части мы детально проанализировали определения CAP-теоремы, готовясь к её формализации на языке Coq, и нашли там серьёзную ошибку (теперь будет о чём поговорить при случае на system design interview).В этой статье мы познакомимся с основами языка Coq и для практики формализуем небольшой фрагмент геометрической системы, близкой к евклидовой. Читать далее
Оглавление Часть 1 1.Введение. 2.Разрезание на части (chunks). 3.Сжатие образов. 3.1.Sparse-файлы. Часть 2 3.2._sparsechunk-файлы. 4.Создание dat-файлов. 5.Источники информации. Структура образов разделов, содержащих файловую систему. 1.Введение Образы разделов мобильных устройств (МУ), содержащих…