МФСП: Оформление задач
Материал из eSyr's wiki.
(некоторые добавления) |
(преобразование индексов к нижнему регистру) |
||
(1 промежуточная версия не показана) | |||
Строка 45: | Строка 45: | ||
=== Решение === | === Решение === | ||
- | 1. Инвариант в B: P( | + | 1. Инвариант в B: P(x<sub>1</sub>, x<sub>2</sub>, y<sub>1</sub>, y<sub>2</sub>) is φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) ∧ (y<sub>2</sub> >= 0) '' // в условии не задан, придумываем сами'' |
Имеем 3 пути: | Имеем 3 пути: | ||
* S-B | * S-B | ||
- | :: ∀ | + | :: ∀ x<sub>1</sub> ∀ x<sub>2</sub> [(x<sub>1</sub> >= 0) ∧ (x<sub>2</sub> > 0) => φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*0 + x<sub>1</sub>) ∧ (x<sub>1</sub> >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать ∧ (y<sub>1</sub> = 0) ∧ (y<sub>2</sub> = x<sub>1</sub>)'' |
* B-T-B | * B-T-B | ||
- | :: ∀ | + | :: ∀ x<sub>1</sub> ∀ x<sub>2</sub> ∀ y<sub>1</sub> ∀ y<sub>2</sub> [φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) ∧ (y<sub>2</sub> >= 0) ∧ (y<sub>2</sub> >= x<sub>2</sub>) => φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*(y<sub>1</sub>+1) + (y<sub>2</sub>-x<sub>2</sub>)) ∧ ((y<sub>2</sub>-x<sub>2</sub>) >= 0)] |
* B-F-H | * B-F-H | ||
- | :: ∀ | + | :: ∀ x<sub>1</sub> ∀ x<sub>2</sub> ∀ y<sub>1</sub> ∀ y<sub>2</sub> [φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) ∧ (y<sub>2</sub> >= 0) ∧ (y<sub>2</sub> < x<sub>2</sub>) => (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) ∧ (y<sub>1</sub> < x<sub>2</sub>)] |
- | 2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция | + | 2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y<sub>2</sub>. |
- | Условие корректности: ∀ | + | Условие корректности: ∀ x<sub>1</sub> ∀ x<sub>2</sub> ∀ y<sub>1</sub> ∀ y<sub>2</sub> [φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) ∧ (y<sub>2</sub> >= 0) => y<sub>2</sub> <math>\isin</math> Nat] |
- | Условие завершимости: ∀ | + | Условие завершимости: ∀ x<sub>1</sub> ∀ x<sub>2</sub> ∀ y<sub>1</sub> ∀ y<sub>2</sub> [φ(x<sub>1</sub>, x<sub>2</sub>) ∧ (x<sub>1</sub> = x<sub>2</sub>*y<sub>1</sub> + y<sub>2</sub>) ∧ (y<sub>2</sub> >= 0) ∧ (y<sub>2</sub> >= x<sub>2</sub>) => (y<sub>2</sub> > y<sub>2</sub>-x<sub>2</sub>) ] |
=== Комментарии === | === Комментарии === | ||
Строка 68: | Строка 68: | ||
==Задача 6 (PVS)== | ==Задача 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 Nat]
Условие завершимости: ∀ x1 ∀ x2 ∀ y1 ∀ y2 [φ(x1, x2) ∧ (x1 = x2*y1 + y2) ∧ (y2 >= 0) ∧ (y2 >= x2) => (y2 > y2-x2) ]
[править] Комментарии
- Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 2 обязательно должны быть явно выписаны условия корректности и завершимости.
- Не забывать ставить ВСЕ условия прохождений по веткам.
- Помните, что подставлять изменённые значения, необходимо не только в правой части а везде, где они меняются (к примеру, если путь проходит через 2 условия, то второе к оменту вхождение может иметь уже изменённую переменную).
[править] Задача 6 (PVS)
ГЛАВНОЕ! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.