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

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

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 1: Строка 1:
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
Как показала практика, на коллоквиумах (и, вероятно, в какой-то степени на экзамене) придираются к оформлению задач. Здесь будут примеры, которые содержат необходимые формальности. Обращаю внимание, что это не мануал по решению и ботать но нему не стоит, это просто пример оформления.
-
== Задача 1 (EI)==
+
== Задача 5, метод Флойда==
-
Первая задача: по явному описанию функции построить неявное, т.е. переписать первоую часть и добавить пост и пред-условия.
+
-
 
+
-
'''Условие''':
+
-
'''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>
Строка 41: Строка 15:
(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 &and; x2 > 0
+
Предусловие: &phi;(x1, x2): x1 >= 0 /\ x2 > 0
-
Постусловие: &psi;(x1, x2, z1, z2): x1 = x2*z1 + z2 &and; z1 < x2
+
Постусловие: &psi;(x1, x2, z1, z2): x1 = x2*z1 + z2 /\ z1 < x2
=== Решение ===
=== Решение ===
-
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) '' // в условии не задан, придумываем сами''
+
1. Инвариант в B: P(x1, x2, y1, y2) is &phi;(x1, x2) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) '' // в условии не задан, придумываем сами''
Имеем 3 пути:
Имеем 3 пути:
* S-B
* S-B
-
:: &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>)''
+
:: &forall; x1 &forall; x2 [(x1 >= 0) /\ (x2 > 0) => &phi;(x1, x2) /\ (x1 = x2*0 + x1) /\ (x1 >= 0)] ''// здесь нужно сразу подставить начальные значения из START, а не писать /\ (y1 = 0) /\ (y2 = x1)''
* B-T-B
* B-T-B
-
:: &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)]
+
:: &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)]
* B-F-H
* B-F-H
-
:: &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>)]
+
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 < x2) => (x1 = x2*y1 + y2) /\ (y1 < x2)]
-
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y<sub>2</sub>.
+
2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2.
-
Условие корректности: &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 <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) &and; (y<sub>2</sub> >= x<sub>2</sub>) => (y<sub>2</sub> > y<sub>2</sub>-x<sub>2</sub>) ]
+
Условие завершимости: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) /\ (x1 = x2*y1 + y2) /\ (y2 >= 0) /\ (y2 >= x2) => (y2 > y2-x2) ]
=== Комментарии ===
=== Комментарии ===
-
* Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 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|Ещё пример от Алексея Хорошилова]]
+
-
 
+
-
{{Курс МФСП}}
+

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Шаблоны, использованные на этой странице:

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