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

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

Текущая версия

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

[править] Задача 1 (EI)

Первая задача: по явному описанию функции построить неявное, т.е. переписать первоую часть и добавить пост и пред-условия.

Условие:

value
f: Int X Int -> write x,y,z Int X Int X Int
f(a,b) as (c,d,e)
f(a,b) is x:=2;
  local variable v: Int := 1 in
    for i in <.a..a-1+b.> do
      v:=i*(x=x+v;i)*2  // (ЗДЕСЬ v не успевает обновиться, т.е идет с предыдущего цикла, т.е. Для x последней итерацией (где v=a-1+b) нет)
    end; (y:=z;a,v:=v+1;x,b+v)
  end

[править] Комментарии

• Как любезно заметил kornevgen, дерево рисовать не обязательно:

  "@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!"

• Важно: в пост-условиях не должно быть локальных переменных и присваиваний

[править] Задача 2 (AX)

Комментарии:

• если в сигнатуре функция определена на множестве ВСЕХ входных данных (потому что там -> а не -~->), то нельзя добавлять предусловие в описание функции -- необходимо это условие запихать в тело функции (т.е. если не удовлетворяет ему, то просто не меняется множество).

[править] Задача 3 (RFN)

[править] Задача 4 (INV)

Тут главное -- просто пишите побольше, от души -- и вам поставят полный балл за задачу. ;)

[править] Задача 5 (FL, метод Флойда)

[править] Условие

                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(x₁, x₂, y₁, y₂) is φ(x₁, x₂) ∧ (x₁ = x₂*y₁ + y₂) ∧ (y₂ >= 0) // в условии не задан, придумываем сами

Имеем 3 пути:

• S-B

∀ x₁ ∀ x₂ [(x₁ >= 0) ∧ (x₂ > 0) => φ(x₁, x₂) ∧ (x₁ = x₂*0 + x₁) ∧ (x₁ >= 0)] // здесь нужно сразу подставить начальные значения из START, а не писать ∧ (y₁ = 0) ∧ (y₂ = x₁)

• B-T-B

∀ x₁ ∀ x₂ ∀ y₁ ∀ y₂ [φ(x₁, x₂) ∧ (x₁ = x₂*y₁ + y₂) ∧ (y₂ >= 0) ∧ (y₂ >= x₂) => φ(x₁, x₂) ∧ (x₁ = x₂*(y₁+1) + (y₂-x₂)) ∧ ((y₂-x₂) >= 0)]

• B-F-H

∀ x₁ ∀ x₂ ∀ y₁ ∀ y₂ [φ(x₁, x₂) ∧ (x₁ = x₂*y₁ + y₂) ∧ (y₂ >= 0) ∧ (y₂ < x₂) => (x₁ = x₂*y₁ + y₂) ∧ (y₁ < x₂)]

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

Условие корректности: ∀ x₁ ∀ x₂ ∀ y₁ ∀ y₂ [φ(x₁, x₂) ∧ (x₁ = x₂*y₁ + y₂) ∧ (y₂ >= 0) => y₂ Nat]

Условие завершимости: ∀ x₁ ∀ x₂ ∀ y₁ ∀ y₂ [φ(x₁, x₂) ∧ (x₁ = x₂*y₁ + y₂) ∧ (y₂ >= 0) ∧ (y₂ >= x₂) => (y₂ > y₂-x₂) ]

[править] Комментарии

• Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.
• Не забывать ставить ВСЕ условия прохождений по веткам.
• Помните, что подставлять изменённые значения, необходимо не только в правой части а везде, где они меняются (к примеру, если путь проходит через 2 условия, то второе к оменту вхождение может иметь уже изменённую переменную).

[править] Задача 6 (PVS)

ГЛАВНОЕ! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.

• Пример, разбиравшийся на лекции
• [пример от Алексея Хорошилова]