МФСП: Оформление задач

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

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

Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.

Содержание

Задача 5, метод Флойда

Условие

                START
          (y1, y2) = (0, x1)
                  |
   -------------->|
   |              B 
   |              |     F
   |           y2 >= x2-------
   |              |T         |
   |              |          |
(y1, y2) = (y1+1, y2-x2)     HALT: (z1, z2) = (y1, y2)

Предусловие: φ(x1, x2): x1 >= 0 ∧ x2 > 0 Постусловие: ψ(x1, x2, z1, z2): x1 = x2*z1 + z2 ∧ z1 < x2

Решение

1. Инвариант в B: P(x1, x2, y1, y2) is φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) // в условии не задан, придумываем сами

Имеем 3 пути:

  • S-B
∀ x1 ∀ x2 [(x1 >= 0) ∧ (x2 > 0) => φ(x1, x2) ∧ (x1 = x2*0 + x1) ∧ (x1 >= 0)] // здесь нужно сразу подставить начальные значения из START, а не писать ∧ (y1 = 0) ∧ (y2 = x1)
  • B-T-B
∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => φ(x1, x2) ∧ (x1 = x2*(y1+1) + (y2-x2)) ∧ ((y2-x2) >= 0)]
  • B-F-H
∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 < x2) => (x1 = x2*y1 + y2) ∧ (y1 < x2)]

2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2.

Условие корректности: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) => y2 \isin Nat]

Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => (y2 > y2-x2) ]

Комментарии

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


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


Лекции

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

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

Личные инструменты
Разделы