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

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

В прошлый раз были рассмотрены алгебраические спецификации. Сейчас рассмотрим императивный стиль в RSL, на чём занятия в классе завершаются. До этого момент был импл. стиль, который ближе к функциональному программированию. До настоящего момента 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 декабря
• Программирование реализации --- до зачётной сессии

Зачёт без оценки.