Это задание состоит из 2-х частей. Нужно выполнить все части.

Задание 3.1

Вам дан исходный модуль на языке Си с типами данных и их спецификацией для ориентированных графов. В модуле определены две функции над ориентированным графом и их спецификация. Подробности смотрите в самом модуле.

Напишите WhyML-модель этого исходного модуля и спецификаций. Машинную арифметику можно не моделировать. Присваивание всех полей можно промоделировать заменой структуры целиком. Модель программы должны работать с указателями и моделью памяти.

При помощи Why3 и солверов докажите полную корректность модели программы относительно ее спецификации. Результат вашей работы – это архив следующего состава: файл на языке WhyML, сессия доказательства.

Прагматика В этом задании вы пробуете самостоятельно выполнить действия при дедуктивной верификации Си-программы: составление модели программы, доказательство полной корректности.

Задание 3.2

Вам дан тот же исходный модуль, что и в задании 3.1. Но теперь вам надо доказать полную корректность, вставляя комментарии непосредственно в исходный модуль и используя язык ACSL.

Результат вашей работы – это архив следующего состава: файл на языке Си со спецификационными комментариями, сессия доказательства.

Леммы с более чем одной меткой памяти можно не доказывать (но эти леммы должны быть доказаны в задании 3.1) или воспользоваться макросами для аналогичной цели (как это сделать, написано в статье Towards Full Proof Automation in Frama-C Using Auto-active Verification).

Прагматика В этом задании вы формулируете доказательство непосредственно на уровне исходного кода. Для этого вы пользуетесь пониманием того, как устроена модель памяти.