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

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

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 1: Строка 1:
-
Цель этих 4—5 занятий будет рассказать оcновы RSL.
+
Цель этих 4--5 занятий будет рассказать онвы RSL.
-
Практическое задание: Необходимо будет по задаче написать явную-неявную спецификацию, тестовое покрытие, тестовый драйвер и реализацию на С++, удовлетворяющую спецификации.
+
Пркт. задание: Небх. будет по здаче написать явную-неявную пецификацию, тетовое покрытие, тетовый драйвер и реализацию на С++, удовлетвряю.щую пец.
Типы данных в RSL:
Типы данных в RSL:
-
* Тип данных bool, знчения true, false, операции: ∧, ∨, ~, ⇒, =, ≠
+
* Тип данных bool, знчения true, false, перации: and, or, ~, =>, =, !=
-
* Int +, −, ×, /, \, ↑, abs, real
+
* Int +-*/ \ uparr, 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.
-
(по гор. второй операнд, по верт. — первый)
+
(по гор. второй операнд, по верт. --- первый)
-
<table cellpadding="10"><tr><td>
+
and T F C
-
{|border="1"
+
T T F C
-
!&and;
+
F F F F
-
!T
+
C C C C
-
!F
+
-
!C
+
-
|-
+
-
!T
+
-
|T
+
-
|F
+
-
|C
+
-
|-
+
-
!F
+
-
|F
+
-
|F
+
-
|F
+
-
|-
+
-
!C
+
-
|C
+
-
|C
+
-
|C
+
-
|}
+
-
</td><td>
+
-
{|border="1"
+
-
!&or;
+
-
!T
+
-
!F
+
-
!C
+
-
|-
+
-
!T
+
-
|T
+
-
|T
+
-
|T
+
-
|-
+
-
!F
+
-
|T
+
-
|F
+
-
|C
+
-
|-
+
-
!C
+
-
|C
+
-
|C
+
-
|C
+
-
|}
+
-
</td><td>
+
-
{|border="1"
+
-
!&rArr;
+
-
!T
+
-
!F
+
-
!C
+
-
|-
+
-
!T
+
-
|T
+
-
|F
+
-
|C
+
-
|-
+
-
!F
+
-
|T
+
-
|T
+
-
|T
+
-
|-
+
-
!C
+
-
|C
+
-
|C
+
-
|C
+
-
|}
+
-
</td><td>
+
-
{|border="1"
+
-
!=
+
-
!a
+
-
!b
+
-
!C
+
-
|-
+
-
!a
+
-
|T
+
-
|F
+
-
|C
+
-
|-
+
-
!b
+
-
|F
+
-
|T
+
-
|C
+
-
|-
+
-
!C
+
-
|C
+
-
|C
+
-
|C
+
-
|}
+
-
</td><td>
+
-
{|border="1"
+
-
!&equiv;
+
-
!a
+
-
!b
+
-
!C
+
-
|-
+
-
!a
+
-
|T
+
-
|F
+
-
|F
+
-
|-
+
-
!b
+
-
|F
+
-
|T
+
-
|F
+
-
|-
+
-
!C
+
-
|F
+
-
|F
+
-
|T
+
-
|}
+
-
</td></tr></table>
+
-
Для описания альтернатив используется if-then-else:
+
or T F C
 +
T T T T
 +
F T F C
 +
C C C C
-
'''if''' expr1 '''then''' expr2 '''else''' expr3 '''end'''
+
=> 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'' true ''then'' expr2 ''else'' expr3 ''end'' = expr2
-
'''if''' false '''then''' expr2 '''else''' expr3 '''end''' = expr3
+
''if'' false ''then'' expr2 ''else'' expr3 ''end'' = expr3
-
'''if''' chaos '''then''' expr2 '''else''' expr3 '''end''' = chaos
+
''if'' chaos ''then'' expr2 ''else'' expr3 ''end'' = chaos
-
'''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 [true/a]''else'' expr3[false/a] ''end'' = expr2
-
В RSL, как и в обычном матлоге, используются кванторы &exist;, &forall;, !&exist;.
+
В RSL, как и в бычном матлоге, исп. кванторы &exist;, &forall;, !&exist;.
-
Задачи. Будут выписываться тождества обычной логики, нужно проверить, работает ли оно в RSL:
+
Задачи. Будут выпис. тождества обычной логики, нужно прверить, работает ли оно в RSL:
-
~~a &equiv; a — выполняется
+
~~a == a --- выполняетя
-
true or a &equiv; true — выполняется
+
true or a == true --- выполняется
-
a or true &equiv; true — не выполняется (если подставить chaos)
+
a or true == true --- не выполняется (если подставить chaos)
-
a => true &equiv; true — не выполняется
+
a => true == true --- не выполняется
-
a => b &equiv; ~a or b
+
a => b == ~a or b
-
a => b &equiv; ~a or b T F C
+
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 &equiv; true — не выполняется
+
a or ~a == true --- не выполняется
-
a and ~a &equiv; false — не выполняется
+
a and ~a == false --- не выполняется
-
a and b and c &equiv; a and (b and c)
+
a and b and c == a and (b and c)
-
a = chaos: chaos &equiv; chaos = true
+
a = chaos: chaos == chaos = true
-
a = false: false &equiv; false = true
+
a = false: false == false = true
-
a = true: b = chaos: chaos &equiv; chaos = true
+
a = true: b = chaos: chaos == chaos = true
-
b = false: false &equiv; false = true
+
b = false: false == false = true
-
b = true: c &equiv; c = true
+
b = true: c == c = true
-
— выполняется
+
выполняется
-
a or b or c &equiv; a or (b or c)
+
a or b or c == a or (b or c)
-
a = chaos: chaos &equiv; chaos = true
+
a = chaos: chaos == chaos = true
-
a = true: truee &equiv; true = true
+
a = true: truee == true = true
-
a = false: b = chaos: chaos &equiv; chaos = true
+
a = false: b = chaos: chaos == chaos = true
-
b = true: true &equiv; true = true
+
b = true: true == true = true
-
b = false: c &equiv; c = true
+
b = false: c == c = true
-
— выполняется
+
выплняется
-
(a=a)&equiv;true — не выполняется
+
(a=a)==true --- не выполняется
-
(a&equiv;a)&equiv;true — выполняется
+
(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&equiv;chaos else false end
+
if a then ~a==chaos else false end
a expr
a expr
Строка 211: Строка 124:
Являются ли истиной лед. выражения:
Являются ли истиной лед. выражения:
-
&forall; i: Int &bull; &exist; j: Int &bull; i+j=0 — истина (при j = -i)
+
&forall; i: Int &dot; &exist; j: Int &dot; i+j=0 --- истина (при j = -i)
-
&forall; i: Int &bull; &exist; j: Nat &bull; i+j=0 — не удовл (нельзя найти j для положительного i)
+
&forall; i: Int &dot; &exist; j: Nat &dot; i+j=0 --- не удовл (нельзя найти j для полож. i)
-
&exist; i: Int &bull; &forall; j: Int &bull; i+j=0 — не верно
+
&exist; i: Int &dot; &forall; j: Int &dot; i+j=0 --- не верно
-
Написать на RSL выражение, выражающее тот факт, что нет наиболее целого числа:
+
Написать на RSL выражение, выраж. тот факт, чт нет наиб. целого числа:
-
~(&exist; i: Int &bull; &forall; j: Int; &bull; (i >= j &equiv; true))
+
~(&exist; i: Int &dot; &forall; j: Int; &dot; (i >= j == true))
-
&forall; i: Int &bull; &exist; j: Int; &bull; (i >= j &equiv; true)
+
&forall; i: Int &dot; &exist; j: Int; &dot; (i >= j == true)
-
== Описание функций в RSL ==
+
Опиание функций в RSL
-
Прежде чем узнать описание функций, узнаем, что такое декартово произведение типов:
+
Прежде чем узнать описание функций, узаем, что такое декартово произведение типов:
Type1 &times; Type2 &times; ... &times; Typen
Type1 &times; Type2 &times; ... &times; Typen
Строка 231: Строка 144:
(5, "ABC", true): Intx &times; Text &times; Bool
(5, "ABC", true): Intx &times; Text &times; Bool
-
Для декартовых произведений определено только равенство и неравенство
+
Для декартовых произв. опр. тлько равентв и нер.
-
Константы в RSL — частный случай функций (функции без аргументов). Функции могут задаваться:
+
Контанты в RSL --- частный случай функций (функ. без арг.). Функции могут задаваться:
-
* Явно. описание, как вычисляется, или знач.
+
* Явно. опис., как вычисл, или знач.
-
* Неявно. Накладываются условия на значения.
+
* Неявно. Накл. условия на знач.
-
* Аксиоматически. Опис., …
+
* Аксиоматически. Опис., ...
Константы:
Константы:
-
'''value'''
+
''value''
name : Type
name : Type
Явное задание:
Явное задание:
-
name: Type = val #задание значения
+
name: Type = val #задание знач.
Пример: x : Int = 5
Пример: x : Int = 5
Неявно:
Неявно:
-
name : Type &bull; cond
+
name : Type &dot; cond
-
x : Int &bull; x > 0
+
x : Int &dot; x > 0
-
Аксиоматически: можно использовать оба варианта
+
Аксиоматически: мжно исп. оба варианта
В разделе опис. констант: x: Int
В разделе опис. констант: x: Int
-
В разделе опис. аксиом:
+
В раздее опис. аксиом:
-
'''Axiom'''
+
''Axiom''
-
x &equiv; 1 или например
+
x == 1 или например
x > 0
x > 0
Функции в 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 &dot; !&exist; y : T2 &dot; f(x)=y
-
* Частично вычислимые. Для некоторых значений x могут иметь 0, 2 или более значений
+
* Частично выч. Для нек-рах зн. x могут иметь 0б 2 или блее знач
-
'''value'''
+
''value''
name : Type &rarr; result_Type
name : Type &rarr; result_Type
-
для частично вычислимых — стрелочка с тильдой. В случае сложных типов используется декартово произведение
+
для чатично вычислимых --- трелочка с тильдой. В случае сложных типов ип. дек. произв.
Явная спецификация:
Явная спецификация:
-
'''value'''
+
''value''
f : Int &rarr; Int;
f : Int &rarr; Int;
f(x) = x + 1
f(x) = x + 1
p : Real стрелочка с тильдой Real
p : Real стрелочка с тильдой Real
-
p(x) &equiv; 1.0
+
p(x) == 1.0
-
'''pre''' x &ne; 0.0 #условия на аргумент
+
''pre'' x &ne; 0.0 #условия на аргумент
Неявная спецификация:
Неявная спецификация:
-
'''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
-
post ((s&times;s=x) and (s&ge;0.0))
+
post ((s*s=x) and (s&ge;0.0))
pre x&ge;0.0
pre x&ge;0.0
Акс. запись:
Акс. запись:
-
'''value'''
+
''value''
f : Int &rarr; Int;
f : Int &rarr; Int;
-
'''axiom'''
+
''axiom''
-
&forall;x"Int &bull; f(x) &equiv; x
+
&forall;x"Int &dot; f(x) == x
-
Пример с sqrt: для частично вычислимой функции предусловие переносится в начало импликации.
+
Пример с sqrt: для част. выч. ф-ции предусловие переносится в нач. импл.
-
'''value'''
+
''value''
sqrt : Real трелочка с тильдой Real
sqrt : Real трелочка с тильдой Real
-
'''axiom'''
+
''axiom''
-
&forall;x:Real &bull; x &ge; 0.0 &rArr; &exist;s: Real &bull; sqrt(x)=s and s&times;s=x and s &ge; 0.0
+
&forall;x:Real &dot; x &ge; 0.0 &rArr; &exist;s: Real &dot; sqrt(x)=s and s*s=x and s &ge; 0.0
Задачи:
Задачи:
-
'''type'''
+
''type''
complex = Real &times; Real
complex = Real &times; Real
Определить 0:
Определить 0:
-
'''value'''
+
''value''
cmplx_zero: complex = (0.0, 0.0)
cmplx_zero: complex = (0.0, 0.0)
Функция сложения:
Функция сложения:
-
'''value'''
+
''value''
cmplx_add: complex &times; complex &rarr; complex;
cmplx_add: complex &times; complex &rarr; complex;
-
cmplx_add((xr, xi), (yr, yi)) &equiv; (xr+yr, xi+yi)
+
cmplx_add((xr, xi), (yr, yi)) == (xr+yr, xi+yi)
Функция умножения:
Функция умножения:
-
'''value'''
+
''value''
cmplx_mul: complex &times; complex &rarr; complex;
cmplx_mul: complex &times; complex &rarr; complex;
-
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)) == (xr*yr-xi*yi, xi*yr+xr*yi)
-
Функция, возвращающая некое комплексное число, отличное от заданного
+
Функция, возвр. некое компл. число, отл. от заданного
-
'''value'''
+
''value''
cmplx_another : complex &rarr; complex
cmplx_another : complex &rarr; complex
cmplx_another(x) as a
cmplx_another(x) as a
Строка 326: Строка 239:
{{МФСП}}
{{МФСП}}
-
{{Lection-stub}}
 

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!


Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_02_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_08_%D1%81%D0%B5%D0%BD%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы