МФСП: Оформление задач
Материал из eSyr's wiki.
(→Решение) |
м |
||
| Строка 15: | Строка 15: | ||
(y1, y2) = (y1+1, y2-x2) HALT: (z1, z2) = (y1, y2) | (y1, y2) = (y1+1, y2-x2) HALT: (z1, z2) = (y1, y2) | ||
</pre> | </pre> | ||
| - | Предусловие: φ(x1, x2): x1 >= 0 | + | Предусловие: φ(x1, x2): x1 >= 0 ∧ x2 > 0 |
| - | Постусловие: ψ(x1, x2, z1, z2): x1 = x2*z1 + z2 | + | Постусловие: ψ(x1, x2, z1, z2): x1 = x2*z1 + z2 ∧ z1 < x2 |
=== Решение === | === Решение === | ||
| - | 1. Инвариант в B: P(x1, x2, y1, y2) is φ(x1, x2) | + | 1. Инвариант в B: P(x1, x2, y1, y2) is φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) '' // в условии не задан, придумываем сами'' |
Имеем 3 пути: | Имеем 3 пути: | ||
* S-B | * S-B | ||
| - | :: ∀ x1 ∀ x2 [(x1 >= 0) | + | :: ∀ x1 ∀ x2 [(x1 >= 0) ∧ (x2 > 0) => φ(x1, x2) ∧ (x1 = x2*0 + x1) ∧ (x1 >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать ∧ (y1 = 0) ∧ (y2 = x1)'' |
* B-T-B | * B-T-B | ||
| - | :: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) | + | :: ∀ 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 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 < x2) => (x1 = x2*y1 + y2) ∧ (y1 < x2)] |
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2. | 2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2. | ||
| - | Условие корректности: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) | + | Условие корректности: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) => y2 <math>\isin</math> Nat] |
| - | Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) | + | Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => (y2 > y2-x2) ] |
=== Комментарии === | === Комментарии === | ||
Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости. | Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости. | ||
Версия 12:49, 22 декабря 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 обязательно должны быть явно выписаны условия корректности и завершимости.
