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

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

Перейти к: навигация, поиск

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

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

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

  • Тип данных bool, знчения true, false, операции: ∧, ∨, ~, ⇒, =, ≠
  • Int +, −, ×, /, \, ↑, abs, real
  • Nat {|I=Int, i > 0|}
  • Real. Всегда должны присутствовать точка и одна цифра после точки. +, −, ×, /, abs, int (сиречь trunc)
  • Char 'A'...'Z'
  • Text — посл. символов
  • Unit. Единственное значение, использующееся для функций без параметров

[править] Логика в RSL

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

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

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

T F C
T T F C
F F F F
C C C C
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 [\frac{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

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


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

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