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

Материал из 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)==
'''ГЛАВНОЕ'''! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.
{{Курс МФСП}}

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. 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 семестр

Поиск

Инструменты

@@ Строка 68: / Строка 68: @@
 ==Задача 6 (PVS)==
 '''ГЛАВНОЕ'''! Убедитесь, что вы доказываете именно теорему, а не лемму или другое какое нибудь дополнительное условие.
-* [[МФСП, 12 лекция (от 26 ноября)|Пример, разбиравшийся на лекции]]
-* [[http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/Tutorial.doc|Ещё пример от Алексея Хорошилова]]
 {{Курс МФСП}}