На лекции 11 апреля состоится контрольная работа по спецификации. В контрольной работе будет два задания. В первом задании нужно будет написать спецификацию для типа данных и операций над ним (как в домашней работе №8). Во втором задании будет дана реализация функции и спецификация для нее и нужно будет вставить аннотации в текст функции, чтобы связка инструментов frama-c+jessie2+why3+солверы доказала полную корректность этой реализации относительно ее спецификации. В реализации будут использоваться указатели, при верификации надо учитывать разделение по регионам.
Как всегда, на контрольной работе можно пользоваться любыми письменными и печатными материалами, а пользоваться электронной техникой нельзя. После написания контрольной работы можно сдавать практическое задание.