Архив автора: Денис Буздалов

Обновление инструментов

Инструменты обновились сегодня. Настоятельно рекомендуется обновить их перед использованием. Для этого используйте команды opam update и opam upgrade.

Рубрика: Новости | Добавить комментарий

Контрольная работа №2-бис

10 июня в 10:00 состоится вторая контрольная работа по блоку спецификации для пропустивших её 28 апреля. Аудитория проведения станет известна в день проведения, узнавать в 718. Время работы 30 мин.

Рубрика: Новости | Добавить комментарий

Дата экзамена

Экзамен обеих групп состоится 16 июня. Экзамен письменный, проводится с 10:00, длительность ориентировочно три часа. Экзамен проверяется в тот же день, показ работ после проверки, ближе к вечеру. UPD: После начала экзамена (непосредственно после раздачи заданий) можно проставить автоматы.

Рубрика: Новости | Добавить комментарий

Верификационная часть практического задания

Для получения верификационной части практического задания (после успешного выполнения спецификационной части) необходимо добавить вашу спецификацию к файлу map.h и прислать его. К функциям, не присутствующим в вашем варианте, не стоит добавлять никаких спецификационных комментариев. Обратите внимание, что файл map.h со … Читать далее

Рубрика: Новости | Добавить комментарий

Занятие 19 мая

Ближайшее занятие (19 мая) переносится из аудитории 609 в другую из-за проходящего госэкзамена. В какую именно должно быть написано на самой аудитории. Если ничего написано не будет, приходите в аудиторию 718.

Рубрика: Новости | Добавить комментарий

Вторая контрольная работа

На занятии 28 апреля будет проведена контрольная работа по блоку спецификации.

Рубрика: Новости | Добавить комментарий

Занятие 14 апреля

Состоялось практическое занятие по пользованию связкой инструментов frama-c – jessie2 – why3. Были рассмотрены вопросы: установка инструмента: установка OCaml и OPAM; включение OPAM командой в терминале или в .bashrc; использование инструмента; запуск инструмента на заданном файле; набор утверждений верхнего уровня (утверждения *_safety, … Читать далее

Рубрика: Лекции | Добавить комментарий

Практическое занятие 14 апреля

Напоминаю, что 14 апреля на лекции будет практическое занятие по пользованию связкой инструментов frama-c — jessie2 — why3. Постарайтесь, чтобы у всех были ноутбуки. Максимально желательно, чтобы вы попробовали установить связку инструментов. Инструкция по установке.

Рубрика: Новости | Добавить комментарий

Лекция 7 апреля

Состоялась лекция, посвящённая особенностям спецификации структур. Были рассмотрены вопросы: спецификация инвариантов типов: потребность в выражении свойств, относящихся ко всему типу (т.е., к любой функции, работающей со значением данного типа); различие между сильными и слабыми инвариантами (аналогично глобальным инвариантам); возможность выражение … Читать далее

Рубрика: Лекции | Добавить комментарий

Четвёртая домашняя работа блока спецификации

Написать спецификации, отражающие данные требования.

Рубрика: Домашние задания | Добавить комментарий