create : Unit -> S

create () is <..>,

push_down : E >< S -> S

push_down (e,s) is <. <. E .> .> ^ S,

push_right : E >< S -> S

push_right (e,s) is if s = <..> then <. <. e .> .>

else <. <. e .> ^ hd s .> ^ tl s

end,

pop_up S -~-> S

pop_up (s) is tl s

pre s ~= <..>,

pop_left : S -~-> S

pop_left (s) is <. tl hd s .> ^ tl s

pre s~= <..> /\ hd s~=<..>,

get : S -~-> E

get (s) is hd hd s

pre s~ ~= <..> /\ hd s~ ~= <..>

3. Рассмотреть возможные варианты результатов вычислений в предположении, что все возможные обмены сообщениями произошли

( ( (x:=a?+1) || ( x:=b?) )

|=|

( (x:=c?+1) )

|=|

(y:=b?+a?) )

|| a!0 || b!2

Решение:

((x:=1) || (x:=2)) |^| (y:=2)

4. Дано определение вариантного типа:

type Collection == empty | atom (head:Elem) | list(head : Collection), Elem

Дать эквивалентное определение без использования вариантных определений.

Решение:

type Elem, Collection

value empty : Collection,

atom : Elem -> Collection,

list : Collection -> Collection,

head : Collection -~-> Collection,

head : Collection -~-> Elem

axiom

[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]

all e : Elem :- head (atom(e)) is e

ОТВЕТЫ И РЕШЕНИЯ К УПРАЖНЕНИЯМ

1.1. (b) type ST = {| n : Int:- n \ 2 = 1 |}

1.2. (a) да

1. да

2. нет

3. нет

4. да

5. нет

6. нет

7. да

8. да

9. нет

10. да

1.3. (a) false (по свойству (1))

1. a

Решение: 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  a

1.4. (a) да (для данного i выбираем j  i)

(b) нет (не верно, например, для i  0)

1. нет

1.5. (a) all i : Int :- exists j : Int :- j  i или (exists i : Int :- all j : Int :- i >= j)

(d) exists k : Nat :-n = k * k

2.1. (a) type Points = {| (x, y) : Real >< Real :- x >= 0 /\ y >= 0 /\ y >= x |}

2.2. (a) is_even : Nat -> Bool

is_even(n) is (exists m : Nat :- n  2  m)

или альтернативное определение:

is_even : Nat -> Bool

is_even(n) is n \ 2  0

2.3. (a) value

max : Int >< Int -> Int

max(i, j) is if i >= j then i else j end

1. value

max : Int >< Int -> Int

max(i, j) as y

post (y = i /\ y >= j) \/ (y  j /\ y >= i)

1. value

max : Int >< Int -> Int

axiom

all i,j : Int :- max(i, j) is if i >= j then i else j end

2.4. (a) type Complex  Real >< Real

1. value zero : Complex  (0.0,0.0)

2. value c : Complex :- let (x, y) = c in x = y end

3. value

add : Complex >< Complex -> Complex

add((x₁,y₁), (x₂,y₂)) is (x₁  x₂, y₁  y₂),

mult : Complex >< Complex -> Complex

mult((x₁,y₁), (x₂,y₂)) is (x₁  x₂  y₁  y₂, x₁  y₂  y₁  x₂)

1. value

f : Complex -> Complex

f(c₁) as c₂ post c₁ ~= c₂

2.5. (a) type

Circle  Center >< Radius,

Center  Position,

Radius = { r : Real :- r >= 0.0 }

1. value

on_circle : Circle >< Position -> Bool

on_circle((c,r), p) is distance(c, p) = r

или альтернативное определение:

value

on_circle : Circle >< Position -> Bool

on_circle(circ, p) is

let

(c,r) = circ

in

distance(c,p) = r

end

1. value

circle : Circle = (origin, 3.0)

1. value

pos : Position :- on_circle(circle, pos)

2.7. value

approx_sqrt : Real >< Real --> Real

approx_sqrt(x, eps) as s

post s ** 2.0 <= x /\ x  (s  eps) ** 2.0

pre x >= 0.0 /\ eps  0.0

2.8. (b) value

F2 : Nat >< Nat >< Nat -> Nat >< Nat

F2(a, b, c) as (v, w)

post

if 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

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} или

{n  n : Nat :- is_a_prime(n) /\ n  20 },

is_a_prime : Nat -> Bool

is_a_prime(n) is (all k : Nat :- (k < n /\ k > 1) => n \ k ~= 0)

1. card { n  n : Nat :- 30 \ n = 0} = card {1, 2, 3, 5, 6, 10, 15, 30} = 8

3.3. card { (x, y)  x, y : Int :- x * x + y * y < 25 }

3.4. (a) value

max : Int-set -~-> Int

max(s) as m

post

m isin s /\ (all k : Int :- k isin s => k <= m)

pre s ~= { }

1. (a)

scheme

UNIVERSITY_SYSTEM =

class

type

Student,

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 -> Bool

is_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 -> Bool

hasStudent(s, (ss, cis)) is s isin ss,

 hasCourse проверяет, читается ли данный курс в указанном университете */

hasCourse : Course >< University -> Bool

hasCourse(c, (ss, cis)) is

(exists (c1, ss1) : CourseInfo :- (c1, ss1) isin cis /\ c = c1),

 studOf возвращает множество студентов заданного университета, посещающих указанный курс 

studOf : Course >< University -~-> Student-set

studOf(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-set

attending(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 -~-> University

newStud(s, (ss, cis)) is (ss union {s}, cis)

pre ~hasStudent(s, (ss, cis)),

 dropStud исключает указанного студента из числа студентов заданного университета 

dropStud : Student >< University -~-> University

dropStud(s, (ss, cis)) is

(ss \ {s}, {(c, ss1 \ {s})  (c, ss1) : CourseInfo :- (c, ss1) isin cis})

pre hasStudent(s, (ss, cis)),

 newCourse добавляет новый курс с пустым множеством студентов к числу курсов заданного университета 

newCourse : Course >< University -~-> University

newCourse(c, (ss, cis)) is (ss, cis union {(c, {})})

pre ~hasCourse(c, (ss, cis)),

 delCourse удаляет указанный курс из числа курсов заданного университета 

delCourse : Course >< University -~-> University

delCourse(c, (ss, cis)) is (ss, cis \ {(c, ss1) | ss1 : Student-set :- true})

pre hasCourse(c, (ss, cis))

end

(b) value

studOf : Course >< University -~-> Student-set

studOf(c, (ss, cis)) as ss1

post (c, ss1) isin cis

pre hasCourse(c, (ss, cis))

1. (a) 169

(b) chaos

4.2. (a) <.2,4,6,8,10,12,14,16,.> или <.2 * n | n in <.1..8.>.>

1. <.1,4,9,16,25,36,49,64,81,100.> или

<.n | n in <.1..100.> :- exists k : Nat :-n = k * k.>

4.3. value

Fib_numbers : Nat-inflist

axiom

Fib_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. value

is_sorted : Int-list -> Bool

axiom

all L : Int-list :-

is_sorted(L) is

(all i1, i2 : Nat :- {i1, i2} <<= inds L /\ i1 < i2 => L(i1) < L(i2))

4.5. type Elem

value

1. length : Elem-list -> Nat

length(k) is if k  <..> then 0 else 1  length(tl k) end

или

length : Elem-list -> Nat

length(k) is card (inds k)

или

length : Elem-list -> Nat

length(k) is

case k of

<..> -> 0,

<.i.> ^ lr -> length(lr)  1

end

1. rev : Elem-list -> Elem-list

rev(k) is if k  <..> then <..> else rev(tl k) ^ <.hd k.> end

или

rev : Elem-list -> Elem-list

rev(k) is <.k(len k  i  1)  i in <.1 .. len k.>.>

1. del : Elem-list >< Elem-> Elem-list

del(k, e) is

case k of

<..> -> <..>,

<.i.> ^ lr -> if i = e then del(lr, e)

else <.i.> ^ del(lr, e) end

end

или

del : Elem-list >< Elem-> Elem-list

del(k, e) is <.x | x in k :- x ~= e.>

1. number_of : Elem-list >< Elem-> Nat

number_of(k, e) is card {i | i : Nat :- i isin inds k /\ k(i) = e}

4.7. scheme

PAGE 

class

type Page  Line-list, Line  Word-list, Word

value

is_on : Word >< Page -> Bool

is_on(w, p) is (exists i : Nat :- i isin inds p /\ w isin elems p(i)),

number_of : Word >< Page -> Nat

number_of(w, p) is

card {(i, j)  i,j : Nat :- i isin inds p /\ j isin inds p(i) /\ w  p(i)(j)}

end