Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 14

Рассмотреть возможные варианты результатов вычислений в предположении,что все возможные обмены сообщениями произошли(( (x:=a?+1) || ( x:=b?) )|=|( (x:=c?+1) )|=|(y:=b?+a?) )|| a!0 || b!2Решение:((x:=1) || (x:=2)) |^| (y:=2)4. Дано определение вариантного типа:typeCollection == empty | atom (head:Elem) | list(head : Collection), ElemДать эквивалентное определение без использования вариантных определений.Решение:type Elem, Collectionvalue empty : Collection,atom : Elem -> Collection,list : Collection -> Collection,head : Collection -~-> Collection,head : Collection -~-> Elemaxiom[disjoint]all c ; Collection, e ; Elem :empty ~= atom(e) /\ empty~=list(c) /\ atom ( e ) ~= list ( c)[induction]all Elem, isCollection ; Collection -> Bool :isCollection(empty) /\ (all c : Collection, e ; Elem :isCollection (atom(e)) /\(isCollection(c) => isCollection(list(c)) )) =>(all c : Collection :- isCollection ( c ))[head_list]all c : Collection :- head (list(c)) is c[head_atom]75all e : Elem :- head (atom(e)) is e76ОТВЕТЫ И РЕШЕНИЯ К УПРАЖНЕНИЯМ1.1.(b)type ST = {| n : Int:- n \ 2 = 1 |}1.2.(a)(b)(c)(d)(e)(f)(g)(h)(i)(j)(k)даданетнетданетнетдаданетда1.3.(a)(b)afalse (по свойству (1))Решение: if a then ∼( a is chaos) else false end ≡ (по свойству (3))if a then ∼( true is chaos) else false end ≡if a then true else false end ≡ (по свойству (3))if a then a else a end ≡ a1.4.(a) да (для данного i выбираем j = −i)(b) нет (не верно, например, для i > 0)(c) нет1.5.(a)(d)all i : Int :- exists j : Int :- j > iexists k : Nat :-n = k * k2.1.(a)type Points = {| (x, y) : Real >< Real :- x >= 0 /\ y >= 0 /\ y >= x |}2.2.(a)is_even : Nat -> Boolis_even(n) is (exists m : Nat :- n = 2 ∗ m)или∼(exists i : Int :- all j : Int :- i >= j)или альтернативное определение:is_even : Nat -> Boolis_even(n) is n \ 2 = 02.3.(a)(b)(c)2.4.(a)(b)(c)valuemax : Int >< Int -> Intmax(i, j) is if i >= j then i else j endvaluemax : Int >< Int -> Intmax(i, j) as ypost (y = i /\ y >= j) \/ (y = j /\ y >= i)valuemax : Int >< Int -> Intaxiomall i,j : Int :- max(i, j) is if i >= j then i else j endtype Complex = Real >< Realvalue zero : Complex = (0.0,0.0)value c : Complex :- let (x, y) = c in x = y end77(d)(e)2.5.(a)(b)valueadd : Complex >< Complex -> Complexadd((x1,y1), (x2,y2)) is (x1 + x2, y1 + y2),mult : Complex >< Complex -> Complexmult((x1,y1), (x2,y2)) is (x1 ∗ x2 − y1 ∗ y2, x1 ∗ y2 + y1 ∗ x2)valuef : Complex -> Complexf(c1) as c2 post c1 ~= c2typeCircle = Center >< Radius,Center = Position,Radius = {| r : Real :- r >= 0.0 |}valueon_circle : Circle >< Position -> Boolon_circle((c,r), p) is distance(c, p) = rили альтернативное определение:(c)(d)valueon_circle : Circle >< Position -> Boolon_circle(circ, p) islet(c,r) = circindistance(c,p) = rendvaluecircle : Circle = (origin, 3.0)valuepos : Position :- on_circle(circle, pos)2.7.valueapprox_sqrt : Real >< Real -∼-> Realapprox_sqrt(x, eps) as spost s ** 2.0 <= x /\ x < (s + eps) ** 2.0pre x >= 0.0 /\ eps > 0.02.8.(b)3.1.(a) {1, 3, 5, 7, 9} или {s | s : Nat :- (s \ 2 = 1) /\ (s < 10) }или {2 * n + 1 | n : Nat :- n <= 4 }(b) {2, 3, 5, 7, 11, 13, 17, 19} илиvalueF2 : Nat >< Nat >< Nat -> Nat >< NatF2(a, b, c) as (v, w)postif a + b > c then v = c else v = a + b end /\if с > 0 then w = a * b * c else w = a * b * (0 –c) end{n | n : Nat :- is_a_prime(n) /\ n < 20 },is_a_prime : Nat -> Boolis_a_prime(n) is (all k : Nat :- (k < n /\ k > 1) => n \ k ~= 0)3.2.card { n | n : Nat :- 30 \ n = 0} = card {1, 2, 3, 5, 6, 10, 15, 30} = 83.3.card { (x, y) | x, y : Int :- x * x + y * y < 25 }783.4.(a)valuemax : Int-set -~-> Intmax(s) as mpostm isin s /\ (all k : Int :- k isin s => k <= m)pre s ~= { }3.5.(a)schemeUNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfo = Course >< Student-set,University = {| (ss, cis) : Student-set >< CourseInfo-set :- is_wf(ss, cis) |}value/∗ is_wf осуществляет проверку на «хорошо сформированную» базу данных,проверяя выполнение свойства уникальности курса ∗/is_wf :- Student-set >< CourseInfo-set -> Boolis_wf(ss, cis) is (all (c, ss1), (c1, ss2) : CourseInfo :(c, ss1) isin cis /\ (c1, ss2) isin cis => (с = с1 = > ss1 = ss2)),/* hasStudent проверяет, учится ли данный студент в указанномуниверситете */hasStudent : Student >< University -> BoolhasStudent(s, (ss, cis)) is s isin ss,/∗ hasCourse проверяет, читается ли данный курс в указанном университете*/hasCourse : Course >< University -> BoolhasCourse(c, (ss, cis)) is(exists (c1, ss1) : CourseInfo :- (c1, ss1) isin cis /\ c = c1),/∗ studOf возвращает множество студентов заданного университета,посещающих указанный курс ∗/studOf : Course >< University -~-> Student-setstudOf(c, (ss, cis)) is{s | s : Student :- exists ss1 : Student-set :- s isin ss1 /\ (c, ss1) isin cis}pre hasCourse(c, (ss, cis)),/∗ attending возвращает множество курсов, которые посещает данныйстудент в указанном университете ∗/attending : Student >< University -~-> Course-setattending(s, (ss, cis)) is{c | c : Course :- exists ss1 : Student-set :- (c, ss1) isin cis /\ s isin ss1}pre hasStudent(s, (ss, cis)),/∗ newStud добавляет нового студента к числу студентов заданногоуниверситета ∗/newStud : Student >< University -~-> UniversitynewStud(s, (ss, cis)) is (ss union {s}, cis)pre ~hasStudent(s, (ss, cis)),/∗ dropStud исключает указанного студента из числа студентов заданногоуниверситета ∗/dropStud : Student >< University -~-> UniversitydropStud(s, (ss, cis)) is(ss \ {s}, {(c, ss1 \ {s}) | (c, ss1) : CourseInfo :- (c, ss1) isin cis})pre hasStudent(s, (ss, cis)),79/∗ newCourse добавляет новый курс с пустым множеством студентов к числукурсов заданного университета ∗/newCourse : Course >< University -~-> UniversitynewCourse(c, (ss, cis)) is (ss, cis union {(c, {})})pre ~hasCourse(c, (ss, cis)),/∗ delCourse удаляет указанный курс из числа курсов заданногоуниверситета ∗/delCourse : Course >< University -~-> UniversitydelCourse(c, (ss, cis)) is (ss, cis \ {(c, ss1) | ss1 : Student-set :- true})pre hasCourse(c, (ss, cis))end(b) valuestudOf : Course >< University -~-> Student-setstudOf(c, (ss, cis)) as ss1post (c, ss1) isin cispre hasCourse(c, (ss, cis))4.1(a)(b)169chaos4.2.(a)<.2,4,6,8,10,12,14,16,.> или <.2 * n | n in <.1..8.>.><.1,4,9,16,25,36,49,64,81,100.> или<.n | n in <.1..100.> :- exists k : Nat :-n = k * k.>(b)4.3.valueFib_numbers : Nat-inflistaxiomFib_numbers(1) = 1,Fib_numbers(2) = 1,all i : Nat :- i > 2 =>Fib_numbers(i) = Fib_numbers(i - 2) + Fib_numbers(i - 2)Искомый список <.n | n in Fib_numbers :- n <= 1000.>4.4.valueis_sorted : Int-list -> Boolaxiomall L : Int-list :is_sorted(L) is(all i1, i2 : Nat :- {i1, i2} <<= inds L /\ i1 < i2 => L(i1) < L(i2))4.5.type Elemvalue(a) length : Elem-list -> Natlength(k) is if k = <..> then 0 else 1 + length(tl k) endилиlength : Elem-list -> Natlength(k) is card (inds k)илиlength : Elem-list -> Natlength(k) iscase k of<..> -> 0,<.i.> ^ lr -> length(lr) + 1end(b) rev : Elem-list -> Elem-list80rev(k) is if k = <..> then <..> else rev(tl k) ^ <.hd k.> endилиrev : Elem-list -> Elem-listrev(k) is <.k(len k − i + 1) | i in <.1 ..

len k.>.>(c) del : Elem-list >< Elem-> Elem-listdel(k, e) iscase k of<..> -> <..>,<.i.> ^ lr -> if i = e then del(lr, e)else <.i.> ^ del(lr, e) endendилиdel : Elem-list >< Elem-> Elem-listdel(k, e) is <.x | x in k :- x ~= e.>(d) number_of : Elem-list >< Elem-> Natnumber_of(k, e) is card {i | i : Nat :- i isin inds k /\ k(i) = e}4.7.schemePAGE =classtype Page = Line-list, Line = Word-list, Wordvalueis_on : Word >< Page -> Boolis_on(w, p) is (exists i : Nat :- i isin inds p /\ w isin elems p(i)),number_of : Word >< Page -> Natnumber_of(w, p) iscard {(i, j) | i,j : Nat :- i isin inds p /\ j isin inds p(i) /\ w = p(i)(j)}end5.1.(b)(c)(d)5.2.[(n, k) +> n \ k | n, k : Nat :- (n <= 50) /\ (k > 1) /\ (k < n)][n +> {k | k : Nat :- n \ k = 0 /\ k <= n /\ k >= 1} | n : Nat :- n <= 20][n +> m | n, m : Nat :- exists k : Nat :k * k = m /\ m <= n /\ (k + 1) * (k + 1) > n]schemeMAP_UNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfos = Course -m-> Student-set,University = Student-set >< CourseInfosvalue/* hasStudent проверяет, учится ли данный студент в указанномуниверситете */hasStudent : Student >< University -> BoolhasStudent(s, (ss, cis)) is s isin ss,/∗ hasCourse проверяет, читается ли данный курс в указанном университете*/hasCourse : Course >< University -> BoolhasCourse(c, (ss, cis)) is c isin dom cis,/∗ studOf возвращает множество студентов заданного университета,посещающих указанный курс ∗/studOf : Course >< University -~-> Student-setstudOf(c, (ss, cis)) is cis(c)81pre hasCourse(c, (ss, cis)),/∗ attending возвращает множество курсов, которые посещает данныйстудент в указанном университете ∗/attending : Student >< University -~-> Course-setattending(s, (ss, cis)) is{c | c : Course :- c isin dom cis /\ s isin cis(c)}pre hasStudent(s, (ss, cis)),/∗ newStud добавляет нового студента к числу студентов заданногоуниверситета ∗/newStud : Student >< University -~-> UniversitynewStud(s, (ss, cis)) is (ss union {s}, cis)pre ~hasStudent(s, (ss, cis)),/∗ dropStud исключает указанного студента из числа студентов заданногоуниверситета ∗/dropStud : Student >< University -~-> UniversitydropStud(s, (ss, cis)) is(ss \ {s}, [ c +> cis(c) \ {s} | c : Course :- c isin dom cis ])pre hasStudent(s, (ss, cis)),/∗ newCourse добавляет новый курс с пустым множеством студентов к числукурсов заданного университета ∗/newCourse : Course >< University -~-> UniversitynewCourse(c, (ss, cis)) is (ss, cis !! [c +> {}])pre ~hasCourse(c, (ss, cis)),/∗ delCourse удаляет указанный курс из числа курсов заданногоуниверситета ∗/delCourse : Course >< University -~-> UniversitydelCourse(c, (ss, cis)) is (ss, cis \ {c})pre hasCourse(c, (ss, cis))end6.1.schemeSTACK_ALG =classtype Elem, Stackvalueempty : Stack,push : Elem >< Stack -> Stack,pop : Stack -~- Stack,is_empty : Stack -> Bool,top : Stack -~-> Elemaxiom[ is_empty_empty ]is_empty(empty) is true,[ is_empty_push ]all e : Elem, s : Stack :is_empty(push(e,s)) is false,[ top_push ]all e : Elem, s : Stack :top(push(e,s)) is e,[ pop_push ]all e : Elem, s : Stack :pop(push(e,s)) is send826.3.schemeSTACK_LIST =classtype Elem, Stack = Elem-listvalueempty : Stack = <..>,push : Elem >< Stack -> Stackpush(e,s) is <.