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

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

Версия от 13:09, 29 января 2010; 217.118.85.90 (Обсуждение)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

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

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

== Задача 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/status/7015914018 kornevgen], дерево рисовать не обязательно:<blockquote>"@dimanium например,все рисуют в 1й задаче дерево,как будто без него не примут задачку!нам же не нужны обезьянки,нам нужны люди!"</blockquote>

== Задача 5, метод Флойда==
===Условие===
<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 обязательно должны быть явно выписаны условия корректности и завершимости.

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

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

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

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