МФСП, 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 декабря
  • Программирование реализации --- до зачётной сессии

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


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы