Описывается трансформация и верификация программы bus_sort_breadthfirst, принадлежащей ядру ОС Linux и реализующей сортировку устройств, прикрепленных к шине компьютера. Программа трансформируется с языка Си в язык cP с раскрытием макросов, реорганизацией структур и устранением указателей. Далее программа преобразуется на язык функционального программирования WhyML. Для полученной программы строится спецификация и проводится дедуктивная...

В статье представлена модель баз данных, основанная на последовательности объектов. Рассмотрены вопросы сериализации/десериализации объектов, индексных построений, структуры и методов универсальной последовательности и универсального индекса, реализация полного базиса редактирования через использование первичного ключа, временной отметки и «пустого» значения.

Показано, что спецификация на языке Event-B представима автоматной программой в виде недетерминировнной композиции простых условных операторов, что соответствует узкому подклассу автоматных программ. Спецификация в Event-B является монолитной. Для построения спецификации нет других средств композиции, кроме уточнения, реализующего расширение ранее построенной спецификации. Сравнение технологий автоматного программирования и Event-B проводится на примере...

В статье представлены результаты экспериментов по конъюнктивной декомпозиции различных представлений булевых функций (ZDD, BDD, OKFDD, AIG) методами, которые получаются путем специализации общего алгоритма декомпозиции. Тестовыми наборами являются случайные булевы функции с различными параметрами, а также набор широко известных бенчмарков, используемых для тестирования алгоритмов оптимизации логических схем. В сравнении участвуют последовательная...