1. Äàíî explicit îïðåäåëåíèå ôóíêöèè. Íàïèñàòü implicit-ñïåöèôèêàöèþ ôóíêöèè ýêâèâàëåíòíîé äàííîé.
value
f : Int ><Int
>< Int -> write x, y Int
>< Int
f(a,b,c) is if a=b then
(if a+b > c then c else x:=y; a+b end,
b*(if c>0 then x:=c; c else 0-c end))
else
(y:=a+b; y, a-b) end
Ðåøåíèå
value
f : Int ><Int
>< Int -> write x, y Int
>< Int
f(a,b,c) as (d,
e)
post if a=b then
y=y’ /\ (if
a+b > c then d=c else x=y; d=a+b end,
if c>0 then x=c; d=b*c else
x=x’ /\ d=0-c end)
else (x=x’ /\ y=a+b /\ d=a+b /\ e=a-b) end
1. Äàíî explicit îïðåäåëåíèå ôóíêöèè. Íàïèñàòü implicit-ñïåöèôèêàöèþ ôóíêöèè ýêâèâàëåíòíîé äàííîé.
value
f :
Int
>< Int
-> write x read y Int >< Int >< Int
f
(a, b) is
local variable v
: Int := 0
in
for i in <.a..b.> do
v := v+2*(x:=i;i)
end; (a,b,v+y)
end
Ðåøåíèå
value
f :
Int
>< Int
-> write x read y Int >< Int >< Int
f
(a, b) as (c,d,e)
post if
a<b then x=x’ /\ (c,d,e)=(a,b,y)
else x=b /\ (c,d,e)=(a,b,(a+b)*(b-a+1)+y)
end
1. Äàíî explicit îïðåäåëåíèå ôóíêöèè. Íàïèñàòü implicit-ñïåöèôèêàöèþ ôóíêöèè ýêâèâàëåíòíîé äàííîé.
value
f : Int ><Int
>< Int -> write x, y read z Int >< Int
f(a,b,c) is if a=b then
(if a+b > c then c else x:=y; a+b end,
b*(if c>0 then x:=c; c else 0-c end))
else
(y:=a+b; y, a-b) end
Ðåøåíèå
value
f : Int ><Int
>< Int -> write x, y read z Int >< Int
f(a,b,c) as (d,e)
post if a=b then
y=y’ /\ (if
a+b > c then d=c else x=y; d=a+b end,
if c>0 then x=c; d=b*c else
x=x’ /\ d=0-c end)
else (x=x’ /\ y=a+b /\ d=y
/\ e=a-b) end
1. Äàíî explicit îïðåäåëåíèå ôóíêöèè. Íàïèñàòü
implicit-ñïåöèôèêàöèþ ôóíêöèè ýêâèâàëåíòíîé äàííîé.
value
f : Int
>< Int
-> write x, y read z Int >< Int >< Int
f (a, b) is
local variable v
: Int := 0
in
y:= x + z;
for i in <.a..b.> do
v := v+(x:=v;2)*i
end; (a,b,v)
end
Ðåøåíèå
value
f :
Int
>< Int
-> write x, y read z Int >< Int >< Int
f
(a, b) as (c,d,e)
post y=x’+z /\ if a<b then x=x’ /\ (c,d,e)=(a,b,0)
else x= (a+b-1)*(b-a) /\ (c,d,e)=(a,b,(a+b)*(b-a+1))
end
Äàíî explicit îïðåäåëåíèå ôóíêöèè. Íàïèñàòü implicit-ñïåöèôèêàöèþ ôóíêöèè ýêâèâàëåíòíîé äàííîé.
value
f : Int ><Int
>< Int -> write x read y Int >< Int
f(a,b,c) is if a=b then
(if a+b > c then c else x:=y; a+b end,
b*(if c>0 then c else 0-c end))
else
(x, (x:=a+b; a-b)) end
Ðåøåíèå
value
f : Int ><Int
>< Int -> write x, y Int
>< Int
f(a,b,c) as (d,
e)
post if a=b then
(if a+b > c
then x=x’ /\ d=c else x=y /\ d=a+b
end /\
if c>0 then
e=b*c else e=b*(0-c) end)
else (x’=a+b /\ d=x’ /\
e=a-b) end
Äàíà implicit
ñïåöèôèêàöèÿ ôóíêöèè, îïèñàòü ôóíêöèþ ýêâèâàëåíòíóþ äàííîé â explicit ôîðìå.
Ñïåöèôèöèðîâàòü ñëàáåéøèå ïðåäóñëîâèÿ.
value
f : Real >< Real -~-> write x Real
f(a,b) as y
post if a>b then ( x / y = a ) /\ ((x2) + y = b ) else y = x /\ a / x = x’ end
Ðåøåíèå:
value
f : Real >< Real
-~-> write x Real
f(a,b) is
if a > b then
if a~=0.0 then
x:= ((0.0-1.0 + sqrt(1+4*a*b) ) |^| (0.0-1.0 - sqrt(1+4*a*b) )) / (2.0*a); x / a
else x:=0.0; b
else x:=a/x
end
pre ((a>b) => (1+4*a*b >= 0.0)) /\
((a<=b) => (x~= 0.0))
Äàíà explicit ñïåöèôèêàöèÿ ôóíêöèè, îïèñàòü åå â implicit ôîðìå.
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) is if a=b then
(if a+b > c then
c else a+b
end, a*b*(if c>0 then x:=c; c else 0-c end))
else (a+b, x:=b;
x-b)
end
Ðåøåíèå:
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) as (v, w)
post
if
a=b then
if a+b > c then
v=c else v=a+b end /\
if c>0 then x=c /\ w= a*b*c else
x=x’ /\ w= a*b*(0-c) end
else v=a+b /\ x=b
/\ w=a-b
end
Çàäà÷à 1.
Äàíî explicit îïðåäåëåíèå ôóíêöèè. Íàïèñàòü implicit-ñïåöèôèêàöèþ ôóíêöèè ýêâèâàëåíòíîé äàííîé.
value
f : Int ><Int
>< Int -> write x, y Int
>< Int
f(a,b,c) is if a=b then
x:=y; (if a+b
> c then c else a+b end,
y:=c; b*(if c>0 then x:=c; c else
0-c end))
else
(y:=a+b; y, a-b) end
Ðåøåíèå:
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) as (v, w)
post
if
a=b then
y=c /\
if c > 0 then x=c else x=y’ end /\
if a+b > c then
v=c else v=a+b end /\
if c>0 then w= b*c else w= b*(0-c) end
else y=a+b /\ v=a+b
/\ x=x’ /\ w=a-b
end
Äàíà explicit ñïåöèôèêàöèÿ ôóíêöèè, îïèñàòü åå â implicit ôîðìå.
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) is
if x>0 then x:=x * 2 end;
if a=b then
(if a+b > c then
c else a+b
end, a*b*(if c>0 then x:=c; c else 0-c end))
else (a+b, x:=b;
a-b)
end
Ðåøåíèå:
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) as (v, w)
post
if
x’>0 then
if b then x = x’ * 2
else if c>0 then x=c else x=x’*2 end
end
else x=b
end /\
if a=b then
if a+b > c then
v=c else v=a+b end /\
if c>0 then w= a*b*c else w= a*b*(0-c) end
else v=a+b /\
w=a-b
end
Çàäà÷à 1.
Äàíà explicit ñïåöèôèêàöèÿ ôóíêöèè, îïèñàòü ôóíêöèþ ýêâèâàëåíòíóþ äàííîé â implicit ôîðìå.
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) is if a=b then
(if a+b > c then
c else a+b
end,
a*b*(if c>0 then x:=c; c else 0-c end))
else (a+b, a-b)
end
Ðåøåíèå:
value
f : Int
><Int
>< Int
-> write x Int >< Int
f(a,b,c) as (v, w)
post
if
a=b then
if a+b > c then
v=c else v=a+b end /\
if c>0 then x=c /\ w= a*b*c else
x=x’ /\ w= a*b*(0-c) end
else v=a+b /\ x=b
/\ w=a-b
end