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

Написать контракт ACSL для сигнатуры заданной функции, соответствующий данному требованию.

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

Четвёртая домашняя работа блока методов Флойда

Срок сдачи этой домашней работы — семинар 17 марта.

Доказать полную корректность блок-схемы относительно заданного контракта. Доменом всех переменных является множество целых чисел.

Читать далее «Четвёртая домашняя работа блока методов Флойда»

Третья домашняя работа блока методов Флойда

  1. Доказать, что заданная блок-схема успешно завершается при заданном предусловии при помощи метода фундированных множеств Флойда. Доменом всех переменных является множество целых чисел.
    Читать далее «Третья домашняя работа блока методов Флойда»

Вторая домашняя работа блока методов Флойда

Стоит доделать задание, которое разбиралось на семинаре.

Основное задание:
доказать методом индуктивных утверждений Флойда частичную корректность следующей блок-схемы относительно заданной спецификации.

Читать далее «Вторая домашняя работа блока методов Флойда»

Первая домашняя работа блока методов Флойда


Доменом всех используемых в блок-схемах переменных является множество целых чисел. В блок-схемах разрешается использовать только сложение, вычитание, умножение, целочисленное деление, взятие остатка от деления и все виды арифметических сравнений (равно, не равно, больше, меньше и т.п.).

Читать далее «Первая домашняя работа блока методов Флойда»