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

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

(Различия между версиями)
Перейти к: навигация, поиск

ESyr01 (Обсуждение | вклад)
(Новая: В прошлый рз рссм. лг. спец. Сейчс рссм. импертивный стиль в КЫД, Н ЧёМ ЗНЯТИЯ В КЛССЕ ЗВЕРШ. До этого мом...)
К следующему изменению →

Версия 01:03, 13 октября 2008

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

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


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

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