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

Презентация:



Advertisements
Похожие презентации
Лекция RAISE Specification Language: списки и операции со списками.
Advertisements

Лекция RAISE Development Method: некоторые виды спецификаций и проверка согласованности моделей.
Лекция Виды формальных спецификаций. Практические задачи курса.
Лекция Неполная спецификация и недетерминизм. Let- и Case-выражения.
Тема: Множества.. Множество – совокупность однотипных элементов, рассматриваемых как единое целое. Примеры множеств: [ 3, 4, 7, 9, 12] [ ] [ a,
Денотационная семантика 0 |1|1 | 0 | 1 Mb:Mb: М b ('0') = 0, М b ('1')=1 М b ( '0') = =2 * М b ( ) М b ( 1) = =2 * М b ( ) + 1.
Часть II. Формальное описание языков программирования ( Формальная спецификация формальных языков ) Приложение. Атрибутная грамматика языка IMP.
3. Математические основы 3.3. Матиндукция 5. Построение языка предикатного программирования. Методы доказательства корректности предикатных программ Методы.
1 Кубенский А.А. Функциональное программирование. Глава 2. Средства функционального программирования. Потоки. «Завязывание узлов» Часто обработку данных.
Множественный тип данных 1. Вычислить значения отношений или указать, что они ошибочны. а)[2][2, 2, 2] б)['a', 'b']=['b', 'а'] в)[4, 5, 6]=[4..б] г)['с',
1 Лекция 13 ОСНОВНЫЕ ПОНЯТИЯ ЯЗЫКА Visual Basic For Applications (VBA) План лекции Типы данных VBA Операции над данными VBA Описание типов данных VBA Имена.
Функции. Функция- это подпрограмма, которая вычисляет и возвращает некоторое значение. Функции описываются в разделе описаний следующим образом: Function.
1 Кубенский А.А. Функциональное программирование. Глава 5. Системы исполнения функциональных программ. Глава 5. Системы исполнения функциональных программ.
Множества. Множество- ограниченный, неупорядоченный набор различных элементов одного типа. Примеры множеств: Множество арабских цифр. Множество знаков.
Условный оператор IF и оператор выбора CASE Turbo Pascal.
Часть II. Формальное описание языков программирования ( Формальная спецификация формальных языков ) Приложение. Операционная семантика языка SIL.
«Программирование с использованием множеств» Delphi. Тема 8:
Семантический анализ КC-грамматики, с помощью которых описывают синтаксис языков программирования, не позволяют задавать контекстные условия (КУ), имеющиеся.
Алгоритмизация и программирование Программирование. Основные алгоритмы и приемы программирования. (на примере языка программирования Turbo Pascal) Дибиров.
Логический тип данных. Логические выражения. Условный оператор.
Транксрипт:

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

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

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

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания типов type type_definition 1,... type_definition n Примеры type My_Nat = Nat, ST1 = T1-set Подтипы type limited_text = {|t : Text :- len t > 0|} Максимальные типы

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания значений value value_definition 1,... value_definition n Описание констант 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

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описания переменных variable variable_definition 1,... variable_definition n Пример variable v : Nat := 10**N, t : Real

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

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

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

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

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

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Описание типов. Литералы и агрегаты Описание типов type ST1 = T1-set ST2 = {| s : ST1 :- (card s < maxset) |} NST1 = T1-infset Литералы и агрегаты {1,2,3} {} {x : Text :- x(1) = a}

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

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

ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 3. А.К.Петренко Пример: SET_DATABASE SET-DATABASE = class type Record = Key >< Data, Database = {( rs : Record-set is_wf_Database(rs) )}, Key, Data value is_wf_Database : Record-set -> Bool is_wf_Database(rs) is ( k : Key, d1,d2 : Data ((k,d1) d1 = d2), empty : Database is {}, insert : Key > Database insert(k,d,db) is remove(k,db) U {(k,d)}, remove : Key > Database remove(k,db) is db \ {(k,d) ) d : Data true}, defined : Key > Bool defined(k,db) is ( d : Data. (k.d) db), lookup : Key > Data lookup(k,db) as d post (k,d) db pre defined(k,db) end