МФСП, 13 лекция (от 03 декабря)
Материал из eSyr's wiki.
(Различия между версиями)
| Строка 8: | Строка 8: | ||
# (flatten) | # (flatten) | ||
# (assert) | # (assert) | ||
| + | |||
| + | {{МФСП}} | ||
| + | {{Lection-stub}} | ||
Версия 01:20, 7 декабря 2008
В данной задаче в первом методе Флойда получилось 6 базовых путей и соответствующих предикатов. На коллоквиуме нужно будет каждый из таких предикатов сформулировать на языке теории PVS (синтаксические ошибки не будут строго караться) и описать последовательность команд, которая приведёт к доказательству его истинности. Дерево строить не надо.
Пример (для первого предиката):
- (skolem!)
- (skolem!)
- (flatten)
- (assert)
Формальная спецификация и верификация программ
|
|
Эта статья является конспектом лекции.
Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
