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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Задача 5, метод Флойда)
Текущая версия (18:31, 18 декабря 2012) (править) (отменить)
(преобразование индексов к нижнему регистру)
 
(9 промежуточных версий не показаны.)
Строка 1: Строка 1:
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
-
== Задача 5, метод Флойда==
+
== Задача 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'''
 +
 
 +
===Комментарии===
 +
*Как любезно заметил [http://twitter.com/kornevgen/status/7015914018 kornevgen], дерево рисовать не обязательно:<blockquote>"@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!"</blockquote>
 +
*'''Важно''': в пост-условиях не должно быть локальных переменных и присваиваний
 +
 
 +
==Задача 2 (AX)==
 +
'''Комментарии''':
 +
* если в сигнатуре функция определена на множестве ВСЕХ входных данных (потому что там -> а не -~->), то нельзя добавлять предусловие в описание функции -- необходимо это условие запихать в тело функции (т.е. если не удовлетворяет ему, то просто не меняется множество).
 +
 
 +
==Задача 3 (RFN)==
 +
==Задача 4 (INV)==
 +
Тут главное -- просто пишите побольше, от души -- и вам поставят полный балл за задачу. ;)
 +
 
 +
== Задача 5 (FL, метод Флойда)==
===Условие===
===Условие===
<pre>
<pre>
Строка 15: Строка 41:
(y1, y2) = (y1+1, y2-x2) HALT: (z1, z2) = (y1, y2)
(y1, y2) = (y1+1, y2-x2) HALT: (z1, z2) = (y1, y2)
</pre>
</pre>
-
Предусловие: &phi;(x1, x2): x1 >= 0 /\ x2 > 0
+
Предусловие: &phi;(x1, x2): x1 >= 0 &and; x2 > 0
-
Постусловие: &psi;(x1, x2, z1, z2): x1 = x2*z1 + z2 /\ z1 < x2
+
Постусловие: &psi;(x1, x2, z1, z2): x1 = x2*z1 + z2 &and; z1 < x2
=== Решение ===
=== Решение ===
-
1. Инвариант в B: P(x1, x2, y1, y2) is &phi;(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) /\ (x2 > 0) => &phi;(x1, x2) /\ (x1 = x2*0 + x1) /\ (x1 >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать /\ (y1 = 0) /\ (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) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 >= x2) => &phi;(x1, x2) /\ (x1 = x2*(y1+1) + (y2-x2)) /\ ((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) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 < x2) => &phi;(x1, x2) /\ (x1 = x2*y1 + y2) /\ (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) /\ (x1 = x2*y1 + y2) /\ (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) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (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>) ]
=== Комментарии ===
=== Комментарии ===
-
Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.
+
* Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.
 +
* Не забывать ставить ВСЕ условия прохождений по веткам.
 +
* Помните, что подставлять изменённые значения, необходимо не только в правой части а везде, где они меняются (к примеру, если путь проходит через 2 условия, то второе к оменту вхождение может иметь уже изменённую переменную).
 +
 
 +
==Задача 6 (PVS)==
 +
'''ГЛАВНОЕ'''! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.
 +
* [[МФСП, 12 лекция (от 26 ноября)|Пример, разбиравшийся на лекции]]
 +
* [[http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc|Ещё пример от Алексея Хорошилова]]
 +
 
 +
{{Курс МФСП}}

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

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

Содержание

[править] Задача 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

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

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