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

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

---

Версия 15:06, 12 сентября 2008

Цель этих 4--5 занятий будет рассказать онвы RSL.

Пркт. задание: Небх. будет по здаче написать явную-неявную пецификацию, тетовое покрытие, тетовый драйвер и реализацию на С++, удовлетвряю.щую пец.

Типы данных в RSL:

• Тип данных bool, знчения true, false, перации: and, or, ~, =>, =, !=
• Int +-*/ \ uparr, abs, real
• Nat {|I=Int, i > 0|}
• Real. Вегда должны приут. точка и одна цифра после точки. +-*/, abs, int (сиречь trunc)
• Char 'A'...'Z'
• Text --- посл. символов
• Unit. Единст. Значение, исп. для функц. без параметров

Логика в RSL

Трёхзначная, пмимо true/false есть ещё chaos (ошибка, нетипизированное).

Все таблицы ит. троятся из тог, что в RSL ленивые выч. лог. выр, крме того ~chaos = chaos.

(по гор. второй операнд, по верт. --- первый)

and T F C
  T T F C
  F F F F
  C C C C

 or T F C
  T T T T
  F T F C
  C C C C

 => T F C
  T T F C
  F T T T
  C C C C

  = a b C
  a T F C
  b F T C
  C C C C

 == a b C
  a T F F
  b F T F
  C F F T

Для описания альтернатив исп. if-then-else:

if expr1 then expr2 else expr3 end

Как вычисляется:

if true then expr2 else expr3 end = expr2

if false then expr2 else expr3 end = expr3

if chaos then expr2 else expr3 end = chaos

if a then expr2 else expr3 end = expr2 = if a then expr2 [true/a]else expr3[false/a] end = expr2

В RSL, как и в бычном матлоге, исп. кванторы ∃, ∀, !∃.

Задачи. Будут выпис. тождества обычной логики, нужно прверить, работает ли оно в RSL:

~~a == a --- выполняетя

true or a == true --- выполняется

a or true == true --- не выполняется (если подставить chaos)

a => true == true --- не выполняется

a => b == ~a or b

a => b == ~a or b T F C
                T T T T
                F T T T
                C T T T

--- выполняетя

a or ~a == true --- не выполняется

a and ~a == false --- не выполняется

a and b and c == a and (b and c)

a = chaos: chaos == chaos = true
a = false: false == false = true
a = true:  b = chaos: chaos == chaos = true
           b = false: false == false = true
           b = true:  c == c = true

выполняется

a or b or c == a or (b or c)

a = chaos: chaos == chaos = true
a = true:  truee == true = true
a = false: b = chaos: chaos == chaos = true
           b = true:  true == true = true
           b = false: c == c = true

выплняется

(a=a)==true --- не выполняется

(a==a)==true --- выполняется

Чему равно значение выражения:

if true then false else chaos end = true

if a then ~a==chaos else false end

a expr
T  T
F  F
C  C

= a

if a then ~a=chaos else false end

a expr
T  C
F  F
C  C

Являются ли истиной лед. выражения:

∀ i: Int ˙ ∃ j: Int ˙ i+j=0 --- истина (при j = -i)

∀ i: Int ˙ ∃ j: Nat ˙ i+j=0 --- не удовл (нельзя найти j для полож. i)

∃ i: Int ˙ ∀ j: Int ˙ i+j=0 --- не верно

Написать на RSL выражение, выраж. тот факт, чт нет наиб. целого числа:

~(∃ i: Int ˙ ∀ j: Int; ˙ (i >= j == true))

∀ i: Int ˙ ∃ j: Int; ˙ (i >= j == true)

Опиание функций в RSL

Прежде чем узнать описание функций, узаем, что такое декартово произведение типов:

Type1 × Type2 × ... × Typen

(5, "ABC", true): Intx × Text × Bool

Для декартовых произв. опр. тлько равентв и нер.

Контанты в RSL --- частный случай функций (функ. без арг.). Функции могут задаваться:

• Явно. опис., как вычисл, или знач.
• Неявно. Накл. условия на знач.
• Аксиоматически. Опис., ...

Константы:

value
  name : Type

Явное задание:

name: Type = val #задание знач.

Пример: x : Int = 5

Неявно:

name : Type ˙ cond
x : Int ˙ x > 0

Аксиоматически: мжно исп. оба варианта

В разделе опис. констант: x: Int
В раздее опис. аксиом:
Axiom
  x == 1 или например
  x > 0

Функции в RSL:

• Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^

∀ x: T1 ˙ !∃ y : T2 ˙ f(x)=y

• Частично выч. Для нек-рах зн. x могут иметь 0б 2 или блее знач

value
  name : Type → result_Type

для чатично вычислимых --- трелочка с тильдой. В случае сложных типов ип. дек. произв.

Явная спецификация:

value 
  f : Int → Int;
  f(x) = x + 1

  p : Real стрелочка с тильдой Real
  p(x) == 1.0
  pre x ≠ 0.0 #условия на аргумент

Неявная спецификация:

value 
  f : Int → Int;
  f(x) as r #опр. новой перем, связ. с зн. ф-ции
  post r>x #постусловие, связ. арг. и зн. функции

Пример пис. кв. корня:

  sqrt : Real трелочка с тильдой Real
  sqrt(x) as s
  post ((s*s=x) and (s≥0.0))
  pre x≥0.0

Акс. запись:

value 
  f : Int → Int;
axiom
  ∀x"Int ˙ f(x) == x

Пример с sqrt: для част. выч. ф-ции предусловие переносится в нач. импл.

value 
  sqrt : Real трелочка с тильдой Real
axiom
  ∀x:Real ˙ x ≥ 0.0 ⇒ ∃s: Real ˙ sqrt(x)=s and s*s=x and s ≥ 0.0

Задачи:

type
  complex = Real × Real

Определить 0:

value
  cmplx_zero: complex = (0.0, 0.0)

Функция сложения:

value
  cmplx_add: complex × complex → complex;
  cmplx_add((xr, xi), (yr, yi)) == (xr+yr, xi+yi)

Функция умножения:

value
  cmplx_mul: complex × complex → complex;
  cmplx_mul((xr, xi), (yr, yi)) == (xr*yr-xi*yi, xi*yr+xr*yi)

Функция, возвр. некое компл. число, отл. от заданного

value
  cmplx_another : complex → complex
  cmplx_another(x) as a
  post a ≠ x