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

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

(Различия между версиями)
Перейти к: навигация, поиск
 
(3 промежуточные версии не показаны)
Строка 1: Строка 1:
-
Цель этих 4--5 занятий будет рассказать онвы RSL.
+
Цель этих 4—5 занятий будет рассказать оcновы RSL.
-
Пркт. задание: Небх. будет по здаче написать явную-неявную пецификацию, тетовое покрытие, тетовый драйвер и реализацию на С++, удовлетвряю.щую пец.
+
Практическое задание: Необходимо будет по задаче написать явную-неявную спецификацию, тестовое покрытие, тестовый драйвер и реализацию на С++, удовлетворяющую спецификации.
Типы данных в RSL:
Типы данных в RSL:
Строка 7: Строка 7:
* Int +, −, ×, /, \, ↑, abs, real
* Int +, −, ×, /, \, ↑, abs, real
* Nat {|I=Int, i > 0|}
* Nat {|I=Int, i > 0|}
-
* Real. Вегда должны приут. точка и одна цифра после точки. +, −, ×, /, abs, int (сиречь trunc)
+
* Real. Всегда должны присутствовать точка и одна цифра после точки. +, −, ×, /, abs, int (сиречь trunc)
* Char 'A'...'Z'
* Char 'A'...'Z'
* Text — посл. символов
* Text — посл. символов
-
* Unit. Единст. Значение, исп. для функц. без параметров
+
* Unit. Единственное значение, использующееся для функций без параметров
== Логика в RSL ==
== Логика в RSL ==
-
Трёхзначная, пмимо true/false есть ещё chaos (ошибка, нетипизированное).
+
Трёхзначная, помимо true/false есть ещё chaos (ошибка, нетипизированное).
-
Все таблицы ит. троятся из тог, что в RSL ленивые выч. лог. выр, крме того ~chaos = chaos.
+
Все таблицы ит. строятся из того, что в RSL ленивые вычисления логических выражений, крме того ~chaos = chaos.
(по гор. второй операнд, по верт. — первый)
(по гор. второй операнд, по верт. — первый)
Строка 132: Строка 132:
</td></tr></table>
</td></tr></table>
-
Для описания альтернатив исп. if-then-else:
+
Для описания альтернатив используется if-then-else:
'''if''' expr1 '''then''' expr2 '''else''' expr3 '''end'''
'''if''' expr1 '''then''' expr2 '''else''' expr3 '''end'''
Строка 146: Строка 146:
'''if''' a '''then''' expr2 '''else''' expr3 '''end''' = expr2 = '''if''' a '''then''' expr2 [<math>\frac{true}{a}</math>]'''else''' expr3[false/a] '''end''' = expr2
'''if''' a '''then''' expr2 '''else''' expr3 '''end''' = expr2 = '''if''' a '''then''' expr2 [<math>\frac{true}{a}</math>]'''else''' expr3[false/a] '''end''' = expr2
-
В RSL, как и в бычном матлоге, исп. кванторы &exist;, &forall;, !&exist;.
+
В RSL, как и в обычном матлоге, используются кванторы &exist;, &forall;, !&exist;.
-
Задачи. Будут выпис. тождества обычной логики, нужно прверить, работает ли оно в RSL:
+
Задачи. Будут выписываться тождества обычной логики, нужно проверить, работает ли оно в RSL:
-
~~a &equiv; a — выполняетя
+
~~a &equiv; a — выполняется
true or a &equiv; true — выполняется
true or a &equiv; true — выполняется
Строка 213: Строка 213:
&forall; i: Int &bull; &exist; j: Int &bull; i+j=0 — истина (при j = -i)
&forall; i: Int &bull; &exist; j: Int &bull; i+j=0 — истина (при j = -i)
-
&forall; i: Int &bull; &exist; j: Nat &bull; i+j=0 — не удовл (нельзя найти j для полож. i)
+
&forall; i: Int &bull; &exist; j: Nat &bull; i+j=0 — не удовл (нельзя найти j для положительного i)
&exist; i: Int &bull; &forall; j: Int &bull; i+j=0 — не верно
&exist; i: Int &bull; &forall; j: Int &bull; i+j=0 — не верно
-
Написать на RSL выражение, выраж. тот факт, чт нет наиб. целого числа:
+
Написать на RSL выражение, выражающее тот факт, что нет наиболее целого числа:
~(&exist; i: Int &bull; &forall; j: Int; &bull; (i >= j &equiv; true))
~(&exist; i: Int &bull; &forall; j: Int; &bull; (i >= j &equiv; true))
Строка 225: Строка 225:
== Описание функций в RSL ==
== Описание функций в RSL ==
-
Прежде чем узнать описание функций, узаем, что такое декартово произведение типов:
+
Прежде чем узнать описание функций, узнаем, что такое декартово произведение типов:
Type1 &times; Type2 &times; ... &times; Typen
Type1 &times; Type2 &times; ... &times; Typen
Строка 231: Строка 231:
(5, "ABC", true): Intx &times; Text &times; Bool
(5, "ABC", true): Intx &times; Text &times; Bool
-
Для декартовых произв. опр. тлько равентв и нер.
+
Для декартовых произведений определено только равенство и неравенство
-
Контанты в RSL — частный случай функций (функ. без арг.). Функции могут задаваться:
+
Константы в RSL — частный случай функций (функции без аргументов). Функции могут задаваться:
-
* Явно. опис., как вычисл, или знач.
+
* Явно. описание, как вычисляется, или знач.
-
* Неявно. Накл. условия на знач.
+
* Неявно. Накладываются условия на значения.
-
* Аксиоматически. Опис., ...
+
* Аксиоматически. Опис.,
Константы:
Константы:
Строка 243: Строка 243:
Явное задание:
Явное задание:
-
name: Type = val #задание знач.
+
name: Type = val #задание значения
Пример: x : Int = 5
Пример: x : Int = 5
Строка 251: Строка 251:
x : Int &bull; x > 0
x : Int &bull; x > 0
-
Аксиоматически: мжно исп. оба варианта
+
Аксиоматически: можно использовать оба варианта
В разделе опис. констант: x: Int
В разделе опис. констант: x: Int
-
В раздее опис. аксиом:
+
В разделе опис. аксиом:
'''Axiom'''
'''Axiom'''
x &equiv; 1 или например
x &equiv; 1 или например
Строка 259: Строка 259:
Функции в RSL:
Функции в RSL:
-
* Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^
+
* Всюду вычислимые. Для любого x из области предусловия существует единственное y, таке что f(x) = y^
&forall; x: T1 &bull; !&exist; y : T2 &bull; f(x)=y
&forall; x: T1 &bull; !&exist; y : T2 &bull; f(x)=y
-
* Частично выч. Для нек-рах зн. x могут иметь 2 или блее знач
+
* Частично вычислимые. Для некоторых значений x могут иметь 0, 2 или более значений
'''value'''
'''value'''
name : Type &rarr; result_Type
name : Type &rarr; result_Type
-
для чатично вычислимых — трелочка с тильдой. В случае сложных типов ип. дек. произв.
+
для частично вычислимых — стрелочка с тильдой. В случае сложных типов используется декартово произведение
Явная спецификация:
Явная спецификация:
Строка 280: Строка 280:
'''value'''
'''value'''
f : Int &rarr; Int;
f : Int &rarr; Int;
-
f(x) as r #опр. новой перем, связ. с зн. ф-ции
+
f(x) as r /* определение новой переменной, связанной с значением функции */
-
post r>x #постусловие, связ. арг. и зн. функции
+
post r>x /* постусловие, связывающее аргументы и значения функции */
-
Пример пис. кв. корня:
+
Пример описания квадратного корня:
sqrt : Real трелочка с тильдой Real
sqrt : Real трелочка с тильдой Real
sqrt(x) as s
sqrt(x) as s
Строка 295: Строка 295:
&forall;x"Int &bull; f(x) &equiv; x
&forall;x"Int &bull; f(x) &equiv; x
-
Пример с sqrt: для част. выч. ф-ции предусловие переносится в нач. импл.
+
Пример с sqrt: для частично вычислимой функции предусловие переносится в начало импликации.
'''value'''
'''value'''
sqrt : Real трелочка с тильдой Real
sqrt : Real трелочка с тильдой Real
Строка 319: Строка 319:
cmplx_mul((xr, xi), (yr, yi)) &equiv; (xr&times;yr-xi&times;yi, xi&times;yr+xr&times;yi)
cmplx_mul((xr, xi), (yr, yi)) &equiv; (xr&times;yr-xi&times;yi, xi&times;yr+xr&times;yi)
-
Функция, возвр. некое компл. число, отл. от заданного
+
Функция, возвращающая некое комплексное число, отличное от заданного
'''value'''
'''value'''
cmplx_another : complex &rarr; complex
cmplx_another : complex &rarr; complex

Текущая версия

Цель этих 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

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


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

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