Редактирование: МФСП, 09 лекция (от 29 октября)

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

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

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

* '''Диктофонная запись:''' http://esyr.org/lections/audio/mfsp_2008_winter/MFSP_08_10_29.ogg

Консультация

В каждом билете должно быть 4 задачи. Теор материала никакого нет.

# Либо перевод явной спецификации в неявную. Спецификации должны быть абсолютно эквивалентны. Любые неточности будут трактоваться как ошибки. Могут быть погрешности практ. плана, это не беда. Если же искажена семантика, то это ошибка. Иногда включается обрб. трансляция, но это случай редкий. Тут рассм. одна функция.
# Дайтся алг. спецификация, и по ней необх. дать явную, неявную спец. группы функций, чтобы в низ были опр. предлусловия, и все спец. долны отв. требованиям аксиом, сформ. в задаче. Тут группа функций рассматривается. Для каких-то функций можно исп. явную, для каких-то — неянвую спецификацию, на выбор.
# Даётся алг. спецификация, плюс даётся явная спецификация. Надо доказать, что явная спец. явл. или не является уточнением алгебраической.
# Упрощение некоего выражения. В качестве выр. даётся фрагмент спецификации, в котором активно исп. параллельность, внутр/внешний выбор, взаимная блоеировка, и так далее.

== Конкретные примеры ==

=== 1. (Билет 1 задание 1 из методички 2008) ===
 f: Int &times; Int &times; Int &rarr; '''write''' x '''read''' y Int &times; Int
   f(a,b,c) &equiv;; '''if''' a=b '''then'''
                      ('''if''' a+b > c '''then''' c '''else''' a+b '''end''',
                      a*b*('''if''' c>0 '''then''' x:=y; c '''else''' 0-c '''end'''))
                    '''else''' (a+b, x:=b; a-b)
   '''end'''

Подводные камни:
* Никогда нет присваивания.
* В случае неизм. перем. на запись в постусловии надо написать, что знач. переменной сохр.: x=x'
* Выражение должно быть корректно

Ответ:
 f: Int &times; Int &times; Int &rarr; '''write''' x '''read''' y Int &times; Int
 f(a,b,c) '''as''' (d, e)
   '''post'''
     '''if''' a=b '''then'''
       '''if''' a+b>c '''then'''
         '''if''' c>0 '''then'''
           d=c &and; x=y &and; e = a*b*c
         '''else'''
           d=c &and; x=x’ &and; e=a*b*(0-c) 
         '''end'''
       '''elseif''' c>0 '''then''' 
         d=a+b &and; x=y &and; e= a*b*c
       '''else''' 
         d=a+b &and; x=x‘ &and; e=a*b*(0-c) 
       '''end'''
     '''else''' 
       d=a+b &and; x=b &and; e=a-b 
     '''end'''

Для каждой комб. входных данных выпис. результат в том или ином случае. Результат состоит из d, e и x.

Где подобная задача может встретиться: в переписывании legacy, как альтернатива реверс-инжинирингу.

Перевод из неявной спец. в явную это обычное программирование.

=== 2. (Билет 1, задание 2) ===
 '''type''' 
   S, E

'''value'''
   create : Unit &rarr; S,
   add : E &times; S &rarr; S,		
   del : S -~-> S,			
   next : S  -~-> S, 		
   get : S -~-> E,
   append : S &times; S &rarr; S

'''axiom'''
   &forall; e : E, s : S :- del(add(e, s)) &equiv; s,
   &forall; e : E, s : S :- get(add(e, s)) &equiv; e,
   &forall; e : E, s : S :- next(add(e, s)) &equiv; 	
     if s = create() then 
       add( e, s )
     else 
       append ( s, add( e, create( ) )
     end,

&forall; e : E, s1, s2 : S :- append(create(), s2)) &equiv; s2,
   &forall; e : E, s1, s2 : S :- append(add(e, s1), s2)) &equiv; add(e, append (s1, s2))

Всегда на входе будет группа функций, работающая с общей структурой данных. При этом, видимо, E — элемент, S — структура. При этом внутр. предст. элемента не важно, а вот что за S, хорошо быд догадаться. Какие бывают виды структур: множество, список, отображение. Элементами его могут быть или сами элементы E, множества, списки, отображения. Помимо совсем простых, базовых структур, может быть более хитрая структура, например, круговой список. Структура может быть необяз. одноур. Т. о.с совет: сначала понять, какая стуктура данных скр. за спецификацией, и после этого писать спецификацию.

Ответ: видимо, S это кользевой список.
 '''type'''
   E,
   S : '''E-l&equiv;t'''
 
 '''value'''
   create : Unit &rarr; S
     create &equiv; <..>,
 
   add : E &times; S &rarr; S 
     add (e,s) &equiv; <.e.> ^ s,
 
   del : S -~-> S 
     del (s) &equiv; tl s
     '''pre''' s &ne; <..>,
 
   next : S  -~-> S 
     next (s) &equiv; tl s ^ <. hd s  .>
     '''pre''' s &ne; <..>, /* Надо писать предусловие */
 
   get : S -~-> E 
     get (s) &equiv; hd s
     '''pre''' s &ne; <..>,
 
   append : S &times; S &rarr; S
     append (s1, s2) as s
     post
       if s1=<..> then s=s2
       else s=add(hd s1, append( tl s1, s2))
       end

=== 3. Доказательства ===

Самое длинное решение.

Какие правила:
* Вычислять всё, что можно вычислить
* Подстановка. Всегда в кач. условия даётся явное опр. Везде, где в алг. спец. вы видите обр. к функции, в жтом месте всегда можно сделать подстановку
* Базовые операции с осн. структурами данных в сдлучае изв. значений.

Для каждой из аксиом проводятсчя преобр. для правой и левой части, пока либо они нне станут текстуально равны, либо пока они не станут явно неэквив.

Может в условии задач сегка ошибиться и можно увидеть по сигн., что они не явл. уточнением. Если такая ошибка найдётся, то ваше счастье.

Если запись будет не слишком подробной, то это нормально

=== 4. Задачи на упрощение ===

Какие бывают типы:
* ||, П
* ||, ++
* ||, []
Более хитрых комбинаций быть не должно.

(b!2) || (y := a?) || '''if''' (x:=1); (a!x); ('''true''' П '''false''') '''then''' a!(b?) '''else''' a!(1+b?) '''end'''

Финальная запись решения, это, как правило, набор выражений, раз. внутр. выбором, каждон из них дост. простое.

Для начала просканировать и найти контрагентов.
* Первый тред пишет b? второй читает
* Второй тред взаимод. с оператором (a!x) из третьего треда

a!(5+b?) || ((x:=('''if''' '''true''' П '''false''' '''then''' x:=b?;1 '''else''' b!3; x:=2; 6 '''end''') +x) ++ (b!4|| y:=b?))

По поводу: (x:=a?)||(x:=b?). Мы ничего не можем сказать без окружения. Если это изолир. оператор и ничего в каналах нет, то это беск. одидание. Если порядок получения данных из каналов известен, то мы можем сказать что-то определённое, если же порядок неизв, то и сказать ничего не можем.

Может ли провзаим. 5+b? и b!3 ? Только если после взаимод в интерлоке это взаимод. не использ. и оно будет выполн., то да.

# Рассм. первые два случая: a!(5+b?) || ((x:=((x:=b?;1)П(b!3;x:=2;6))+x)||(y:=4)). Поск. все взаимод. произошли, то ++ заменяется на ||.
## a!(5+b?) || ((x:=(x:=b?;1)+x)||(y:=4)) — первое решение

Больше выпис. не будем.

Варивант со внеш. взаимодействием: почти наверняка это будет case:
 case (1 П b?) '''of'''
   1:
   3:
   5:
 '''end''' || a! ... || b!(a?+2) || ...

Результатом будет ветка кейса и те взаимод., которые не заверш..

Орг. замечания:
* Можно польз. молча любыми ист. информации
* Нельзя обмениваться информацией ни в каком виде

Результ. окзенка за предмет будет сост. из двух коллоквиум и возм. оценка по успехам за практ. задание.

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

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

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

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

Получено с http://esyr.us/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_09_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_29_%D0%BE%D0%BA%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29

Редактирование: МФСП, 09 лекция (от 29 октября)

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

Просмотры

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

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 3: / Строка 3: @@
 Консультация
-В каждом билете должно быть 4 задачи. Теоретического материала никакого нет.
+В каждом билете должно быть 4 задачи. Теор материала никакого нет.
-# Либо перевод явной спецификации в неявную. Спецификации должны быть абсолютно эквивалентны. Любые неточности будут трактоваться как ошибки. Могут быть погрешности практического плана, это не беда. Если же искажена семантика, то это ошибка. Иногда включается обрб. трансляция, но это случай редкий. Тут рассматривается одна функция.
+# Либо перевод явной спецификации в неявную. Спецификации должны быть абсолютно эквивалентны. Любые неточности будут трактоваться как ошибки. Могут быть погрешности практ. плана, это не беда. Если же искажена семантика, то это ошибка. Иногда включается обрб. трансляция, но это случай редкий. Тут рассм. одна функция.
-# Даётся алгебраическая спецификация, и по ней необходимо дать явную, неявную спецификацию группы функций, чтобы в них были определены предусловия, и все спецификации должны отвечать требованиям аксиом, сформулированным в задаче. Тут группа функций рассматривается. Для каких-то функций можно использовать явную, для каких-то — неявную спецификацию, на выбор.
+# Дайтся алг. спецификация, и по ней необх. дать явную, неявную спец. группы функций, чтобы в низ были опр. предлусловия, и все спец. долны отв. требованиям аксиом, сформ. в задаче. Тут группа функций рассматривается. Для каких-то функций можно исп. явную, для каких-то — неянвую спецификацию, на выбор.
-# Даётся алгебраическая спецификация, плюс даётся явная спецификация. Надо доказать, что явная спец. явл. или не является уточнением алгебраической.
+# Даётся алг. спецификация, плюс даётся явная спецификация. Надо доказать, что явная спец. явл. или не является уточнением алгебраической.
-# Упрощение некоего выражения. В качестве выражения даётся фрагмент спецификации, в котором активно используется параллельность, внутренний/внешний выбор, взаимная блокировка, и так далее.
+# Упрощение некоего выражения. В качестве выр. даётся фрагмент спецификации, в котором активно исп. параллельность, внутр/внешний выбор, взаимная блоеировка, и так далее.
 == Конкретные примеры ==
@@ Строка 22: / Строка 22: @@
 Подводные камни:
 * Никогда нет присваивания.
-* В случае неизменённых переменных на запись в постусловии надо написать, что значение переменной сохраняется: x=x'
+* В случае неизм. перем. на запись в постусловии надо написать, что знач. переменной сохр.: x=x'
 * Выражение должно быть корректно
@@ Строка 45: / Строка 45: @@
      '''end'''
-Для каждой комбинации входных данных выписывается результат в том или ином случае. Результат состоит из d, e и x.
+Для каждой комб. входных данных выпис. результат в том или ином случае. Результат состоит из d, e и x.
 Где подобная задача может встретиться: в переписывании legacy, как альтернатива реверс-инжинирингу.
-Перевод из неявной спецификации в явную это обычное программирование.
+Перевод из неявной спец. в явную это обычное программирование.
 === 2. (Билет 1, задание 2) ===
@@ Строка 76: / Строка 76: @@
    &forall; e : E, s1, s2 : S :- append(add(e, s1), s2)) &equiv; add(e, append (s1, s2))
-Всегда на входе будет группа функций, работающая с общей структурой данных. При этом, видимо, E — элемент, S — структура. При этом внутреннее представление элемента не важно, а вот что за S, хорошо бы догадаться. Какие бывают виды структур: множество, список, отображение. Элементами его могут быть или сами элементы E, множества, списки, отображения. Помимо совсем простых, базовых структур, может быть более хитрая структура, например, круговой список. Структура может быть необязательно одноуровневой Т. о.с совет: сначала понять, какая структура данных скрыта за спецификацией, и после этого писать спецификацию.
+Всегда на входе будет группа функций, работающая с общей структурой данных. При этом, видимо, E — элемент, S — структура. При этом внутр. предст. элемента не важно, а вот что за S, хорошо быд догадаться. Какие бывают виды структур: множество, список, отображение. Элементами его могут быть или сами элементы E, множества, списки, отображения. Помимо совсем простых, базовых структур, может быть более хитрая структура, например, круговой список. Структура может быть необяз. одноур. Т. о.с совет: сначала понять, какая стуктура данных скр. за спецификацией, и после этого писать спецификацию.
-Ответ: видимо, S это кольцевой список.
+Ответ: видимо, S это кользевой список.
  '''type'''
    E,
@@ Строка 115: / Строка 115: @@
 Какие правила:
 * Вычислять всё, что можно вычислить
-* Подстановка. Всегда в качестве условия даётся явное определение. Везде, где в алгебраической спецификации вы видите обращение к функции, в этом месте всегда можно сделать подстановку
+* Подстановка. Всегда в кач. условия даётся явное опр. Везде, где в алг. спец. вы видите обр. к функции, в жтом месте всегда можно сделать подстановку
-* Базовые операции с основными структурами данных в случае известных значений.
+* Базовые операции с осн. структурами данных в сдлучае изв. значений.
-Для каждой из аксиом проводятся преобр. для правой и левой части, пока либо они нне станут текстуально равны, либо пока они не станут явно неэквив.
+Для каждой из аксиом проводятсчя преобр. для правой и левой части, пока либо они нне станут текстуально равны, либо пока они не станут явно неэквив.
-Может в условии задач слегка ошибиться и можно увидеть по сигнатуре, что они не являются уточнением. Если такая ошибка найдётся, то ваше счастье.
+Может в условии задач сегка ошибиться и можно увидеть по сигн., что они не явл. уточнением. Если такая ошибка найдётся, то ваше счастье.
 Если запись будет не слишком подробной, то это нормально
@@ Строка 134: / Строка 134: @@
  (b!2) || (y := a?) || '''if''' (x:=1); (a!x); ('''true''' П '''false''') '''then''' a!(b?) '''else''' a!(1+b?) '''end'''
-Финальная запись решения, это, как правило, набор выражений, различающихся внутренним выбором, каждое из них достаточно простое.
+Финальная запись решения, это, как правило, набор выражений, раз. внутр. выбором, каждон из них дост. простое.
 Для начала просканировать и найти контрагентов.
 * Первый тред пишет b? второй читает
-* Второй тред взаимодействует с оператором (a!x) из третьего треда
+* Второй тред взаимод. с оператором (a!x) из третьего треда
  a!(5+b?) || ((x:=('''if''' '''true''' П '''false''' '''then''' x:=b?;1 '''else''' b!3; x:=2; 6 '''end''') +x) ++ (b!4|| y:=b?))
-По поводу: (x:=a?)||(x:=b?). Мы ничего не можем сказать без окружения. Если это изолированный оператор и ничего в каналах нет, то это бесконечное ожидание. Если порядок получения данных из каналов известен, то мы можем сказать что-то определённое, если же порядок неизвестен, то и сказать ничего не можем.
+По поводу: (x:=a?)||(x:=b?). Мы ничего не можем сказать без окружения. Если это изолир. оператор и ничего в каналах нет, то это беск. одидание. Если порядок получения данных из каналов известен, то мы можем сказать что-то определённое, если же порядок неизв, то и сказать ничего не можем.
-Может ли провзаимодействовать 5+b? и b!3 ? Только если после взаимодействия в интерлоке это взаимодействие не используется и оно будет выполнено, то да.
+Может ли провзаим. 5+b? и b!3 ? Только если после взаимод в интерлоке это взаимод. не использ. и оно будет выполн., то да.
-# Рассмотрим первые два случая: a!(5+b?) || ((x:=((x:=b?;1)П(b!3;x:=2;6))+x)||(y:=4)). Поскольку все взаимодействия произошли, то ++ заменяется на ||.
+# Рассм. первые два случая: a!(5+b?) || ((x:=((x:=b?;1)П(b!3;x:=2;6))+x)||(y:=4)). Поск. все взаимод. произошли, то ++ заменяется на ||.
 ## a!(5+b?) || ((x:=(x:=b?;1)+x)||(y:=4)) — первое решение
-Больше выписывать не будем.
+Больше выпис. не будем.
-Варивант со внешним взаимодействием: почти наверняка это будет case:
+Варивант со внеш. взаимодействием: почти наверняка это будет case:
  case (1 П b?) '''of'''
 :
@@ Строка 158: / Строка 158: @@
  '''end''' || a! ... || b!(a?+2) || ...
-Результатом будет ветка кейса и те взаимодействия, которые не заверш..
+Результатом будет ветка кейса и те взаимод., которые не заверш..
-Организационные замечания:
+Орг. замечания:
-* Можно пользоваться молча любыми источниками информации
+* Можно польз. молча любыми ист. информации
 * Нельзя обмениваться информацией ни в каком виде
-Результирующая оценка за предмет будет состоять из двух коллоквиумов и, возможно, оценки по успехам за практическое задание.
+Результ. окзенка за предмет будет сост. из двух коллоквиум и возм. оценка по успехам за практ. задание.
 {{МФСП}}
 {{Lection-stub}}