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

Материал из 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) /\ (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) ]