Презентация "базовые типы, логика, декартовы произведени" по математике – проект, доклад

Лекция

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

ВМиК МГУ, сентябрь-декабрь 2001

Формальные спецификации программ-I, Лекция 3. А.К.Петренко

План лекции

Описания Базовые типы Логика Декартовы произведения Множества. Свойства множеств Описание типов Литералы и агрегаты Операции с множествами Диаграмма Гогена Пример

Описания

Типы (type) Значения (value) Переменные (variable) Каналы (channel) Схемы (scheme)

Описания типов

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

Описания значений

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

Описания переменных

variable variable_definition1, ... variable_definitionn Пример variable v : Nat := 10**N, t : Real

Базовые типы

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

Логика (1)

Логика (2)

Декартовы произведения

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

Множества. Свойства множеств

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

Описание типов. Литералы и агрегаты

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

Операции с множествами

inter isin  union  <<  <<=  >>  >>=  card

Диаграмма Гогена Bool T-set

Задание: Нарисуйте связи, которые задают операции над множествами между этими типами данных

Пример: 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) <= rs /\ (k,d2) <= rs) => d1 = d2), empty : Database is {}, insert : Key >< Data >< Database -> Database insert(k,d,db) is remove(k,db) U {(k,d)}, remove : Key >< Database -> Database remove(k,db) is db \ {(k,d) ) d : Data • true}, defined : Key >< Database -> Bool defined(k,db) is ( d : Data. (k.d)  db), lookup : Key >< Database -> Data lookup(k,db) as d post (k,d) db pre defined(k,db) end