Редактирование: МФСП, 02 семинар (от 08 сентября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | Цель этих | + | Цель этих 4--5 занятий будет рассказать онвы RSL. |
- | + | Пркт. задание: Небх. будет по здаче написать явную-неявную пецификацию, тетовое покрытие, тетовый драйвер и реализацию на С++, удовлетвряю.щую пец. | |
Типы данных в RSL: | Типы данных в RSL: | ||
- | * Тип данных bool, знчения true, false, | + | * Тип данных bool, знчения true, false, перации: and, or, ~, =>, =, != |
- | * Int + | + | * Int +-*/ \ uparr, abs, real |
* Nat {|I=Int, i > 0|} | * Nat {|I=Int, i > 0|} | ||
- | * Real. | + | * Real. Вегда должны приут. точка и одна цифра после точки. +-*/, abs, int (сиречь trunc) |
* Char 'A'...'Z' | * Char 'A'...'Z' | ||
- | * Text | + | * Text --- посл. символов |
- | * Unit. | + | * 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, как и в бычном матлоге, исп. кванторы ∃, ∀, !∃. |
- | Задачи. Будут | + | Задачи. Будут выпис. тождества обычной логики, нужно прверить, работает ли оно в RSL: |
- | ~~a | + | ~~a == a --- выполняетя |
- | true or a | + | true or a == true --- выполняется |
- | a or true | + | a or true == true --- не выполняется (если подставить chaos) |
- | a => true | + | a => true == true --- не выполняется |
- | a => b | + | a => b == ~a or b |
- | a => b | + | a => b == ~a or b T F C |
T T T T | T T T T | ||
F T T T | F T T T | ||
C T T T | C T T T | ||
- | + | --- выполняетя | |
- | a or ~a | + | a or ~a == true --- не выполняется |
- | a and ~a | + | a and ~a == false --- не выполняется |
- | a and b and c | + | a and b and c == a and (b and c) |
- | a = chaos: chaos | + | a = chaos: chaos == chaos = true |
- | a = false: false | + | a = false: false == false = true |
- | a = true: b = chaos: chaos | + | a = true: b = chaos: chaos == chaos = true |
- | b = false: false | + | b = false: false == false = true |
- | b = true: c | + | b = true: c == c = true |
- | + | выполняется | |
- | a or b or c | + | a or b or c == a or (b or c) |
- | a = chaos: chaos | + | a = chaos: chaos == chaos = true |
- | a = true: truee | + | a = true: truee == true = true |
- | a = false: b = chaos: chaos | + | a = false: b = chaos: chaos == chaos = true |
- | b = true: true | + | b = true: true == true = true |
- | b = false: c | + | b = false: c == c = true |
- | + | выплняется | |
- | (a=a) | + | (a=a)==true --- не выполняется |
- | (a | + | (a==a)==true --- выполняется |
Чему равно значение выражения: | Чему равно значение выражения: | ||
Строка 194: | Строка 107: | ||
if true then false else chaos end = true | if true then false else chaos end = true | ||
- | if a then ~a | + | if a then ~a==chaos else false end |
a expr | a expr | ||
Строка 211: | Строка 124: | ||
Являются ли истиной лед. выражения: | Являются ли истиной лед. выражения: | ||
- | ∀ i: Int & | + | ∀ i: Int ˙ ∃ j: Int ˙ i+j=0 --- истина (при j = -i) |
- | ∀ i: Int & | + | ∀ i: Int ˙ ∃ j: Nat ˙ i+j=0 --- не удовл (нельзя найти j для полож. i) |
- | ∃ i: Int & | + | ∃ i: Int ˙ ∀ j: Int ˙ i+j=0 --- не верно |
- | Написать на RSL выражение, | + | Написать на RSL выражение, выраж. тот факт, чт нет наиб. целого числа: |
- | ~(∃ i: Int & | + | ~(∃ i: Int ˙ ∀ j: Int; ˙ (i >= j == true)) |
- | ∀ i: Int & | + | ∀ i: Int ˙ ∃ j: Int; ˙ (i >= j == true) |
- | + | Опиание функций в RSL | |
- | Прежде чем узнать описание функций, | + | Прежде чем узнать описание функций, узаем, что такое декартово произведение типов: |
Type1 × Type2 × ... × Typen | Type1 × Type2 × ... × Typen | ||
Строка 231: | Строка 144: | ||
(5, "ABC", true): Intx × Text × Bool | (5, "ABC", true): Intx × Text × Bool | ||
- | Для декартовых | + | Для декартовых произв. опр. тлько равентв и нер. |
- | + | Контанты в RSL --- частный случай функций (функ. без арг.). Функции могут задаваться: | |
- | * Явно. | + | * Явно. опис., как вычисл, или знач. |
- | * Неявно. | + | * Неявно. Накл. условия на знач. |
- | * Аксиоматически. Опис., | + | * Аксиоматически. Опис., ... |
Константы: | Константы: | ||
- | + | ''value'' | |
name : Type | name : Type | ||
Явное задание: | Явное задание: | ||
- | name: Type = val #задание | + | name: Type = val #задание знач. |
Пример: x : Int = 5 | Пример: x : Int = 5 | ||
Неявно: | Неявно: | ||
- | name : Type & | + | name : Type ˙ cond |
- | x : Int & | + | x : Int ˙ x > 0 |
- | Аксиоматически: | + | Аксиоматически: мжно исп. оба варианта |
В разделе опис. констант: x: Int | В разделе опис. констант: x: Int | ||
- | В | + | В раздее опис. аксиом: |
- | + | ''Axiom'' | |
- | x | + | x == 1 или например |
x > 0 | x > 0 | ||
Функции в RSL: | Функции в RSL: | ||
- | * Всюду | + | * Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^ |
- | ∀ x: T1 & | + | ∀ x: T1 ˙ !∃ y : T2 ˙ f(x)=y |
- | * Частично | + | * Частично выч. Для нек-рах зн. x могут иметь 0б 2 или блее знач |
- | + | ''value'' | |
name : Type → result_Type | name : Type → result_Type | ||
- | для | + | для чатично вычислимых --- трелочка с тильдой. В случае сложных типов ип. дек. произв. |
Явная спецификация: | Явная спецификация: | ||
- | + | ''value'' | |
f : Int → Int; | f : Int → Int; | ||
f(x) = x + 1 | f(x) = x + 1 | ||
p : Real стрелочка с тильдой Real | p : Real стрелочка с тильдой Real | ||
- | p(x) | + | p(x) == 1.0 |
- | + | ''pre'' x ≠ 0.0 #условия на аргумент | |
Неявная спецификация: | Неявная спецификация: | ||
- | + | ''value'' | |
f : Int → Int; | f : Int → 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 | ||
- | post ((s | + | post ((s*s=x) and (s≥0.0)) |
pre x≥0.0 | pre x≥0.0 | ||
Акс. запись: | Акс. запись: | ||
- | + | ''value'' | |
f : Int → Int; | f : Int → Int; | ||
- | + | ''axiom'' | |
- | ∀x"Int & | + | ∀x"Int ˙ f(x) == x |
- | Пример с sqrt: для | + | Пример с sqrt: для част. выч. ф-ции предусловие переносится в нач. импл. |
- | + | ''value'' | |
sqrt : Real трелочка с тильдой Real | sqrt : Real трелочка с тильдой Real | ||
- | + | ''axiom'' | |
- | ∀x:Real & | + | ∀x:Real ˙ x ≥ 0.0 ⇒ ∃s: Real ˙ sqrt(x)=s and s*s=x and s ≥ 0.0 |
Задачи: | Задачи: | ||
- | + | ''type'' | |
complex = Real × Real | complex = Real × Real | ||
Определить 0: | Определить 0: | ||
- | + | ''value'' | |
cmplx_zero: complex = (0.0, 0.0) | cmplx_zero: complex = (0.0, 0.0) | ||
Функция сложения: | Функция сложения: | ||
- | + | ''value'' | |
cmplx_add: complex × complex → complex; | cmplx_add: complex × complex → complex; | ||
- | cmplx_add((xr, xi), (yr, yi)) | + | cmplx_add((xr, xi), (yr, yi)) == (xr+yr, xi+yi) |
Функция умножения: | Функция умножения: | ||
- | + | ''value'' | |
cmplx_mul: complex × complex → complex; | cmplx_mul: complex × complex → complex; | ||
- | cmplx_mul((xr, xi), (yr, yi)) | + | cmplx_mul((xr, xi), (yr, yi)) == (xr*yr-xi*yi, xi*yr+xr*yi) |
- | Функция, | + | Функция, возвр. некое компл. число, отл. от заданного |
- | + | ''value'' | |
cmplx_another : complex → complex | cmplx_another : complex → complex | ||
cmplx_another(x) as a | cmplx_another(x) as a | ||
Строка 326: | Строка 239: | ||
{{МФСП}} | {{МФСП}} | ||
- | {{Lection-stub}} |