Category: лытдыбр

Category was added automatically. Read all entries about "лытдыбр".

иероглифы

coq + imperative algorithm proving

Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз Unix.read (обёртку над read()) не очень гуманно в плане количества вызовов ОС, например.
И решил я реализовать более умный алгоритм чтения-кеширования, читающий в блок размера "дисковый блок * 2", по выравненным смещениям, стараясь читать по границе блока, чтобы не читать ненужные блоки. Однако, кое-где явно нет нужды пропускать данные через буфер, когда ясно, что "цельные блоки" можно прочитать напрямую в строку-получателя.
Но оказалось, что я не смог отладить этот сугубо императивный алгоритм руками, и у меня вообще не было уверенности в том, что он работает правильно. Эти гадские смещения, длины! Невозможно интуитивно проверить, правильно ли сделал. Очень БЕСЕД, знаете ли.

Тогда я взял Coq.
Collapse )