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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Задача 6 (PVS))
Текущая версия (18:31, 18 декабря 2012) (править) (отменить)
(преобразование индексов к нижнему регистру)
 
Строка 45: Строка 45:
=== Решение ===
=== Решение ===
-
1. Инвариант в B: P(x1, x2, y1, y2) is φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) '' // в условии не задан, придумываем сами''
+
1. Инвариант в B: P(x<sub>1</sub>, x<sub>2</sub>, y<sub>1</sub>, y<sub>2</sub>) is &phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) '' // в условии не задан, придумываем сами''
Имеем 3 пути:
Имеем 3 пути:
* S-B
* S-B
-
:: &forall; x1 &forall; x2 [(x1 >= 0) &and; (x2 > 0) => &phi;(x1, x2) &and; (x1 = x2*0 + x1) &and; (x1 >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать &and; (y1 = 0) &and; (y2 = x1)''
+
:: &forall; x<sub>1</sub> &forall; x<sub>2</sub> [(x<sub>1</sub> >= 0) &and; (x<sub>2</sub> > 0) => &phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*0 + x<sub>1</sub>) &and; (x<sub>1</sub> >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать &and; (y<sub>1</sub> = 0) &and; (y<sub>2</sub> = x<sub>1</sub>)''
* B-T-B
* B-T-B
-
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2) => &phi;(x1, x2) &and; (x1 = x2*(y1+1) + (y2-x2)) &and; ((y2-x2) >= 0)]
+
:: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) &and; (y<sub>2</sub> >= x<sub>2</sub>) => &phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*(y<sub>1</sub>+1) + (y<sub>2</sub>-x<sub>2</sub>)) &and; ((y<sub>2</sub>-x<sub>2</sub>) >= 0)]
* B-F-H
* B-F-H
-
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 < x2) => (x1 = x2*y1 + y2) &and; (y1 < x2)]
+
:: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) &and; (y<sub>2</sub> < x<sub>2</sub>) => (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>1</sub> < x<sub>2</sub>)]
-
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2.
+
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y<sub>2</sub>.
-
Условие корректности: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) => y2 <math>\isin</math> Nat]
+
Условие корректности: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) => y<sub>2</sub> <math>\isin</math> Nat]
-
Условие завершимости: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2) => (y2 > y2-x2) ]
+
Условие завершимости: &forall; x<sub>1</sub> &forall; x<sub>2</sub> &forall; y<sub>1</sub> &forall; y<sub>2</sub> [&phi;(x<sub>1</sub>, x<sub>2</sub>) &and; (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) &and; (y<sub>2</sub> >= 0) &and; (y<sub>2</sub> >= x<sub>2</sub>) => (y<sub>2</sub> > y<sub>2</sub>-x<sub>2</sub>) ]
=== Комментарии ===
=== Комментарии ===

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

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

Содержание

[править] Задача 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(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 обязательно должны быть явно выписаны условия корректности и завершимости.
  • Не забывать ставить ВСЕ условия прохождений по веткам.
  • Помните, что подставлять изменённые значения, необходимо не только в правой части а везде, где они меняются (к примеру, если путь проходит через 2 условия, то второе к оменту вхождение может иметь уже изменённую переменную).

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

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


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


Лекции

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

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

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