В этом задании вам предлагается попробовать применить инструмент дедуктивной верификации к (почти) реальным исходным текстам на языке Си. В качестве таких текстов выбрана часть ядра операционной системы JOS. Более точно, структуры данных и функции, позволяющие организовать список ограниченного размера с быстрой вставкой в конец и удалением произвольного элемента из списка. Эта структура данных используется для организации таблицы процессов в данном ядре. Вы уже знакомы с этой операционной системой по курсу «Конструкирование ядра операционной системы» (лектор — Хорошилов А.В.).
Скачайте архив с исходными текстами по этой ссылке.
Ваша задача — написать спецификацию для структуры данных struct Env на разных уровнях абстракции, для глобальных переменных и для функций env_init(), env_alloc() и env_free() также на разных уровнях абстракции. То есть необходимо предусмотреть возможность наличия нескольких различных реализаций, удовлетворяющих интерфейсу, описанному в заголовочных файлах.
Если вам трудно сформулировать требования корректности списка свободных блоков, ничего страшного, напишите столько требований, насколько сможете. Кроме того, можно для начала опустить спецификацию структур, описывающих виртуальную память, и требования к выбору идентификаторов создаваемых процессов.
После написания спецификации попробуйте доказать корректность выданной реализации и, если такое случится, найти и объяснить ошибки в ней.