МФСП: Оформление задач
Материал из eSyr's wiki.
(→Задача 1 - доб. условие) |
|||
| Строка 2: | Строка 2: | ||
== Задача 1== | == Задача 1== | ||
| + | Первая задача: по явному описанию функции построить неявное, т.е. переписать первоую часть и добавить пост и пред-условия. | ||
| + | |||
| + | '''Важно''': в пост-условиях не должно быть локальных переменных | ||
| + | |||
| + | '''Условие''': | ||
| + | '''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 kornevgen], дерево рисовать не обязательно:<blockquote>"@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!"</blockquote> | |
== Задача 5, метод Флойда== | == Задача 5, метод Флойда== | ||
Версия 12:03, 27 января 2010
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
Содержание |
Задача 1
Первая задача: по явному описанию функции построить неявное, т.е. переписать первоую часть и добавить пост и пред-условия.
Важно: в пост-условиях не должно быть локальных переменных
Условие:
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й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!"
Задача 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 
Nat]
Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => (y2 > y2-x2) ]
Комментарии
Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.
