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

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

(Различия между версиями)
Перейти к: навигация, поиск
Строка 1: Строка 1:
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
 +
 +
== Задача 1==
 +
 +
===Комментарии===
 +
как любезно заметил kornevgen, дерево рисовать не обязательно "@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!" ( http://twitter.com/kornevgen )
== Задача 5, метод Флойда==
== Задача 5, метод Флойда==

Версия 15:42, 28 декабря 2009

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

Содержание

Задача 1

Комментарии

как любезно заметил kornevgen, дерево рисовать не обязательно "@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!" ( http://twitter.com/kornevgen )

Задача 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 \isin Nat]

Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => (y2 > y2-x2) ]

Комментарии

Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.


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


Лекции

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

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

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