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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Новая: В прошлый рз рссм. лг. спец. Сейчс рссм. импертивный стиль в КЫД, Н ЧёМ ЗНЯТИЯ В КЛССЕ ЗВЕРШ. До этого мом...)
 
Строка 1: Строка 1:
-
В прошлый рз рссм. лг. спец. Сейчс рссм. импертивный стиль в КЫД, Н ЧёМ ЗНЯТИЯ В КЛССЕ ЗВЕРШ. До этого момент был имплик. стиль, ктрый ближе к функ. прогрммировнию. Д нст. ммент RSL был ближе к функ. пргр. Н исп. RSL, мжно писть спец., близкие к имп. стилю.
+
В прошлый раз были рассмотрены алгебраические спецификации. Сейчас рассмотрим императивный стиль в RSL, на чём занятия в классе завершаются. До этого момент был импл. стиль, который ближе к функциональному программированию. До настоящего момента RSL был ближе к функциональному программированию. Используя RSL, можно записать спецификации, близкие к императивному стилю.
-
Нч. с пнятия перем:
+
Начнём с понятия переменной:
'''variable''' id : Type = val
'''variable''' id : Type = val
Строка 10: Строка 10:
r : Nat = 0
r : Nat = 0
-
Чт миы мжем с переменными делть:
+
Что мы можем с переменными делать:
* присвоение
* присвоение
id = val
id = val
-
: Плуч. выр. н длжно иметь тип. Выр. имеет тип Unit.
+
: Получаемое выражение не должно иметь тип. Выражение имеет тип Unit.
-
Имея перем и присв. для них, мы хтим чт-т делть. Хтим функции.
+
Имея переменные и присваивания для них, мы хотим чт-то делать. Хотим функции.
-
Функции пис. след. брзм:
+
Функции описываются следующим образом:
'''value'''
'''value'''
f1 : Unit → '''write''' n, b '''read''' a, r Nat
f1 : Unit → '''write''' n, b '''read''' a, r Nat
-
В имп. стиле функции, котрые чит. и пишут. глб. перем. нз. функции с глоб эффектом. ни бычно прм. не имеют.
+
В императивном стиле функции, которые читают и пишут глобальные переменные называются функции с глобальным эффектом. Они обычно переменных не имеют (?).
-
Сст перции:
+
Составные операции:
expr1, expr2, expr3
expr1, expr2, expr3
-
Результт тип посл выр.
+
Результат тип посл выр.
x = 1; x
x = 1; x
-
В результте знч. выр. 1, x стнвится рвным 1.
+
В результате значение выражения 1, x становится равным 1.
x = 1; x = x / 2
x = 1; x = x / 2
-
Знач выр. (), x ≡ 0.5
+
Значение выражения (), x ≡ 0.5
-
if импертивный:
+
if императивный:
'''if''' val '''then''' expr1 (типа Unit)
'''if''' val '''then''' expr1 (типа Unit)
'''else''' expr2 (типа Unit)
'''else''' expr2 (типа Unit)
Строка 44: Строка 44:
'''do''' unit_expr '''until''' bool_val '''end'''
'''do''' unit_expr '''until''' bool_val '''end'''
-
for пр. тльк для спис. структур:
+
for применим только для списочных структур:
'''for''' list_limit '''do''' unit_expr '''end'''
'''for''' list_limit '''do''' unit_expr '''end'''
Строка 50: Строка 50:
'''for''' i in <1..n> '''do''' x=x+i '''end'''
'''for''' i in <1..n> '''do''' x=x+i '''end'''
-
Переменные могут быть бъявл. как локльные, тогд их бл. видимости будет огр.
+
Переменные могут быть объявлены как локальные, тогда их область видимости будет ограничена:
'''local'''
'''local'''
'''variable''' x : Type, ...
'''variable''' x : Type, ...
Строка 57: Строка 57:
'''end'''
'''end'''
-
Имплик. зпись мжно исп. кк для явнго тк и для неявнго опис. функций.
+
Импл. запись можно использовать как для явного так и для неявного описания функций.
Пример:
Пример:
Строка 65: Строка 65:
inc() &equiv; cnt = cnt + 1; cnt
inc() &equiv; cnt = cnt + 1; cnt
-
Импер. стиль мжно исп. и ля неявнй спец. Но тут возн. вопрс: нм нужн в пстусл. ссылться н сост. перем кк до, тк и псле. Для этог исп. пстрф: id` — предыдущее сост. переменнй.
+
Императивный стиль можно использовать и для неявной спецификации. Но тут возникает вопрос: нам нужно в постусловии ссылаться на состояние переменной как до, так и после. Для этого используется апостроф: id` — предыдущее состояние переменной.
Пример:
Пример:
Строка 76: Строка 76:
'''pre''' s &ne; {}
'''pre''' s &ne; {}
-
Здчи.
+
Задачи.
-
Дпустим, бъявлен '''variable''' x : Int. Для кждого выр. пр. тип и знач. перем. x:
+
Допустим, объявлена '''variable''' x : Int. Для каждого выражения определим тип и значение переменной x:
x = 1; x = 2
x = 1; x = 2
Выр: Unit, (), x &equiv; 2
Выр: Unit, (), x &equiv; 2
Строка 84: Строка 84:
Выр: Int, 3, x &equiv; 2
Выр: Int, 3, x &equiv; 2
-
Пострить явн. спец. в имп. стиле ф-ции _sum, ктря выч. сумму нт. ряд. Для ряд исп. список.
+
Построить явную спецификацию в императивном стиле функции _sum, которая вычисляет сумму натурального ряда. Для ряда использовать список.
-
С исп. глб. перем:
+
С использованием глобальных переменных:
'''variable'''
'''variable'''
list : Nat*
list : Nat*
Строка 95: Строка 95:
'''pre''' l &le; len list
'''pre''' l &le; len list
-
С исп. лк. перем:
+
С использованием локальных переменных:
'''variable'''
'''variable'''
list : Nat*
list : Nat*
Строка 109: Строка 109:
'''pre''' l &le; len list
'''pre''' l &le; len list
-
С исп. while:
+
С использованием while:
'''variable'''
'''variable'''
list : Nat*
list : Nat*
Строка 124: Строка 124:
'''pre''' l &le; len list
'''pre''' l &le; len list
-
Задача: постр. опис. стека.
+
Задача: построить описание стека.
'''variable'''
'''variable'''
Stack : T*
Stack : T*
Строка 144: Строка 144:
'''pre''' not isempty(Stack)
'''pre''' not isempty(Stack)
-
Специф. пр. выч. в RSL
+
== Спецификация параллельных вычислений в RSL ==
-
Нчнём с понятия кнлов. Похже н пнятие перем, но эт не тльдко тчк перед. инф., н и тчк синхр.
+
Начнём с понятия каналов. Похоже на пнятие переменной, но это не только точка передачи информации, но и точка синхронизации.
-
Синтксис:
+
Синтаксис:
'''channel'''
'''channel'''
id : Type,
id : Type,
Строка 154: Строка 154:
b, c : Int
b, c : Int
-
Анлгич. рбте с перем, укз. типы дступ по рбте с кнлми при объявл. функции:
+
Аналогично работе с переменными, указ. типы доступны по работе с каналами при объявлении функции:
'''value'''
'''value'''
p : Unit &rarr; '''in''' a '''out''' b Unit
p : Unit &rarr; '''in''' a '''out''' b Unit
-
У нс есть кнл с им. id, и для счит. исп. кнстр. id?. Эт выр. имеет тип тип кнл, и ег можн присв.
+
У нас есть канал с именем id, и для считывания используется конструкция id?. Это выражение имеет тип канал, и его можно присваивать.
x := c?
x := c?
-
Рз мы мжем читть, знчит ни лжны туд кк-т пдтью Для зписи исп. кнстр. id!val.
+
Для записи используется конструкция id!val.
a!0
a!0
-
Есть кнлы кк т. синхр, есть опер. рбты с кнлми. Н не дшли до пр. выч.
+
Есть каналы кк т. синхронизации, есть операции работы с каналами. Но не дошли до параллельных вычислений.
-
Пр. выр. в rsl форм. след. брзом: есть expr1, expr2. Мжн спец., чт они выч. прллельно: expr1 . expr2, где тчк мжет иметь след. вид:
+
Параллельное вычисление в rsl формулируется следующим образом: есть expr1, expr2. Можно специфицировать, что они вычисляют параллельно: expr1 . expr2, где точка может иметь следующий вид:
-
* || — прллельня компзиция
+
* || — параллельная композиция
-
* [] (прямоугльник) — внеш. выбор
+
* [] (прямоугльник) — внешний выбор
-
* П (прямроуг. без ниж. ребра) — внутр. выбор
+
* П (прямоугольник без нижнего ребра) — внутренний выбор
-
* ++ (перечёрк. прямый) — взаимня блкировка.
+
* ++ (перечёркнутый прямоугольник) — взаимная блокировка.
Пусть есть
Пусть есть
Строка 175: Строка 175:
'''variable''' x : Int
'''variable''' x : Int
-
И зписн констр:
+
И записана конструкция:
x := c? || c!5
x := c? || c!5
-
При этм мы не мжем не гр ни прядок, ни взимод. Какие мгут быть вринты:
+
При этом мы не можем гарантировать порядок взаимодействий. Какие могут быть варианты:
* x = 5
* x = 5
* &empty;
* &empty;
-
В блее слжнм случе:
+
В более сложном случае:
(x := c? || c!5) || c!7
(x := c? || c!5) || c!7
-
Для тког выр. x мжет стть рвным и 5, и 7, и ничему.
+
Для такого выражения x может стать равным и 5, и 7, и ничему.
-
неш. выбр:
+
внешний выбор:
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 мжет быть рвным 1 или не мжет.
+
В случае с П показываем, что внешний выбор неважен, и тогда x может быть равным 1 или не может.
(x := c? П d!5) || c!1
(x := c? П d!5) || c!1
-
Взимня блкировка.
+
Взаимная блокировка.
'''channel''' c : T
'''channel''' c : T
'''variable''' x : T
'''variable''' x : T
'''value''' e : T
'''value''' e : T
-
И тке выржение:
+
И такое выражение:
x := c! ++ c!e &equiv; x = 2
x := c! ++ c!e &equiv; x = 2
-
Выч. снчл т, кторе мжет вычислиться. В дннм случе эт выр. экв. x := e
+
Вычислим сначала то, которое может вычислиться. В данном случае это выражение эквивалентно x := e
-
Н этй рдужнй нте семинрские здния звершим, и выддим задния.
+
На этой радужной ноте семинарские занятия завершим, и выдадим задания.
-
Задание либ в метдичке, либо н сйте sp.cs.msu.su/mfsp
+
Задание либо в методичке, либо на сайте sp.cs.msu.su/mfsp
Сдача:
Сдача:
-
* Снпч. небх. сдть лг. спец. — д1 нября
+
* Сначала необходимо сделать алгебраическую спецификацию — до 1 ноября
-
* П ней небх. сдть явн-нефвн спец. --- до 1 декбря
+
* По ней необходимо сделать явную-неявную спецификацию --- до 1 декабря
-
* Пргр. релиз. --- д зч. сессии
+
* Программирование реализации --- до зачётной сессии
-
Прядок сдчи: есть чекре, пкз., чт н не ругется, птм Петрвскму или Глвину её рсск., покз. В эти дни, в этй же удитории.
+
Зачёт без оценки.
-
 
+
-
Зсёт без ценки.
+
-
 
+
-
<!-- У меня 5 впринт. -->
+
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

Текущая версия

В прошлый раз были рассмотрены алгебраические спецификации. Сейчас рассмотрим императивный стиль в 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

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


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

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_06_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_06_%D0%BE%D0%BA%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы