МФСП, 13 лекция (от 03 декабря)

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: [http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc Пример первой задачи] ...)
 
(3 промежуточные версии не показаны)
Строка 1: Строка 1:
[http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc Пример первой задачи]
[http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc Пример первой задачи]
-
В данной задаче в первом методе Флойда получилось 6 базовых путей и соответствующих предикатов. На коллоквиуме нужно будет каждый из них сформулировать на языке теории PVS (синтаксические ошибки не будут строго караться) и описать последовательность команд, которые приведут к доказательству его истинности. Дерево строить не надо.
+
В данной задаче в первом методе Флойда получилось 6 базовых путей и соответствующих предикатов. На коллоквиуме нужно будет каждый из таких предикатов сформулировать на языке теории PVS (синтаксические ошибки не будут строго караться) и описать последовательность команд, которая приведёт к доказательству его истинности. Дерево строить не надо.
Пример (для первого предиката):
Пример (для первого предиката):
Строка 8: Строка 8:
# (flatten)
# (flatten)
# (assert)
# (assert)
 +
 +
{{МФСП}}
 +
{{Lection-stub}}

Текущая версия

Пример первой задачи

В данной задаче в первом методе Флойда получилось 6 базовых путей и соответствующих предикатов. На коллоквиуме нужно будет каждый из таких предикатов сформулировать на языке теории PVS (синтаксические ошибки не будут строго караться) и описать последовательность команд, которая приведёт к доказательству его истинности. Дерево строить не надо.

Пример (для первого предиката):

  1. (skolem!)
  2. (skolem!)
  3. (flatten)
  4. (assert)


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

Лекции

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

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


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

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_13_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_03_%D0%B4%D0%B5%D0%BA%D0%B0%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы