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

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

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

ESyr01 (Обсуждение | вклад)
(Новая: Цель этих 4--5 занятий будет рассказать онвы RSL. Пркт. задание: Небх. будет по здаче написать явную-неявн...)
К следующему изменению →

Версия 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


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


Лекции

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

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


Эта статья является конспектом лекции.
Личные инструменты
Разделы