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

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

Версия от 20:51, 30 сентября 2010; 212.192.253.132 (Обсуждение)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

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

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

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

Типы данных в RSL:
* Тип данных bool, знчения true, false, операции: &and;, &or;, ~, &rArr;, =, &ne;
* Int +, &minus;, &times;, /, \, &uarr;, abs, real
* Nat {|I=Int, i > 0|}
* Real. Всегда должны присутствовать точка и одна цифра после точки. +, &minus;, &times;, /, abs, int (сиречь trunc)
* Char 'A'...'Z'
* Text — посл. символов
* Unit. Единственное значение, использующееся для функций без параметров

== Логика в RSL ==

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

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

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

<table cellpadding="10"><tr><td>
{|border="1"
 !&and;
 !T
 !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:

'''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 [<math>\frac{true}{a}</math>]'''else''' expr3[false/a] '''end''' = expr2

В RSL, как и в обычном матлоге, используются кванторы &exist;, &forall;, !&exist;.

Задачи. Будут выписываться тождества обычной логики, нужно проверить, работает ли оно в RSL:

~~a &equiv; a — выполняется

true or a &equiv; true — выполняется

a or true &equiv; true — не выполняется (если подставить chaos)

a => true &equiv; true — не выполняется

a => b &equiv; ~a or b

a => b &equiv; ~a or b T F C
                 T T T T
                 F T T T
                 C T T T
— выполняетя

a or ~a &equiv; true — не выполняется

a and ~a &equiv; false — не выполняется

a and b and c &equiv; a and (b and c)
 a = chaos: chaos &equiv; chaos = true
 a = false: false &equiv; false = true
 a = true:  b = chaos: chaos &equiv; chaos = true
            b = false: false &equiv; false = true
            b = true:  c &equiv; c = true
— выполняется

a or b or c &equiv; a or (b or c)
 a = chaos: chaos &equiv; chaos = true
 a = true:  truee &equiv; true = true
 a = false: b = chaos: chaos &equiv; chaos = true
            b = true:  true &equiv; true = true
            b = false: c &equiv; c = true
— выполняется

(a=a)&equiv;true — не выполняется

(a&equiv;a)&equiv;true — выполняется

Чему равно значение выражения:

if true then false else chaos end = true

if a then ~a&equiv;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

Являются ли истиной лед. выражения:

&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)

&exist; i: Int &bull; &forall; j: Int &bull; i+j=0 — не верно

Написать на RSL выражение, выражающее тот факт, что нет наиболее целого числа:

~(&exist; i: Int &bull; &forall; j: Int; &bull; (i >= j &equiv; true))

&forall; i: Int &bull; &exist; j: Int; &bull; (i >= j &equiv; true)

== Описание функций в RSL ==

Прежде чем узнать описание функций, узнаем, что такое декартово произведение типов:

Type1 &times; Type2 &times; ... &times; Typen

(5, "ABC", true): Intx &times; Text &times; Bool

Для декартовых произведений определено только равенство и неравенство

Константы в RSL — частный случай функций (функции без аргументов).  Функции могут задаваться:
* Явно. описание, как вычисляется, или знач.
* Неявно. Накладываются условия на значения.
* Аксиоматически. Опис., ...

Константы: 
 '''value'''
   name : Type

Явное задание:
 name: Type = val #задание знач.

Пример: x : Int = 5

Неявно:
 name : Type &bull; cond
 x : Int &bull; x > 0

Аксиоматически: можно исп. оба варианта
 В разделе опис. констант: x: Int
 В разделе опис. аксиом:
 '''Axiom'''
   x &equiv; 1 или например
   x > 0

Функции в RSL:
* Всюду выч. Для любого x из бл. пр. сущ. единст. y, таке что f(x) = y^
 &forall; x: T1 &bull; !&exist; y : T2 &bull; f(x)=y
* Частично выч. Для нек-рах зн. x могут иметь 0, 2 или более значений

'''value'''
   name : Type &rarr; result_Type

для частично вычислимых — стрелочка с тильдой. В случае сложных типов используется декартово произведение

Явная спецификация:
 '''value''' 
   f : Int &rarr; Int;
   f(x) = x + 1

p : Real стрелочка с тильдой Real
   p(x) &equiv; 1.0
   '''pre''' x &ne; 0.0 #условия на аргумент

Неявная спецификация:
 '''value''' 
   f : Int &rarr; Int;
   f(x) as r /* определение новой переменной, связанной с значением функции */
   post r>x /* постусловие, связывающее аргументы и значения функции */

Пример пис. квадратного корня:
   sqrt : Real трелочка с тильдой Real
   sqrt(x) as s
   post ((s&times;s=x) and (s&ge;0.0))
   pre x&ge;0.0

Акс. запись:
 '''value''' 
   f : Int &rarr; Int;
 '''axiom'''
   &forall;x"Int &bull; f(x) &equiv; x

Пример с sqrt: для частично вычислимой функции предусловие переносится в начало импл.
 '''value''' 
   sqrt : Real трелочка с тильдой Real
 '''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

Задачи:
 '''type'''
   complex = Real &times; Real

Определить 0:
 '''value'''
   cmplx_zero: complex = (0.0, 0.0)

Функция сложения:
 '''value'''
   cmplx_add: complex &times; complex &rarr; complex;
   cmplx_add((xr, xi), (yr, yi)) &equiv; (xr+yr, xi+yi)

Функция умножения:
 '''value'''
   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)

Функция, возвращающая некое комплексное число, отличное от заданного
 '''value'''
   cmplx_another : complex &rarr; complex
   cmplx_another(x) as a
   post a &ne; x

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. 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