Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 15
Описание файла
PDF-файл из архива "Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 15 страницы из PDF
e .> ^ s,pop : Stack -~- Stackpop(s) is tl spre s ~= empty,is_empty : Stack -> Boolis_empty(s) is s = empty,top : Stack -~-> Elemtop(s) is hd spre s ~= emptyendДанная схема является уточнением схемы STACK_ALG, т.к. в ней определенывсе типы и функции из схемы STACK_ALG и справедливы все аксиомы исходнойсхемы. В качестве примера приведем доказательство справедливости аксиомы[top_push] для схемы STACK_LIST (справедливость остальных аксиом доказываетсяаналогично).[ top_push ]all e : Elem, s : Stack :top(push(e,s)) is e[[раскрыть квантор]]top(push(e,s)) is e[[раскрыть идентификатор push]]top(<.
e .> ^ s) is e[[раскрыть идентификатор top]]hd (<. e .> ^ s) is e[[вычислить hd]]e is e[[тождественное преобразование is]]true6.5.Да, вторая спецификация является уточнением первой. В качестве примераприведем доказательство справедливости третьей аксиомы (справедливостьостальных аксиом доказывается аналогично).all a : A, b : L :f1(a,b) is f2(a,b)pre f3(b) = 1[[раскрыть квантор]]if f3(b) = 1 then f1(a,b) is f2(a,b) else true end[[раскрыть идентификаторы f3,f1,f2]]if len b =1 then <. a .> ^ tl b is tl b ^ <.
a .> else true end[[вычислить tl при len b =1]]if len b =1 then <. a .> ^ <..> is <..> ^ <. a .> else true end[[вычислить ^]]if len b =1 then <. a .> is <. a .> else true end[[тождественное преобразование is]]if len b =1 then true else true end83[[вычислить if]]true7.1.type Record = = new_record(key_of : Key, data_of: Data)Эквивалентное определение:type Recordvaluenew_record : Key >< Data -> Record,key_of : Record -> Key,data_of : Record -> Dataaxiomall p : Record -> Bool :(all (k,d) : Key >< Data :-p(new_record(k,d))) => (all r : Record :- p(r)),all k : Key, d : Data :- key_of(new_record(k,d)) = k,all k : Key, d : Data :- data_of(new_record(k,d)) = d7.2.type Stack = = empty | push(top : Elem, pop : Stack)7.3.(b)type Treevalueempty : Tree,node : Tree >< Elem >< Tree -> Tree,left : Tree -~-> Tree,val : Tree -~-> Elem,rigth : Tree -~-> Treeaxiom[disjoint]all t1,t2 :Tree, e : Elem:- empty ~= node(t1,e,t2),[induction]all p : Tree -> Bool :(p(empty) /\(all t1,t2 : Tree, e : Elem:- p(t1) /\ p(t2) => p(node(t1,e,t2)))) =>(all t : Tree :- p(t)),[left_node]all t1,t2 : Tree, e : Elem:- left(node(t1,e,t2)) is t1,[val_node]all t1,t2 : Tree, e : Elem:- val(node(t1,e,t2)) is e,[right_node]all t1,t2 : Tree, e : Elem:- right(node(t1,e,t2)) is t28.1.(a)(b)(c)x := 2x := 2; 3x := 1; 38.2.(a)scheme I_STACK_EX =classtype Elemvariable st : Elem-listvalueempty : Unit -> write st Unitempty() is st := <..>,push : Elem -> write st Unitpush(e) is st := <.
e .> ^ st,pop : Unit -~-> write st Unit84pop() is st := tl stpre st ~= <..>,is_empty : Unit -> read st Boolis_empty() is st = <..>,top : Unit -~-> read st Elemtop() is hd stpre st ~= <..>end8.2.(b)scheme I_STACK_IM =classtype Elemvariable st : Elem-listvalueempty : Unit -> write st Unitempty() post st = <..>,push : Elem -> write st Unitpush(e) post st = <. e .> ^ st’,pop : Unit -~-> write st Unitpop() post st = tl st’pre st ~= <..>,is_empty : Unit -> read st Boolis_empty() as b post b = (st = <..>),top : Unit -~-> read st Elemtop() as e post e = hd stpre st ~= <..>end8.3.(a)variable result : Realvaluefract_sum : Nat -~-> write result Unitfract_sum(n) islocal variable counter : Nat := n inresult := 0.0;while counter> 0 doresult := result + 1.0 / (real counter);counter := counter – 1endendpre n > 08.4.(a) valuef : Int >< Int >< Int -> write x, y Int >< Intf(a,b,c) as (d, e)postif a = b theny = y’ /\ (if a + b > с then d = с else x = y /\ d = a + b end) /\(if с > 0 then x =c /\ d = b * с else x = x’ /\ d = b * (0 – с) end)else (x = x’ /\ y =a + b /\ d = a + b /\ e = a - b) end9.1.x := 1; (y := 1) ; (a!2) |^|x := 1; (y := 1) ; (a!3)9.2.x := 3 || a!2 || a!0 |^|x := 0 || a!3 ; a!2 |^|x := 7 ; a!(1 + b?) || a!0 |^|85x := 0 || a!7; a!(1 + b?)9.3.x := 1; y := 09.6.x := 2 || b!5 |^|x := 4 || b!3 |^|y := 1; x := 1 |^|y := 686ЛИТЕРАТУРА1.
The RAISE specification language. Prentice Hall, 1992.2. RAISE Tools Reference Manual. LACOS/CRI/DOC/13/1/V2, 1994.3 Е.А. Кузьменкова, А.К. Петренко. Формальная спецификация программ наязыке RSL (методическое пособие по практикуму), М., Изд-во АО "ДиалогМГУ", 1999.4 Е.А. Кузьменкова, А.К. Петренко. Формальная спецификация программ наязыке RSL (конспект лекций), М., Издательский отдел факультета ВМиК МГУ,2001.5 ftp://ftp.iist.unu.edu/pub/RAISE/course_material87СОДЕРЖАНИЕВВЕДЕНИЕ.................................................................................................................................... 3ГЛАВА 1. ОСНОВНЫЕ ТИПЫ ЯЗЫКА RSL. СПЕЦИФИКА RSL-ЛОГИКИ.......................5Концепция типов в языке RSL.................................................................................................
5Описание подтипов....................................................................................................................5Встроенные типы языка RSL....................................................................................................5Логика в языке RSL................................................................................................................... 6Квантифицированные и условные выражения RSL...............................................................8Упражнения ...............................................................................................................................9ГЛАВА 2.
ОПИСАНИЕ КОНСТАНТ И ФУНКЦИЙ...............................................................11Общая структура RSL спецификации....................................................................................11Декартовы произведения ( products ).....................................................................................11Выражение let...........................................................................................................................12Описание констант.................................................................................................................. 12Всюду вычислимые и частично вычислимые функции.......................................................13Явное описание функций........................................................................................................14Неявное описание функций.................................................................................................... 15Аксиоматическое описание функций ...................................................................................15Схема определения функции..................................................................................................16Упражнения..............................................................................................................................16ГЛАВА 3.
ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХСПЕЦИФИКАЦИЯХ. МНОЖЕСТВА.......................................................................................20Понятие множества................................................................................................................. 20Способы определения множеств............................................................................................20Операции над множествами...................................................................................................
21Упражнения..............................................................................................................................21ГЛАВА 4. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХСПЕЦИФИКАЦИЯХ. СПИСКИ................................................................................................24Понятие списка........................................................................................................................ 24Способы определения списков...............................................................................................24Операции над списками..........................................................................................................26Выражение case........................................................................................................................27Упражнения..............................................................................................................................28ГЛАВА 5.
ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХСПЕЦИФИКАЦИЯХ. ОТОБРАЖЕНИЯ...................................................................................30Понятие отображения..............................................................................................................30Способы определения отображений......................................................................................31Операции над отображениями................................................................................................32Упражнения..............................................................................................................................33ГЛАВА 6.
