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

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

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

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

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

== Задача 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>
                START
          (y1, y2) = (0, x1)
                  |
   -------------->|
   |              B 
   |              |     F
   |           y2 >= x2-------
   |              |T         |
   |              |          |
(y1, y2) = (y1+1, y2-x2)     HALT: (z1, z2) = (y1, y2)
</pre>
Предусловие: &phi;(x1, x2): x1 >= 0 &and; x2 > 0
Постусловие: &psi;(x1, x2, z1, z2): x1 = x2*z1 + z2 &and; z1 < x2

=== Решение ===
1. Инвариант в B: P(x1, x2, y1, y2) is &phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) '' // в условии не задан, придумываем сами''

Имеем 3 пути:
* S-B
:: &forall; x1 &forall; x2 [(x1 >= 0) &and; (x2 > 0)   =>   &phi;(x1, x2) &and; (x1 = x2*0 + x1) &and; (x1 >= 0)]   ''// здесь нужно сразу подставить начальные значения из START, а не писать &and; (y1 = 0) &and; (y2 = x1)''
* B-T-B
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2)   =>   &phi;(x1, x2) &and; (x1 = x2*(y1+1) + (y2-x2)) &and; ((y2-x2) >= 0)]
* B-F-H
:: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 < x2)   =>    (x1 = x2*y1 + y2) &and; (y1 < x2)]

2. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y2.

Условие корректности: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0)   =>   y2 <math>\isin</math> Nat]

Условие завершимости: &forall; x1 &forall; x2 &forall; y1 &forall; y2 [&phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2)   =>   (y2 > y2-x2) ]

=== Комментарии ===
* Доказательства тождеств приводить не надо (хотя их рекомендуется сделать для уверенности в правильности). В пункте 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:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

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

Шаблон:Курс МФСП

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F:_%D0%9E%D1%84%D0%BE%D1%80%D0%BC%D0%BB%D0%B5%D0%BD%D0%B8%D0%B5_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87

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

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 45: / Строка 45: @@
 === Решение ===
-. Инвариант в 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) '' // в условии не задан, придумываем сами''
+. Инвариант в B: P(x1, x2, y1, y2) is &phi;(x1, x2) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) '' // в условии не задан, придумываем сами''
 Имеем 3 пути:
 * 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) &and; (x2 > 0)   =>   &phi;(x1, x2) &and; (x1 = x2*0 + x1) &and; (x1 >= 0)]   ''// здесь нужно сразу подставить начальные значения из START, а не писать &and; (y1 = 0) &and; (y2 = x1)''
 * 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) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2)   =>   &phi;(x1, x2) &and; (x1 = x2*(y1+1) + (y2-x2)) &and; ((y2-x2) >= 0)]
 * 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) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 < x2)   =>    (x1 = x2*y1 + y2) &and; (y1 < x2)]
-. Фундированное множество - (Nat, >), точка сечения B. Оценочная функция y<sub>2</sub>.
+. Фундированное множество - (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) &and; (x1 = x2*y1 + y2) &and; (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) &and; (x1 = x2*y1 + y2) &and; (y2 >= 0) &and; (y2 >= x2)   =>   (y2 > y2-x2) ]
 === Комментарии ===