МФСП, 06 семинар (от 06 октября)

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

В прошлый рз рссм. лг. спец. Сейчс рссм. импертивный стиль в КЫД, Н ЧёМ ЗНЯТИЯ В КЛССЕ ЗВЕРШ. До этого момент был имплик. стиль, ктрый ближе к функ. прогрммировнию. Д нст. ммент RSL был ближе к функ. пргр. Н исп. RSL, мжно писть спец., близкие к имп. стилю.

Нч. с пнятия перем:

variable id : Type = val

Пример:

variable
  a, b : Int,
  n : Nat = 1,
  r : Nat = 0

Чт миы мжем с переменными делть:

• присвоение

id = val

Плуч. выр. н длжно иметь тип. Выр. имеет тип Unit.

Имея перем и присв. для них, мы хтим чт-т делть. Хтим функции.

Функции пис. след. брзм:

value
  f1 : Unit → write n, b read a, r Nat

В имп. стиле функции, котрые чит. и пишут. глб. перем. нз. функции с глоб эффектом. ни бычно прм. не имеют.

Сст перции:

expr1, expr2, expr3

Результт тип посл выр.

x = 1; x

В результте знч. выр. 1, x стнвится рвным 1.

x = 1; x = x / 2

Знач выр. (), x ≡ 0.5

if импертивный:

if val then expr1 (типа Unit)
  else expr2 (типа Unit)
end

Циклы:

while bool_val do unit_expr1 end

do unit_expr until bool_val end

for пр. тльк для спис. структур:

for list_limit do unit_expr end

пример:

for i in <1..n> do x=x+i end

Переменные могут быть бъявл. как локльные, тогд их бл. видимости будет огр.

local
  variable x : Type, ...
in
  expr1, ... exprn;
end

Имплик. зпись мжно исп. кк для явнго тк и для неявнго опис. функций.

Пример:

variable cnt : Nat
value
  inc : Unit → write cnt Nat
    inc() ≡ cnt = cnt + 1; cnt

Импер. стиль мжно исп. и ля неявнй спец. Но тут возн. вопрс: нм нужн в пстусл. ссылться н сост. перем кк до, тк и псле. Для этог исп. пстрф: id` — предыдущее сост. переменнй.

Пример:

variable
  s : Int-set
value
  choose : Unit → с волной write s Int
    choose() as res
    post res ∈ s` ∧ s = s` \ {res}
    pre s ≠ {}

Здчи.

Дпустим, бъявлен variable x : Int. Для кждого выр. пр. тип и знач. перем. x:

x = 1; x = 2

Выр: Unit, (), x ≡ 2

(x = 1; x) + (x = 2; x)

Выр: Int, 3, x ≡ 2

Пострить явн. спец. в имп. стиле ф-ции _sum, ктря выч. сумму нт. ряд. Для ряд исп. список.

С исп. глб. перем:

variable
  list : Nat*
  s : Nat
value
  sum : Nat → write s read list Nat
    sum(l) ≡ s = 0; for i in <1..l> do s = s + list(i) end; s
    pre l ≤ len list

С исп. лк. перем:

variable
  list : Nat*
value
  sum : Nat → write s read list Nat
    sum(l) ≡
      local
        variable
          s : Nat = 0
      in
        for i in <1..l> do s = s + list(i) end; s
      end
    pre l ≤ len list

С исп. while:

variable
  list : Nat*
value
  sum : Nat → write s read list Nat
    sum(l) ≡
      local
        variable
          s : Nat = 0,
          i : Nat = 1
      in
        while i ≤ l do s = s + list(i); i = i + 1 end; s
      end
    pre l ≤ len list

Задача: постр. опис. стека.

variable
  Stack : T*

value
  Empty : T* = <>

  push : T → write Stack Unit
    push(l) ≡ Stack = <l> ^ Stack

  pop : Unit → write Stack Unit
    pop() ≡ Stack = tl Stack

  isempty : Unit → read Stack Unit
    isempty() ≡ Stack ≡ <>

  peek : Unit → read Stack Nat
    peek() ≡ Stack(0)
    pre not isempty(Stack)

Специф. пр. выч. в RSL

Нчнём с понятия кнлов. Похже н пнятие перем, но эт не тльдко тчк перед. инф., н и тчк синхр.

Синтксис:

channel
  id : Type,
  a : Nat,
  b, c : Int

Анлгич. рбте с перем, укз. типы дступ по рбте с кнлми при объявл. функции:

value
  p : Unit → in a  out b Unit

У нс есть кнл с им. id, и для счит. исп. кнстр. id?. Эт выр. имеет тип тип кнл, и ег можн присв.

x := c?

Рз мы мжем читть, знчит ни лжны туд кк-т пдтью Для зписи исп. кнстр. id!val.

a!0

Есть кнлы кк т. синхр, есть опер. рбты с кнлми. Н не дшли до пр. выч.

Пр. выр. в rsl форм. след. брзом: есть expr1, expr2. Мжн спец., чт они выч. прллельно: expr1 . expr2, где тчк мжет иметь след. вид:

• || — прллельня компзиция
• [] (прямоугльник) — внеш. выбор
• П (прямроуг. без ниж. ребра) — внутр. выбор
• ++ (перечёрк. прямый) — взаимня блкировка.

Пусть есть

channel c : Int
variable x : Int

И зписн констр:

x := c? || c!5

При этм мы не мжем не гр ни прядок, ни взимод. Какие мгут быть вринты:

• x = 5
• ∅

В блее слжнм случе:

(x := c? || c!5) || c!7

Для тког выр. x мжет стть рвным и 5, и 7, и ничему.

неш. выбр:

x := c? [] d!5

Внеш. выбор. зн., чт выч. т чсть выр., для ктрой есть усл. выч., здння извне. Если мы дпишем тке условие:

(x := c? [] d!5) ||  c!1

То x присвится 1.

В случе с П пкзывем, что внеш. выбр невжен, и тогд x мжет быть рвным 1 или не мжет.

(x := c? П d!5) ||  c!1

Взимня блкировка.

channel c : T
variable x : T
value e : T

И тке выржение:

x := c! ++ c!e ≡ x = 2

Выч. снчл т, кторе мжет вычислиться. В дннм случе эт выр. экв. x := e

Н этй рдужнй нте семинрские здния звершим, и выддим задния.

Задание либ в метдичке, либо н сйте sp.cs.msu.su/mfsp

Сдача:

• Снпч. небх. сдть лг. спец. — д1 нября
• П ней небх. сдть явн-нефвн спец. --- до 1 декбря
• Пргр. релиз. --- д зч. сессии

Прядок сдчи: есть чекре, пкз., чт н не ругется, птм Петрвскму или Глвину её рсск., покз. В эти дни, в этй же удитории.

Зсёт без ценки.