Задачи 2-го типа (номер 2)

2. Дать explicit или implicit определение функций (включая слабейшее предусловие), отвечающих требованиям аксиом:

type S, E value create : Unit -> S, add : E >< S -> S, del : E>< Nat >< S -~-> S, get : E >< S -> Nat,

axiom all e : E, s : S :- get( e, create( ) ) is 0, all e1,e2 : E, s : S :- get ( e1, add (e2, s)) is if e1 = e2 then 1+get( e1, s ) else get( e1, s ) end, all e1, e2 : E, n : Nat, s : S :- del( e1, n, add( e2, s )) is if n=0 then add(e2, s ) elsif e1 = e2 then del( e1, n-1, s ) else add(e2, del( e1, n, s ) ) end

Решение

- мультимножество

2. Дать явную спецификацию, которая может быть уточнением данной:

type С,A = Nat value create: Unit -> C, add : A >< C -> C,

get : C -~-> A >< C axiom all e:A, l:C :- get (add(e,l)) is if (e<0) \/ (l=create()) then (e,l) else let (a,b)=get(l) in (a,add(e,b)) end end

Решение

type С-list, A = Nat

value

create: Unit -> C create() is <..>,

add : A >< C -> C

add (a,c) is

if (a<0) then a ^ l

else l ^ a end ,

get : C -~-> A >< C

get (c) is (hd c, tl c)

pre len c > 0

2. Дать explicit или implicit определение функций (включая слабейшие предусловия), отвечающих требованиям аксиом:

type S, E value create : Unit -> S, add2 : S >< E -> S, add3 : E >< S >< E-> S, del : S -~-> S, get : S -~-> E

axiom all e1,e2 : E, s : S :- del( add3( e1, s, e2 ) ) is add2(s, e2) , all e : E, s : S :- del(add2(s,e)) is if s=create() then create() else add2(del(s), e) end, all e1,e2 : E, s : S:- get(add3(e1,s,e2)) is e1, all e : E, s : S :- get(add2(s, e)) is if s=create() then e else get (s) end

Решение

add2 реализует очередь, add3 добавляет элемент с двух сторон.

2. Дать explicit или implicit определение функций (включая слабейшее предусловие), отвечающих требованиям аксиом:

type S, E value create : Unit -> S, add : E >< S -> S, del : E>< Nat >< S -~-> S, get : E >< S -> Nat,

axiom all e : E, s : S :- get( e, create( ) ) is 0, all e1,e2 : E, s : S :- get ( e1, add (e2, s)) is if e1 = e2 then 1+get( e1, s ) else get( e1, s ) end, all e1, e2 : E, n : Nat, s : S :- del( e1, n, add( e2, s )) is if n<=1 then add(e2, s ) elsif e1 = e2 then del( e1, n-1, s ) else add(e2, del( e1, n, s ) ) end

Решение – мультимножество, где не все элементы удаляются.

2. Дать explicit или implicit определение функций (включая слабейшие предусловия), отвечающих требованиям аксиом:

type S, E value create : Unit -> S, add1 : S >< E -> S, add2 : S >< E-> S, del : S -~-> S, get : S -~-> E

axiom all e : E, s : S :- add2(s, e) ) is add1(add1(s, e), e) , all e : E, s : S :- del(add1(s,e)) is if s=create() then create() else add1(del(s), e) end, all e : E, s : S :- get(add1(s, e)) is if s=create() then e else get (s) end

Решение: - add1 реализует очередь, add2, ставит в очередь сразу два элемента.

Задачи 2-го типа

Дать explicit или implicit определение функций (включая слабейшее предусловие), отвечающих требованиям аксиом:

type S, E value create : Unit -> S, add : E >< S -> S, del : E>< Nat >< S -~-> S, get : E >< S -> Nat,

axiom all e : E, s : S :- get( e, create( ) ) is 0, all e1,e2 : E, s : S :- get ( e1, add (e2, s)) is if e1 = e2 then 1+get( e1, s ) else get( e1, s ) end, all e1, e2 : E, n : Nat, s : S :- del( e1, n, add( e2, s )) is if n=0 then add(e2, s ) elsif e1 = e2 then del( e1, n-1, s ) else add(e2, del( e1, n, s ) ) end

Решение

- мультимножество; у функции del есть предусловие – нельзя исключить большее количество элементов данного значения, чем их имеется в мультимножестве

Задача 2.

Определить типы данных, дать явную спецификацию функций, определить предусловия частично-вычислимых функций.

type S, E

value

create : Unit -> S,

push_down : E >< S -> S,

push_right : E >< S -> S,

pop_up : S -~-> S,

pop_left : S -~-> S,

get : S -~-> E,

axiom

all e : E, s : S :-

pop_up( push_down( e, s ) ) is s,

all e : E, s : S :-

pop_up( push_right( e, s ) ) is pop_up( s ),

all e : E, s : S :-

get( push_down( e, s ) ) is e,

all e : E, s : S :-

get( push_right( e, s ) ) is e,

all e : E, s : S :-

pop_left( push_right( e, s ) ) is s

Решение:

type S = L-list, L = E-list, E

value

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 ~= <..>

(pre s ~= <..> /\ len hd s > 1) – тоже верно,

get : S -~-> E

get (s) is hd hd s

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

Задача 2.

Разработать спецификацию группы функций.

Определить типы данных и дать explicit определение функций add и del, удовлетворяющих следующим аксиомам. Если необходимо, специфицировать предусловия.

type S, K, V

value

create : Unit -> S,

add : K >< V >< S -> S,

del : K >< S -~-> S,

get : K >< S -~-> V

axiom

all k1,k2 : K, v2 : V, s : S :-

get (k1, add (k2, v2, s)) is if k1 = k2 then v2

else get( k1, s )

end,

all k1,k2 : K, v2 : V, s : S :-

del( k1, add( k2, v2, s )) is if k1 = k2 then del (k1, s)

else add(k2, v2, del( k1, s ) )

end

Решение:

type S = K –m-> V, K, V

value

create : Unit -> S

create () is [ ],

add : K >< V >< S -> S

add (k,v,s) is

s !! [k +> v],

del : K >< S -~-> S

del (k, s) is

s \ {k}

pre true

Задача 2.

Разработать явную спецификацию группы функций, удовлетворяющих следующим аксиомам.

Если необходимо, специфицировать предусловия.

type S, E

value

create : Unit -> S,

down : E >< S -> S,

right : E >< S -> S,

up : S -~-> S,

left : S -~-> S,

get : S -~-> E

axiom

all e : E, s : S :-

get(right( e, s ) ) is e,

all e : E, s : S :-

left(right( e, s ) ) is s,

all e : E, s : S :-

up(down( e, s ) ) is s,

all e : E, s : S :-

up(right( e, s ) ) is up( s ),

all e : E, s : S :-

get(down( e, s ) ) is e

Решение:

type S = L-list, L = E-list, E

value

create : Unit -> S

create () is <..>,

down : E >< S -> S

down (e,s) is <. <.e.> .>^s,

right : E >< S -> S

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

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

end,

up : S -~-> S

up (s) is tl s

pre s ~= <..>,

left : S -~-> S

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 ~= <..>