МФСП: Оформление задач
Материал из eSyr's wiki.
(→Задача 5, метод Флойда) |
(→Решение) |
||
Строка 27: | Строка 27: | ||
:: ∀ 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)] | :: ∀ 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 | * B-F-H | ||
- | :: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 < x2) => | + | :: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 < x2) => (x1 = x2*y1 + y2) /\ (y1 < x2)] |
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2. | 2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2. |
Версия 20:52, 21 декабря 2009
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
Содержание |
Задача 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 Nat]
Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 >= x2) => (y2 > y2-x2) ]
Комментарии
Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.