Практическое задание

В рамках практического задания нужно написать формальную спецификацию требований к некоторой структуре данных и операциях над нею (этап 1) и доказать полную корректность одной из реализаций операций относительно их спецификаций (этап 2). Язык реализации — Си, язык спецификации — ACSL, инструменты доказательства — frama-c+jessie2+why3+солверы.

Этапы задания выполняются последовательно. Реализация для выполнения этапа 2 выдается преподавателем после успешной сдачи этапа 1. Этап 1 сдается только очно, этап 2 может сдаваться заочно. Дни для сдачи этапа 1: 11 апреля, 18 апреля, 25 апреля, 16 мая, с 13:50 до последнего сдающего, но не позднее 17:20. При отсутствии желающих сдавать до 14:05 сдача в данный день прекращается. Преподаватели оценивают правильность выполнения этапа и могут не давать комментариев о месте ошибки в исходных текстах спецификаций. Можно пытаться сдавать несколько раз. Этап 1 считается выполненным только целиком и не оценивается частично.

Текст, общий для всех вариантов задания, и файлы находятся по этой ссылке. Для получения варианта нужно отправить письмо на почту .

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Этот сайт использует Akismet для борьбы со спамом. Узнайте как обрабатываются ваши данные комментариев.