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

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

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

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

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

Текущая версия Ваш текст
Строка 12: Строка 12:
Недетерминированная функция — функция, которая при одном и том же значении возвращает различные результаты.
Недетерминированная функция — функция, которая при одном и том же значении возвращает различные результаты.
 +
 +
Лектор просит записать определения 4 понятий:
 +
# Неполная спецификация констант
 +
# Неполная спецификация функции
 +
# Недетерминированная спецификация констант
 +
# Недетерминированная спецификация функции
# Неполная спецификация констант — когда недостаточно информации для получения значения константы
# Неполная спецификация констант — когда недостаточно информации для получения значения константы
Строка 20: Строка 26:
В RSL нет возможности представить недетерминизм констант, и там такого понятия нет.
В RSL нет возможности представить недетерминизм констант, и там такого понятия нет.
-
Для функций же недетерминизм возможен, это происходит тогда, кгда при дном наборе параметров возвращаются разные значения.
+
Для функций же недетерм. взмжен, это происх. тогда, кгда при дном наборе параметров возвр. разные значения.
И ситуация, когда мы не написали ничего, кроме сигнатуры — типичный пример неполной спецификации. Или же мы написали только постусловие или аксиому, неполное описание поведение функции. Например:
И ситуация, когда мы не написали ничего, кроме сигнатуры — типичный пример неполной спецификации. Или же мы написали только постусловие или аксиому, неполное описание поведение функции. Например:
Строка 29: Строка 35:
'''post''' (y=) ∨ (y=x-1) ∨ (y=x+1)
'''post''' (y=) ∨ (y=x-1) ∨ (y=x+1)
-
Насколько мы могли знать из семинаров, бывают полностью пр. и неполно определённые функции. Неполно определённые обозначаются в ASCII-нотации как ~→. При исп. → известно, что функция является детерминированной и тотальной. При использовании ~→ функция может быть нетот. и недетерминированной.
+
Насколько мы могли знать из семинаров, бывают полностью пр. и неполно определённые функции. Неп. опр. обозначаются в ASCII-нотации как ~→. При исп. → известно, что функция является детерминированной и тотальной. При использовании ~→ функция может быть нетот. и недетерминированной.
Если же функция может детерминированно менять значение, то мы сможем описать некое условие на некое дополнительное множество, которое введём специально. И можно ввести дополнительные условия, чтобы но удовлетворяющие некоему распределению с произвольной точностью. обычно это актуально при введении функции генерации сл. значений.
Если же функция может детерминированно менять значение, то мы сможем описать некое условие на некое дополнительное множество, которое введём специально. И можно ввести дополнительные условия, чтобы но удовлетворяющие некоему распределению с произвольной точностью. обычно это актуально при введении функции генерации сл. значений.
Строка 35: Строка 41:
При неполной спецификации мы можем допустить некоторую вольность в реализации. Недетерминированная спецификация может возвращать различные значения, будучи вызванной в одной и той же ситуации.
При неполной спецификации мы можем допустить некоторую вольность в реализации. Недетерминированная спецификация может возвращать различные значения, будучи вызванной в одной и той же ситуации.
-
Примеры использования понятий неполной спецификации:
+
Лектор просит написать рядом с каждым определением небольшой пример, когда это может встретиться. В каких ситуациях соответствующее понятие может быть использовано.
1.
1.
Строка 49: Строка 55:
'''post''' (y > 0)
'''post''' (y > 0)
-
Единственное отличие — какой синтаксис использовать — написать аксиому, или ещё что. Второй вариант — константный предметной области, диапазон, список (коды ошибок).
+
Единственное отличие — какой синтаксис исп. — написать аксиому, или ещё что. Второй вариант — константный предметной области, диапазон, список (коды ошибок).
-
В RSL нет понятия времени, но мы можем его ввести дополнительно, например, в качестве глобальной переменной Синтаксические способы могут быть придуманы, но непосредственно в языке этого не предусмотрено. Временное расширение RSL есть, но в курсе не рассматривается.
+
В RSL нет понятия времени, но мы можем его ввести дополнительно, например, в качестве глобальной переменной Синтаксические способы могут быть придуманы, но непосредственно в языке этого не предусмотрено. Временное расширение RSL есть, но лектор его не рассматривает.
-
Что касается вопроса относительно спецификации алгоритма, то в RSL, когда мы описываем спецификацию, мы описываем её значимое и побочное действие. Ограничения на внутреннюю реализацию на RSL никак описаны быть не могут, кроме как придумывая синтетический способ.
+
Что кас. вопр. отн. специф. алгоритма, то в RSL, когда мы опис. спец., мы опис. её знач. и побоч. действие. Огр. на внутр. реализацию на RSL никак описаны быть не могут, кроме как придумывая синтетич. способ.
В то же время спецификация может относиться не только к результату, но и к тому, как она бн. переменную. Этт аспект может быть недоспецифицирован.
В то же время спецификация может относиться не только к результату, но и к тому, как она бн. переменную. Этт аспект может быть недоспецифицирован.
Строка 66: Строка 72:
Как мы выяснили, понятие детерминизма-недетерминизма реализации рассматривается тн. модели, а не по своим внутренним зар-кам.
Как мы выяснили, понятие детерминизма-недетерминизма реализации рассматривается тн. модели, а не по своим внутренним зар-кам.
-
Какие ещё пример: мель детали, системы недетерминированы. Это достаточно реальный пример, может встретиться, когда спецификация неполна. Например, если в спецификации результирующего типа Bool, а в реализации — Int, и в качестве True возвращается значение, отл. от 0. При этом это некий мухлёж, это недетерминизм уже внутри реализации.
+
Какие ещё пример: мель детали, системы недетерминированы. Это дост. реальный пример, мжет встр., когда специф. неполна. Нпр., если в спец. рез. типа Bool, а в реализации — Int, и в качестве True выозвр. зн., отл. от 0. При этом это некий мухлёж, это недетерминизм уже внутри реализации.
<!-- перерыв -->
<!-- перерыв -->
Строка 80: Строка 86:
add(e1, add(e2, s)) is add(e2, add(e1, s))
add(e1, add(e2, s)) is add(e2, add(e1, s))
-
Каким образом может появиться недетерминизм? Можно легко написать такую реализацию:
+
Единственное, что хотел лектр показать — каким бр. может появиться недетерм. Можно легк напис. такую реализацию:
case s of
case s of
Строка 86: Строка 92:
end
end
-
В RSL можно писать по таким определениям case, когда мы выбираем по некоторому множеству, мы пишем некоторый паттерн по операции из вариант. пр. этого типа с двумя параметрами, и подразумеваем, что это может быть любое ..., сзд. множеств, а поскольку есть аксиома неуп., то в качестве x и y подбирается заранее неизвестно какая пара, поэтому это выражение будет недетерминировано. Можно написать ещё кое-что в нед.:
+
В RSL мжно писать по таким опр. case, когда мы виб. по некоторому мнжеству, мы пишем некоторый паттерн по операции из вариант. пр. этого типа с двумя параметрами, и подразумеваем, чт это может быт ь любое ..., сзд. множеств, а поск. есть аксиома неуп., то в качестве x и y подб. заранее неизв. какая пара, поэтому это выр. будет недетерм. Мжно напис. ещё кое-что в нед.:
let x : Int in x end
let x : Int in x end
-
Крме выражения для получения недетерминированной спецификации, есть ещё одно, мы с ним познакомимся, когда будем рассматривать спецификации параллельных программ на RSL.
+
Крме выр. для получ. нед. спец, есть ещё дно, мы с ним пзн., когда будем рассм. спец. пар. прграмм на RSL.
-
В языке RSL есть такое понятие как канал. Они имеют синтаксис такой же, как и у переменных, только вместо value пишется channel, для них не определено присваивание, но есть тип:
+
В языке RSL есть таке понятие как канал. Они имеют синт такй же, как и у перем, тлько вместо value пишется channel, для них не опр. присв, но есть тип:
-
'''channel'''
+
'''channe'''
c1:int, c2 : Char
c1:int, c2 : Char
-
Если у каналов разные идентификаторы, то они разные и равными оказаться не могут.
+
Если у каналов разные идент, то они разные и равными оказ. не могут.
-
При определении функции в её сигнатуре должны обязательно присутствовать каналы, к которым она обращается.
+
При опр. функции в её сигнатуре должни обяз. присутствовать каналы, к кторым на обр.
'''value'''
'''value'''
Строка 106: Строка 112:
при этом функция читает из c1 и пишет в c2 в данном случае.
при этом функция читает из c1 и пишет в c2 в данном случае.
-
Внутри тела для обращения к каналам у нас могут использоваться следующие выражения:
+
Внутри тела для бр. к каналам у нас могу исп. следующие выр.:
'''value''' f(x) is
'''value''' f(x) is
Строка 112: Строка 118:
с2!expr № Запись в канал. Тип выр. должен совп. с типом канала.
с2!expr № Запись в канал. Тип выр. должен совп. с типом канала.
-
RSL предусматривает не только аксиоматическую и имплицитную спецификацию, но и эксплицитные спецификации. Здесь аналогично мы расп. некую стр. целевой системы в явном виде с пр. каналов и их взаимодействия с их исп., и это такой вид спецификации, не являющийся замещающим, или продолжением тех, что мы рассматривали ранее, это некий дополнительный способ, предусмотренный языком. Его можно для некоторых доп. целей использовать.
+
RSL предусм. не тлько аксим. и импл. специф, но и эксплицитные спецификации. Здесь аналгично мы расп. некую стр. целевй сист. в явном виде с пр. каналов и их взаимод. с их исп., и это такой вид спейификации. н не явл. замещающим, или продолжением тех, что мы рассм. ранее, эт некий доп. способ, предусм. языком. Его можно для некоторых доп. целей испльзовать.
-
Функции, которые работают с каналами называются процессами. Посмотрим, какие есть возможности для композиции процессов.
+
Функции, которые работают с каналами наз. прцессами. Посмотрим, какие есть возм. для компзиции процессов.
-
Первый, простой способ — параллельная композиция: f1 || f2. Это означает, что они работают параллельно и могут взаимодействовать по общему каналу. А могут и не взаимодействовать.
+
Первый, прост. способ — парал. компзиция: f1 || f2. Это озн., что они работают параллельно и могут взаимд. по общему каналу. А мгут и не взаимодействовать.
c!5 || x := c?
c!5 || x := c?
-
Это может произойти, а может и нет. Это не эквивалентно присваиванию 5 в x.
+
Это может произойти, а мжет и нет. Это не экв. присваиванию 5 в x.
с!& || (x :=c? || c!5)
с!& || (x :=c? || c!5)
-
может быть эквивалентно:
+
мжет быть экв:
x:=5; c!7
x:=5; c!7
x:=7; c!5
x:=7; c!5
-
или как-то иначе.
+
или как-т иначе.
-
Второй вариант композиции: внешний выбор. |=| Он говорит то, что как поведёт себя система, зависит от внешнего окружения.
+
Второй вариант компзиции: внешний выбор. |=| Он говорит то, что как поведёт себя система, зависит от внешнего окружения.
x := c? |=| d!5
x := c? |=| d!5
-
То, как поведёт себя система, зависит от внешнего окруженияя
+
То, как пведёт себя сист., зависит от внеш. окр.
(x := c? |=| d!5) || c!1
(x := c? |=| d!5) || c!1
Это будет экв.
Это будет экв.
x:=1
x:=1
-
|^| — внутренний выбор. Это говорит, что выбор происходит не от окр., а по внутренним сображениям процесса.
+
|^| — внутренний выбор. Это говорит, что выбр происх. не от окр., а по внутр. собр. процесса.
(x := c? |^| d!5) || c!1
(x := c? |^| d!5) || c!1
Результат в этом случае вполне мог быть либо
Результат в этом случае вполне мог быть либо
Строка 140: Строка 146:
либо
либо
(d!5||c!1)
(d!5||c!1)
-
Это отличие внутреннего выбора от внешнего.
+
Это отличие внутр. выбра от внешнего.
-
Отличие выборов от композиции в том, что в случае выбора выражения, между которыми происходит выбор, взаимодействовать не могут.
+
От личие выборов от комп. в том, что в случае выбора выр., между которыми присх. выбор, взаимод. не мгут.
-
4 вариант композиции — взаимная блокировка, обозначается ++. Все взаимодействующие должны пройти между выр., композирующих с помощью взаимной блокировки.
+
4 вариант композиции — взаимная блокировка, обозн. ++. Все взаимод. должны пройти между выр., композирующих с помощью взаимной блокирвки.
(x:=c?++c!e) == (x:=e)
(x:=c?++c!e) == (x:=e)
-
Если для параллельной композиции взаимодействие необязательно, то в случае блокировки взаимодействие обязательно.
+
Если для пар. комп. взаимод. небяз, то в случае блкировки взаимод. обязательно.
(x:=c?||c!e) == (x:=e) |^| ((x:=c?; c!e) |=| (c!e; x:=c?) |=| (x:=e))
(x:=c?||c!e) == (x:=e) |^| ((x:=c?; c!e) |=| (c!e; x:=c?) |=| (x:=e))
-
Все взаимодействия происходят синхронно.
+
Все взаимод. происх. синхронно.
-
Тема работы с параллельными процессами в RSL не очень простая, но на экзамене задача по упрощению выражений подобных будет и на коллоквиуме она тоже появится. И это надо учитывать.
+
Тема работы с пар. прцессами в RSL не чень простая, но на экз. задача по упр. выр. подбных будет и на кллоквиуме она тоже появится. И это надо учитывать.
-
Пример на interlock, иллюстрирует отличие между внешним и внутренним выбором:
+
Пример на interlock, иллюстр. отл. между внеш. и внутр. выбором:
-
//Все каналы блокируются, небуферизованные.
+
//Все каналы блкир., небуферизованные.
((x:=c1?|=|c2!e2)++c1!e1) == x:=e
((x:=c1?|=|c2!e2)++c1!e1) == x:=e
-
((x:=c1?|^|c2!e2)++c1!e1) == x:=e |^| stop #stop — специфическое ключевое слово в RSL, обозначает блокировку, тупиковую ситуацию, когда вычисление дальше идти не может.
+
((x:=c1?|^|c2!e2)++c1!e1) == x:=e |^| stop #stop — спец. ключевое слово в RSL, зн. блокировку, тупиковую ситуацию, когда выч. дальше идти не может.
-
Как ещё появляется недетерминизм в RSL? Оператор недетерминированного внутреннего выбора — оператор, привносящий недетерминизм в язык. Можно написать 1|^|2 — явное выражение, являющееся недетерминированным.
+
Лектор говорил, что мы узн, как ещё появл. нед. в RSL/ Оператор нед. внутр. выбра — оператр, привносящий нед. в язык. Можно написать 1|^|2 — явне выр., явл. нед.
-
Семантика гр. у композиции такие, что в случае параллельной композиции или блокировки, тип у операндов должен быть Unit. В случае внешнего и внутреннего выбора тип может быть любой, но одинаковый и у правой, и у левой части.
+
Семант. гр. у кмп. такие, что в случае пар. кмп. или блокировки, тип у операндв должен быть Unit. В случае внеш и внутр. выбора тип мжет быть любй, но одинаковый и у правой, и у левой части.
-
Некие эквивалентности, полезные для упрощения выражений, это в методичке есть:
+
Некие экв., плезные для упр. выр, это в метдичке есть:
expr1||(expr2|^|expr3) is (expr1||expr2)|^|(expr1||expr3)
expr1||(expr2|^|expr3) is (expr1||expr2)|^|(expr1||expr3)
expr1++(expr2|^|expr3) is (expr1++expr2)|^|(expr1++expr3)
expr1++(expr2|^|expr3) is (expr1++expr2)|^|(expr1++expr3)
-
Если у нас каналы… в предположении, что expr1 и expr2 не взаимодействуют, то справедливо след. свойство:
+
Если у нас каналы.... в предположении, что expr1 и expr2 не вщаимдействуют, т справедливо след. св-во:
x:=c1?||c2!expr == (x:=c1;c2!expr)|=|(c2:=expr; x:=c1?)
x:=c1?||c2!expr == (x:=c1;c2!expr)|=|(c2:=expr; x:=c1?)
-
//== и is — граф. и ASCII-нотация
+
//== и is — граф. и ASCII-нтация
x:=c? || c!expr == x:=expr |^| ((x:c?;c!expr)|=|(c!expr;x:=c)|=|(x:=expr))
x:=c? || c!expr == x:=expr |^| ((x:c?;c!expr)|=|(c!expr;x:=c)|=|(x:=expr))
-
На экзамене будут задачи на упрощение параллельных выражений, где будут встречаться все виды из этих 4 композиций, и внутри отдельных подпроцессов могут встретиться if, недетерминированные выборы или же case.
+
Лектор только хтел тметить, что на экз. будут задачи на упр. пар. выр., где будут встр. все виды из этих 4 кмп, и внутри отд. пдпроцессв мгут встр. if, нед. выборы или же case.
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

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


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

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

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_04_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_24_%D1%81%D0%B5%D0%BD%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы