МФСП, 02 семинар (от 08 сентября)
Материал из eSyr's wiki.
Цель этих 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
Формальная спецификация и верификация программ
|
|