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

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

(Различия между версиями)
Перейти к: навигация, поиск
Строка 261: Строка 261:
* Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^
* Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^
∀ x: T1 • !∃ y : T2 • f(x)=y
∀ x: T1 • !∃ y : T2 • f(x)=y
-
* Частично выч. Для нек-рах зн. x могут иметь 2 или блее знач
+
* Частично выч. Для нек-рах зн. x могут иметь 0, 2 или блее знач
'''value'''
'''value'''
name : Type → result_Type
name : Type → result_Type
-
для чатично вычислимых — трелочка с тильдой. В случае сложных типов ип. дек. произв.
+
для чатично вычислимых — стрелочка с тильдой. В случае сложных типов ип. дек. произв.
Явная спецификация:
Явная спецификация:
Строка 280: Строка 280:
'''value'''
'''value'''
f : Int → Int;
f : Int → Int;
-
f(x) as r #опр. новой перем, связ. с зн. ф-ции
+
f(x) as r /* опр. новой перем, связ. с зн. ф-ции */
-
post r>x #постусловие, связ. арг. и зн. функции
+
post r>x /* постусловие, связ. арг. и зн. функции */
Пример пис. кв. корня:
Пример пис. кв. корня:

Версия 15:26, 4 октября 2008

Цель этих 4--5 занятий будет рассказать онвы 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

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


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

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