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

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

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

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

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

Текущая версия Ваш текст
Строка 1: Строка 1:
Неполная спецификация.
Неполная спецификация.
-
Неполная спецификация --- спецификация, описывающая не все детали реализации
+
Н. с. --- с., пис. не все детали реализации
'''value'''
'''value'''
MAX_PACKET : Int
MAX_PACKET : Int
-
Мы можем указать границы, в которых находится константа, но эта спецификация также будет неполна:
+
Мы мжем указать границы, в которых нахдится конст, н эта спец. также будет неполна:
'''value'''
'''value'''
MAX_PACKET : Int := MAX_PACKET ≥ 1024
MAX_PACKET : Int := MAX_PACKET ≥ 1024
-
Недетерминированная функция — функция, которая при одном и том же значении возвращает различные результаты.
+
Недетерм. функция — функция, которая при одном и том же значении взвр. разл. рез-ты.
-
# Неполная спецификация констант — когда недостаточно информации для получения значения константы
+
Летор просит завписать в тетр. опр. 4 понятий:
-
# Неполная спецификация функции — когда недостаточно информации для получения значения функции
+
# Неп. спец. конст
-
# Недетерминированная спецификация константы — когда константа определена так, что её значение неизвестно
+
# Неп. спец. функции
-
# Недетерминированная спецификация функции — когда функция определена так, что её значение для пр. набора (наборов) параметров неизвестно
+
# Недетерм. спец. конст.
 +
# Недетерм. спец. функции
-
В RSL нет возможности представить недетерминизм констант, и там такого понятия нет.
+
# Неп. спец. конст — когда недост. инф. для полоуч. зн. конст.
 +
# Неп. спец. функции — когда недост. инф. для получ. зн. функции
 +
# Недетерм. спец. конст. — когда константа опр. так, что её знач. неизвестно
 +
# Недетерм. спец. функции — когда функция опр. так, что её знач. для пр. набора (наборов) параметров неизвестно
-
Для функций же недетерминизм возможен, это происходит тогда, кгда при дном наборе параметров возвращаются разные значения.
+
В RSL нет возм. предст. предст. недетерменизм конст., и там таког понятия нет.
-
И ситуация, когда мы не написали ничего, кроме сигнатуры — типичный пример неполной спецификации. Или же мы написали только постусловие или аксиому, неполное описание поведение функции. Например:
+
Для функций же недетерм. взмжен, это происх. тогда, кгда при дном наборе параметров возвр. разные значения.
 +
 
 +
И ситуация, когда мы не написали ничего, кроме сигн — типичный пример неп. чспец. Или же мы нап. тлько постусл. или аксиому, неполн. опис. поведение функции. Например:
'''value'''
'''value'''
Строка 29: Строка 35:
'''post''' (y=) ∨ (y=x-1) ∨ (y=x+1)
'''post''' (y=) ∨ (y=x-1) ∨ (y=x+1)
-
Насколько мы могли знать из семинаров, бывают полностью пр. и неполно определённые функции. Неполно определённые обозначаются в ASCII-нотации как ~→. При исп. → известно, что функция является детерминированной и тотальной. При использовании ~→ функция может быть нетот. и недетерминированной.
+
Наск. мы мгли знать из семинаров, бывают полностью пр. и неп. опр. функции. Неп. опр. обозн. в ASCII-нтации как ~→. При исп. → известн, что ф-ция явл. детерминированной и тотальной. При исп. ~→ функция мжет быть нетот. и недетерм.
-
Если же функция может детерминированно менять значение, то мы сможем описать некое условие на некое дополнительное множество, которое введём специально. И можно ввести дополнительные условия, чтобы но удовлетворяющие некоему распределению с произвольной точностью. обычно это актуально при введении функции генерации сл. значений.
+
Если же функция может детерм. менять значение, то мы см. описать некое усл. на неке доп. мн-во, кторое введём специалдьно. И мжно ввести дп. условия, чтобы но удовл. некоему распр. с пр. точнстью. бычно это актуально при введении функции генерации сл. зн.
-
При неполной спецификации мы можем допустить некоторую вольность в реализации. Недетерминированная спецификация может возвращать различные значения, будучи вызванной в одной и той же ситуации.
+
При неп. спец. мы мжем дп. нек-ую вльность в реализации. Нед. спец. может возвр. разл. знач, будучи вызв. в одной и той же ситуации.
-
Примеры использования понятий неполной спецификации:
+
Лектор просит написать рядм с кждый опр. небольшой пример, когда это может встретиться. В каких ситуациях сотв. понятие мжет быть использовано.
1.
1.
Строка 49: Строка 55:
'''post''' (y > 0)
'''post''' (y > 0)
-
Единственное отличие — какой синтаксис использовать — написать аксиому, или ещё что. Второй вариант — константный предметной области, диапазон, список (коды ошибок).
+
Единст. отл. — какой синт исп. — написть аксиому, идли ещё что. Втрй вариант — констатнты предм. бласти, диапазн, список (коды ошибок).
-
В RSL нет понятия времени, но мы можем его ввести дополнительно, например, в качестве глобальной переменной Синтаксические способы могут быть придуманы, но непосредственно в языке этого не предусмотрено. Временное расширение RSL есть, но в курсе не рассматривается.
+
В RSL нет понятия времени, но мы можем его ввести дополнительно, например, в качестве глб. перем. Синт. способы могут быть предуманы, но непоср. в языке этго не преждусм. Временное расш. RSL есть, но лектор его не рассм.
-
Что касается вопроса относительно спецификации алгоритма, то в RSL, когда мы описываем спецификацию, мы описываем её значимое и побочное действие. Ограничения на внутреннюю реализацию на RSL никак описаны быть не могут, кроме как придумывая синтетический способ.
+
Что кас. вопр. отн. специф. алгоритма, то в RSL, когда мы опис. спец., мы опис. её знач. и побоч. действие. Огр. на внутр. реализацию на RSL никак описаны быть не могут, кроме как придумывая синтетич. способ.
-
В то же время спецификация может относиться не только к результату, но и к тому, как она бн. переменную. Этт аспект может быть недоспецифицирован.
+
В то же время спец. может отн. не только к результату, но и к тому, как она бн. переменную. Этт аспект мжет быть недоспецифицирован.
-
Пример недоспецификации и неполной спецификации — когда задан RNG, у которого не задано распределение.
+
Пример нед. и неп. специф. — кгджа задан RNG, у кторого не задано распределение.
-
Рассмотрим соотношение между моделью и системой, реализация, которая специфицируется. Есть модель, есть реализация, система, её реализующая. Может быть 4 вариант, когда модель является детерминированной и система детерминирована, модель недетерминирована и система детерминирована, модель детерминирована, система недетерминирована, и когда обе системы недетерминированы.
+
Рассмтрим соотн. между моделью и системой, реализацие, кторая специфицируется. Есть мдель, есть реализацуия, система, её реализующая. Может быть 4 вариант, кгда мдель явл. детерменированной и систе. дет., м. нед. и сист. дет., мд. дет., сист. нед., и когд обе системы нед.
-
С первым случаем всё достаточно понятно. Второй вариант, когда модель является недетерминированной, а система, её реализация, является детерминированной, достаточно странный вариант, но в природе существовать может. Например, стандарт POSIX. Если стандарт не требует конкретного значения, описания кода ошибки, а система при этом конкретные значения приписывает. Этот пример неправильный, поскольку в этом случае модель неполна. Это действительно странный случай, когда мы описываем, что функция может возвращать недетерминированное значение, а реализация при этом детерминирована. Здесь говорится о недетерминированности с т.з. спецификации. Например, если реализация имеет внутренний счётчик и каждый раз, инкримирует его, возвращает значение, то этот недетерминизм пр. с т.з. специф. f : Int ~→ Int f(x) as y '''post''' (y > 0).
+
С первым случаем всё дост. понятно. Второй вариант, когда мдель явл. нед., а система, её реализ., явл. дет., дост. странный вариант, н в природе сущ. мжет. Например, стандарт POSIX. Если стандарт не тр. конкр. знач., опис. код шибки, а система при этом конкр. зн. приписывает. Этот пример неправильныцй, поск. в этом случае мдель неполна. Это действ. странный случай, кгда мы опис., что функция может возвр. нед. знач, а реализ. при этом детерм. Здесь говорится о нед. с т. з. спецификации. Например, если реализ. имеет внутр. счётчик и каждый раз, инкр. его, взвр. знач., то эт нед. пр. с т. з. специф. f : Int ~→ Int f(x) as y '''post''' (y > 0).
-
Как мы выяснили, понятие детерминизма-недетерминизма реализации рассматривается тн. модели, а не по своим внутренним зар-кам.
+
Как мы выясн., пнятие дет.-нед. реализации рассм. тн. модели, а не по свим внутр. зар-кам.
-
Какие ещё пример: мель детали, системы недетерминированы. Это достаточно реальный пример, может встретиться, когда спецификация неполна. Например, если в спецификации результирующего типа 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
Разделы