МФСП, 12 лекция (от 26 ноября)

Материал из eSyr's wiki.

Перейти к: навигация, поиск

Докажем с применением индукции с помощью PVS, что марок номиналом 3 и 5 хватит, чтобы покрыть любую сумму, большую 7.

stamps : THEORY
BEGIN
    stamps : LEMMA
    (FORALL (i : nat) : (i > 7) IMPLIES
    EXIST (t : nat, f : nat) :
        i = 3 * t + 5 * f
    )
END stamps

Сразу применять (skolem!) нельзя, так как мы хотим провести доказательство с использованием индукции. Следовательно, сначала применяем (induct "i"), а потом уже в индуктивном переходе применим (skolem!).

По этому поводу будут 2 задачи:

  1. Написать формулу, получающуюся при решении задачи по методу Флойда и показать, как она будет доказываться в PVS.
  2. Тоже на доказательство в PVS, скорее всего с применением индукции, но не сильно сложное.

Следующая среда — консультация, через раз — коллоквиум.

Ссылки:


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы