19 апреля состоится контрольная работа №2. За полтора часа надо будет решить несколько задач.
Одна задача посвящена спецификации интерфейса модуля на языке Си: спецификации глобальных переменных, типов и функций при помощи языка ACSL. Необходимо понимать, что интерфейсу соответствует не одна реализация, а множество реализаций.
Другая — доказать, что некоторая заданная реализация функции с циклом соответствует заданной спецификации. Нужно будет дополнить реализацию аннотациями на языке ACSL. Для решения этой задачи нужно уметь применять методы Флойда в ACSL.
Работа выполняется без использования компьютера. Можно использовать свои конспекты, иные материалы на бумаге. Электронными материалами и спедствами связи пользоваться нельзя.
После окончания контрольной работы можно будет показывать практическое задание.