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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: [http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc Пример первой задачи] ...)
Строка 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 (синтаксические ошибки не будут строго караться) и описать последовательность команд, которая приведёт к доказательству его истинности. Дерево строить не надо.
Пример (для первого предиката):
Пример (для первого предиката):

Версия 17:11, 6 декабря 2008

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

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

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

  1. (skolem!)
  2. (skolem!)
  3. (flatten)
  4. (assert)
Личные инструменты
Разделы