Лекция RAISE Specification Language: базовые типы, логика, декартовы произведения, множества и операции с множествами

Август 31, 2022

Главная
Математика
Лекция RAISE Specification Language: базовые типы, логика, декартовы произведения, множества и операции с множествами

Содержание

2. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко План лекции Описания Базовые типы Логика
3. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания Типы (type) Значения (value) Переменные
4. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания типов type type_definition1, ... type_definitionn
5. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания значений value value_definition1, ... value_definitionn
6. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания переменных variable variable_definition1, ... variable_definitionn
7. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Базовые типы Bool -- {true, false}
8. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Логика (1)
9. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Логика (2)
10. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Декартовы произведения Описание типа PT1 =
11. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Множества. Свойства множеств каждый элемент встречается
12. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описание типов. Литералы и агрегаты Описание
13. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Операции с множествами inter isin ∈
14. ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Диаграмма Гогена Bool T-set Задание: Нарисуйте
16. Скачать презентацию

Слайд 2

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
План лекции
Описания
Базовые типы
Логика
Декартовы произведения
Множества.

Свойства множеств
Описание типов
Литералы и агрегаты
Операции с множествами
Диаграмма Гогена
Пример

Слайд 3

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Описания
Типы (type)
Значения (value)
Переменные (variable)
Каналы (channel)
Схемы (scheme)

Слайд 4

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Описания типов
type
type_definition1,
...
type_definitionn
Примеры
type
My_Nat =

Nat,
ST1 = T1-set
Подтипы
type
limited_text = {|t : Text :- len t > 0|}
Максимальные типы

Слайд 5

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Описания значений
value
value_definition1,
...
value_definitionn
Описание констант
value

V : Nat = 10**N
Описание функций
Всюду вычислимые функции, тотальные (total)
value
f : Int -> Nat
f (x) is
if x>0 then 1 else 0 end
Частично вычислимые функции, нетотальные
value
f : Real -~-> Real
f (x) is
1 / x
pre x ~= 0

Слайд 6

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Описания переменных
variable
variable_definition1,
...
variable_definitionn
Пример
variable
v

: Nat := 10**N,
t : Real

Слайд 7

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Базовые типы
Bool -- {true, false}
Nat --

<.0, 1, 2, ... .>
Int -- <. ... –1, 0, 1, ... .>
Real -- ... 0.0 ...
Char -- 'a', 'A', ...
Text -- "abc"
<никакого типа> -- Unit

Слайд 8

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Логика (1)

Слайд 9

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Логика (2)

Слайд 10

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Декартовы произведения
Описание типа
PT1 =

T1 >< T2 >< T3
PT2 = T1 >< (T2 >< T3)
Литералы и агрегаты
(1,2,3)
(1,(2,3))
Операции
=
~=

Слайд 11

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Множества. Свойства множеств
каждый элемент

встречается не более одного раза (не мультимножества)
не определен порядок

Слайд 12

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Описание типов. Литералы и

агрегаты

Описание типов
type
ST1 = T1-set
ST2 = {| s : ST1 :- (card s < maxset) |}
NST1 = T1-infset
Литералы и агрегаты
{1,2,3}
{}
{x : Text :- x(1) = ‘a’}

Слайд 13

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Операции с множествами
inter
isin ∈
union

∪
<< ⊂
<<= ⊆
>> ⊃
>>= ⊇
card

Слайд 14

ВМиК МГУ, сентябрь-декабрь 2001
Формальные спецификации программ-I, Лекция 3. А.К.Петренко
Диаграмма Гогена
Bool
T-set
Задание: Нарисуйте связи,

которые задают операции над множествами между этими типами данных