Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://sp.cs.msu.ru/courses/fmsp/meth2008.pdf Äàòà èçìåíåíèÿ: Tue Sep 6 20:26:06 2011 Äàòà èíäåêñèðîâàíèÿ: Mon Oct 1 21:35:58 2012 Êîäèðîâêà:

..

.. , ..

RSL

2008


378(075.8):004.43 32.973-018.173 89 « », RSL. RSL , . « ». « » , .

: .., ..., .., ..-..,

.. , .. « RSL» -- . ( 05899 24.09.01), 2008. -- 88 .

- . .. .

ISBN 978-5-89407-338-5 ISBN 978-5-317-02422-2

© . .. , 2008 © .. , .. , 2008
2



« » ­ « ». : · - · · (), , , . . « ». : · () · () , . , . , / , . , . , , , ( ) , , , / . . « » , , . - , , , . , , . , . , , , , . , , , , , , , , , .
3


, . , , , . , : , , . , , . ­ , , , , , . , . . RSL. , , RSL . , RSL, . . « ».

4


1. RSL. RSL
RSL (, , ). . RSL. RSL. RSL. . RSL RSL : · (), · , · (). . . , ( = ~=). , , = ~=. . = ~=. . () . :
ST1 = {| t : T1:- p(t) |},

ST1 , T1 - () , p(t) ­ , . () , - true. RSL RSL :
Bool ­ , Int ­ , Nat ­ , Real ­ , Char ­ , Text ­ ,

5


Unit ­ ().

Bool truefalse, /\, \/, =>, , is (), =, ~=. Int . +, -, , /, \, , abs, real, / , \ ­ ,- ,abs ­ real ­ Int Real. , Int Real RSL . <, <=, >, >=, =, ~=. Nat 0, 1, 2, ..., Int :
Nat = {| i : Int :- i >= 0 |}.

, Real , +, -, , /, , <, <=, >, >=, =, ~=, abs, Real 0 . :
int 4.6 = 4 int -4.6 = -4

Int. int, int ­ Int,

(1 .0, 12.35 ..). Char , = ~, Char (: f, Z ..). Text , . ,ABC, ­ . =, ~=. Unit void C, C++, Java, C#, . RSL RSL, . RSL chaos, () . - , - (, 1/ x x=0.0). chaos RSL , .

6


,chaos Bool, Int. RSL , .. , . ( chaos) . , ­ .
/\ true false chaos \/ true false chaos => true false chaos true true false chaos true true true chaos true true true chaos false false false chaos false true false chaos false false true chaos chaos chaos false chaos chaos true chaos chaos chaos chaos true chaos

:
chaos chaos

= is a b , .
is a b chaos = a b chaos a true false false a true false chaos b false true false b false true chaos chaos false false true chaos chaos chaos chaos

, , RSL /\\/ , .. e1 /\ e2 e2 /\ e1e1 \/ e2 e2 \/ e1 .

7


RSL RSL , :
if expr then expr1 else expr2 end,

expr , expr1expr2 , . , :
if x > y then x ­ y else y ­ x end

:
if true then expr1 else expr2 end expr1 (1), expr2 , if false then expr1 else expr2 end expr2 (2), expr1 , if a then expr1 else expr2 end if a then expr1[true/a] else expr2[false/a ] end (3), expr1[true/a] expr1 true a. if chaos then expr1 else expr2 end chaos (4), expr1 expr2 .

RSL , :
if expr1 then v_expr1 elsif expr2 then v_expr2 ... if exprn-1 then v_expr else v_exprn end

n-1

:
if expr1 then v_expr1 else if expr2 then v_expr2 else ... else if exprn-1 then v_expr else v_exprn end end ... end

n-1

8


, x:
if x = 0 then 0 elsif x > 0 then x else 0 ­ x end

RSL . :all (), exists (), exists! (!). 1. : (a) , (b) , (c) (­1.0, 1.0).
2. , .

RSL?
(a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k)
(a) is a true \/ a is true a \/ true is true a => true is true a => b is a b a \/ a is true (a /\ a) is false (a /\ b) /\ c is a /\ (b /\ c) (a \/ b) \/ c is a \/ (b \/ c) (a = a) is true (a is a) is true

: · ; · , chaos. , (c):
chaos \/ true is chaos, (chaos is true) is false

, (c) RSL. 3. :
(a) if true then false else chaos end is ? (b) if a then ( a is chaos) else false end is ? 9


: (1) - (4). 4. ?
(a) all i : Int :- exists j : Int :- i+j = 0 (b) all i : Int :- exists j : Nat :- i+j = 0 (c) exists i : Int :- all j : Int :- i+j = 0 5. RSL , :

(a) , (b) max x y, (c) n , (d) n , (e) n . : RSL.

10


2.
RSL . . let. - , , . . . . . . RSL RSL . . ­ , . () :
scheme id = class decl ... decl end

1

n

id ­ , decl1 ,..., decln (n 0) ­ . , . . RSL : (type), (value), (axiom), (variable) (channel). :
scheme id = class type

< >
value

< >
axiom

< >
end

( products ) , , , :
(1,2) (1,true,John).

, .. (1,2)(2,1) .

11


, , :
t1 >< ... >< tn, n2,



, ti (1 i n) ><. n(n- ) (v1,...,vn), vi ­ ti. :
(true, p => q) : Bool >< Bool (x + 1,0,this is a text) : Int >< Nat >< Text

=~=. , , (x,y,z). let let . let­ , . let . let- :
let (x1,...,xn) = a in expr end

a , x1,...,xn - , expr , . , a b . :
let (x1,y1) = a in let (x2,y2) = b in ((x2 ­ x1)**2.0 + (y2 ­ y1)**2.0)**0.5 end end

RSL , , value. RSL : · (, explicit), · (, implicit), · .
12


, . , RSL :
value x : Int = 1

x=1. , , , , , . , :
type Stack value x : Int :- x > 0, empty : Stack

x, , empty Stack, . . , - . . , , (, ). , , . , x :
value x : Int axiom x is 1 value x : Int axiom x > 0

( ), ( ).

RSL , .. , , . ­ . f, T1 T2, (total function), T1 f T2, .. f :
all x : T1 :- exists! y : T2 :- f(x) is y

13


f :
f : T1 -> T2

. f, T1 T2, (partial function), v T1, f(v) ( f(v) is chaos), , f(v) . f :
f : T1 --> T2

. , . , . : · (, explicit), · (, implicit), · . . ( ) , . RSL :
value f : Int -> Int f(x) is x + 1

p(x), 1/x:
value p : Real -~-> Real p(x) is 1.0/x pre x ~= 0.0

, , .

14


( ) , . , , , , .. , . , , . , , , . . f(x), , :
value f : Int -> Int f(x) as r post r > x

square_root(x) :
value square_root : Real -->. Real square_root(x) as s post s s = x /\ s >= 0.0 pre x >= 0.0

, , , . , . , . , . , (,f(g(x), x) is h(x)), .. .

15


f(x), :
value f : Int -> Int axiom all x : Int :- f(x) is x + 1

square_root(x), , :
value square_root : Real --> Real axiom all x : Real :-x >= 0.0 => exists s : Real :- square_root(x) = s /\ s s = x /\ s >= 0.0

, : 1. : · ; · : (a) , (b) , (c) : - ( ), - ( ); 2. : · ( ), · ( ), · ( , ). 1. : , y=x, (b) , 5.
(a)

: .

16


2. , :
(a) (b)

is_even , is_a_prime, , .

: (a) \ ( ) .
3. max,

, : (a) , (b) , (c) . : · ; · (a) (c) RSL. 4. :
(a) (b) (c) (d) (e)

Complex , zero 0 + 0i, c, x + xi; addmult , f, , .

: · (b) (d) (explicit) , .. ; · (c) (e) (implicit) , ; · (c) (d) let. , , ( c) c :
let (x, y) = c in x = y end

5. :
scheme SYSTEM_OF_COORDINATES= class type Position = Real >< Real value

17


origin : Position = (0.0,0.0), distance : Position >< Position -> Real distance((x1, y1),(x2, y2)) is ((x2 ­ x1)**2.0 + (y2 ­ y1)**2.0)**0.5 end

Position , origin , . , origin , .. . :

distance distance

(a) Circle ; (b) on_circle,,

;
(c) 3.0 ; (d) pos ,

. : · (a) CenterRadius , Center Position, Radius :
Radius = {| r : Real :- r >= 0.0 |},

;
· (b) (c)

, let ; · (d) .
6.

RATIONAL_NUMBERS, : (a) Rational ; (b) less, true, ; (c) add ; (d) max ; (e) check, , . : .
7. approx_sqrt, eps

( ) .
18


, : [approx_sqrt(x,eps), approx_sqrt(x,eps) + eps). : · , .. ; · , , .. . 8. , , : (a) value
F1 : Int >< Int >< Int -> Int >< Int F1(a, b, c) is if a < b then (a * c, b - a) elsif a > b then (a ­ b, b * c) else (a, b) end value F2 : Nat >< Nat >< Nat -> Nat >< Nat F2(a, b, c) is (if a + b > c then c else a + b end, a * b * (if > 0 then c else 0 ­c end))

(b)

19


3. .
, . . RSL. - . . RSL , .. . :
{1,3,5} {0.0, 1.5, 4.7} {Mary,John,Peter}

: - , - . , {1,3,5}, {5,3,1} {3,5,1,1} . RSL . RSL -set -infset, T-set T T-infset ­ . , Bool-set :
{ { { { } true} false} true, false},

{}. T-infset , , T. , T T-set T-infset. , Nat-infset ( ) . ( ), , , {v1,...,vn}, n0. , , , , ( ). , {3 .. 7} {3,4,5,6,7},{3 .. 3} ­ {3} {3 .. 2} ­ {}.
20


, , , :
{ value_expr | set_limitation },

(compehended) . value_expr , set_limitation , . {2n | n : Nat :- n <= 3}, {0, 2, 4, 6} {2n | n : Nat}, . RSL :
inter ­ (), union ­ (), \ - , isin, ~isin ­ ( ) <<, <<=, >>, >>= - ,

(,),

(, , , ), card ­ ,

= ~=. card , .. :
card : T-infset --> Nat

:





cardchaos.

card {1, 4, 56} = 3 card {} = 0 card {n | n : Nat} chaos

1. , : (a) 0 10, (b) 2 20. : . -

21


2. :
card { n | n : Nat :- 30 \ n = 0}

3. RSL

, 5. : . 4. : (a) max, , (b) choose, . : · , · , , .. . 5. . , - , . :

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, /* hasStudent , */ hasStudent : Student >< University -> Bool, / hasCourse , */ hasCourse : Course >< University -> Bool, / studOf , / studOf : Course >< University -~-> Student-set, / attending , / attending : Student >< University -~-> Course-set, / newStud / newStud : Student >< University -~-> University,

22


/ dropStud / dropStud : Student >< University -~-> University, / newCourse / newCourse : Course >< University -~-> University, / delCourse / delCourse : Course >< University -~-> University end

(a) , . (b) studOf. (c) ? : · University , ( ), · () .

23


4. .
, . . . case. - . , :
<.1, 3, 3, 1, 5.> <.true, false, true.> <.3.14, 0.15.>

: - , - . , <.1, 3, 5.>, <.5, 3, 1.> <.1, 3, 3, 1, 5.> . RSL . -list -inflist, T-list T T-inflist ­ . , Bool-list ( ) . T-inflist , T. , T T- list T-inflist. , . , . <.v1,...,vn.>, n0 vi , , <..> . . , , .. <.v1..v2.>, v1 v2 , v1 > v2 . :
<.3..7.> =<.3, 4, 5, 6, 7.> <.3..3.> = <.3.> <.3..2.> = <..>

24


( comprehended list expression), <. value_expr | list_limitation .>. , - . value_expr ,list_limitation , , . , :
<.2n | n in <.0 .. 3.>.>

<.0 .. 3.>, , , <.0,2,4,6.>, . :
<.n | n in <.1 .. 100.> :- is_a_prime(n).>,

is_a_prime(n) , n . , 1 .. 100 , .. <.2,3,5,7,...,97.>. - RSL . , 1 , . :
<.2,5,3.> (2) = 5 <.<.2,5,3.>, <.3.>.> (1) = <.2,5,3.> <.<.2,5,3.>, <.3.> .> (1)(2) = <.2,5,3.> (2) = 5

chaos. :
<.1 .. 50.> (51) = chaos



, . , , , all_natural_numbers :
value all_natural_numbers : Nat-inflist axiom all_natural_numbers(1) = 0, exists idx : Nat :idx >= 2 => all_natural_numbers(idx) = all_natural_numbers(idx -1) + 1

. , ,
25


, :
<.n | n in all_natural_numbers :- is_a_prime(n).>

RSL :
^ : T-list >< T-inflist -> T-inflist hd : T-inflist --> T tl : T-inflist --> T-inflist len : T-inflist --> Nat elems : T-inflist -> T-infset inds : T-inflist -> Nat-infset

, RSL, = ~=. ^ , . hdtl «» - , . L :
hd L is L(1)

len ( 0), chaos. elems , . :
elems <..> = {} elems <.1,3,1.> = {1, 3} elems all_natural_numbers = {n | n : Nat}

L card elems L. inds . :
inds <..> = {} inds <.1,3,1.> = {1, 2, 3}

, FL:
inds FL = {1 .. len FL},

IL:
inds IL = {idx | idx : Nat :- idx >= 1}.

26


L :
elems L is {L(x) | x : Nat :- x isin inds L}

Text Char, .. Text = Char-list, , . :
"abc"(2) = <.'a', `b', `c'.>(2) = `b' tl "abc" = "bc"

case case, . case :
case value_expr of pattern1 -> value_expr1, ... patternn -> value_exprn end, n 1.

value_expr , pattern1,...,patternn ­ , . value_expr ( ) . patterni value_expri. , (). RSL , . ( RSL) (_), . case. , .
type Nat1 = {|n : Nat :- n > 0|} value Fib: Nat1 -> Nat1 Fib(n) is case n of 1 -> 1, 2 -> 1, _ -> Fib(n - 2) + Fib(n - 1) end

27


, ­ , .. if (let ...). , :
value reverse : Int-list -> Int-list reverse(L) is case L of <..> -> <..>, <.i.> ^ Lr-> reverse(Lr) ^ <.i.> end

1. :
(a) (b)
<.n * n | n in <.1..20.> :- n \ 2 = 1.>(7), <.n * n | n in <.1..20.> :- n \ 2 = 1.>(12).

2. , : (a) 2 16, (b) 1 100. : - . 3. , , 1000. : · , · , .
4. is_sorted,

. : .
5. Elem.

:
(a) length ­ len, (b) rev ­ , (c) del ­ , (d) number_of ­

. :
28


· hd tl; ·

case,

· (c) (d)

, .

6. max

.
7.

: , - . PAGE, :
(a) Page,Line, Word ,

, (b) is_on,, , (c) number_of, . : · (a) PageLine, · (b) indselems, · (c) ( , ), , card.

29


5. - .
, . . . - . . , , (domain) , , , (range). :
[3 +> true, 5 +> false] [Klaus +> 7, John +> 2, Mary +> 7]

Bool, ­ Text Nat. () {3,5}, ­ {true,false}, {Klaus,John,Mary}{2,7}. v +> w v w. , , , [3 +> true,5 +> false] [5 +> false,3 +> true] . :
T1 ­m-> T2,

T1 - () T2 ­ . , Nat -m->BoolText -m-> Nat. , , . :
[v1 +> w1,...,vn +> wn],

:
[v1 +> w1,...,vn +> wn,...],

n 0, vi wi ­ T1T2. . , .. :

30


vi = vk => wi = wk ,

vivk ­ .
[3 +> true,3 +> false].

. :

RSL , , : . , :
[v1 +> w1,...,vn +> wn],

n 0 ( , n = 0 []). vi wi ­ . . (comprehended map expression) , :
[ value_expr_pair | set_limitation ],

value_expr_pair , set_limitation . , :
[ n +> 2n | n : Nat :- n <= 2 ]

[0 +> 0,1 +> 2,2 +> 4]. :
[ n +> 2n | n : Nat ]

[0 +> 0,1 +> 2,2 +> 4,...]. - ( ) value_expr1(value_expr2), value_expr1 , ,value_expr2­ . :
[Klaus +> 7, John +> 2, Mary +> 7](John) = 2, [1 +> [Per +> 5, Jan +> 7], 2 +> [ ]](1)(Jan) = = [Per +> 5, Jan +> 7] (Jan) = 7,

:
[3 +> true,3 +> false](3) = true |^| false,

31


|^| () . , , , .. chaos:
[1 +> 2, 2 +> 3](5) = chaos

:
dom : (T1 ­m-> T2) -> T1-infset rng : (T1 ­m-> T2) -> T2-infset !! : (T1 ­m-> T2) >< (T1 ­m-> T2) -> (T1 ­m-> T2) union : (T1 ­m-> T2) >< (T1 ­m-> T2) -> (T1 ­m-> T2) \ : (T1 ­m-> T2) >< T1-infset -> (T1 ­m-> T2) / : (T1 ­m-> T2) >< T1-infset -> (T1 ­m-> T2) # : (T2 ­m-> T3) >< (T1 ­m-> T2) -> (T1 ­m-> T3)

domrng , m :
rng m is {m(x) | x : T1 :- x isin dom m}

= ~=. .

:
dom rng [ dom rng [ dom rng [ [3 +> true 3 +> true, []={} ]={} [ n +> 2n n +> 2n | , 5 +> false] = {3, 5} 5 +> false] = {true, false} | n : Nat ] = { n | n : Nat } n : Nat ] = { 2*n | n : Nat }

!!( ) , , , .. , , . :
x !! y is [v +> w | v : T1, w : T2 :- w = y(v) \/ v ~isin dom y /\ w = x(v)]

:
[3 +> true, 5 +> false] !! [5 +> true] = [3 +> true, 5 +> true] [3 +> true] !! [5 +> false] = [3 +> true, 5 +> false] [3 +> true] !! [ ] = [3 +> true]

union , :











32


[3 +> true, 5 +> false] union [5 +> true] = [3 +> true, 5 +> false, 5 +> true]

( ), . \/ , :\ ,/, , , . :
m \ s = [v +> m(v) | v : T1 :- v isin (dom m) \ s] m / s = [v +> m(v) | v : T1 :- v isin (dom m) inter s]

:
[ [ [ [ 3 3 3 3 +> +> +> +> tr tr tr tr ue ue ue ue , , , , 5 5 5 5 +> +> +> +> f f f f al al al al se se se se ] ] ] ] \ / \ / { { { { 5, 5, 3, 3, 7} 7} 5, 5, =[ =[ 7} 7} 3 5 = = +> true] +> false] [] [3 +> true, 5 +> false]

# , .. m1 m2 :
m1 # m2 = [v +> m1(m2(v)) | v : T1 :- v isin dom m2 /\ m2(v) isin dom m1]

:
[3 +> true, 5 +> false] # [Klaus +> 3, John +> 7] = [Klaus +> true] [3 +> true] # [Klaus +> 5] = [ ]

1. , : (a) , 30, 3, (b) ( 50), (c) , 20, , (d) , , , , (e) n, 30, [2, n]; n = 1, 10, 50. : . 2. - . :

33


scheme MAP_UNIVERSITY_SYSTEM = class type Student, Course, CourseInfos = Course -m-> Student-set, University = Student-set >< CourseInfos value /* hasStudent , */ hasStudent : Student >< University -> Bool, / hasCourse , */ hasCourse : Course >< University -> Bool, / studOf , / studOf : Course >< University -~-> Student-set, / attending , / attending : Student >< University -~-> Course-set, / newStud / newStud : Student >< University -~-> University, / dropStud / dropStud : Student >< University -~-> University, / newCourse / newCourse : Course >< University -~-> University, / delCourse / delCourse : Course >< University -~-> University end

, . : · , · , CourseInfos - , , .

34


6.
. , . . RAISE . . . . , - , . :
id(value_expr1, ..., value_exprn) is value_expr,

value_expri , , . , f(g(x),x) is h(g(x)). , .., , . , ( ) . , , - . . , , ( ). , , , , . :
DATABASE = class type Database, Key, Data value / / empty : Database, / / insert : Key> Database, / / remove : Key >< Database -> Database, / / defined : Key >< Database -> Bool, / , / lookup : Key >< Database -~-> Data end

35


Database. , ­ () ­ . () , . . empty, insert remove. ( observers) , . . . defined lookup. , , , ­ . empty insert, - remove. , :
insert(k1,d1,insert(k2,d2,...,insert(kn,dn,empty)...)),

.. insert . , . , . . : · / , · / . / . . , - lookup lookup(empty) lookup.

36


, : 1. , 2. , 3. / /. :
scheme DATABASE = class type Database, Key, Data value empty : Database, insert : Key> Database, remove : Key >< Database -> Database, defined : Key >< Database -> Bool, lookup : Key >< Database -~-> Data axiom [ defined_empty ] all k:Key :defined(k,empty) is false, [ defined_insert ] all k,k1:Key, d:Data, db:Database :defined(k,insert(k1,d,db)) is k = k1 \/ defined(k,db), [ defined_remove ] all k,k1:Key, db:Database :defined(k,remove(k1,db)) is k ~= k1 /\ defined(k,db), [ lookup_insert ] all k,k1:Key, d:Data, db:Database :lookup(k,insert(k1,d,db)) is if k = k1 then d else lookup(k,db) end pre k = k1 \/ defined(k,db), [ lookup_remove ] all k,k1:Key, db:Database :lookup(k,remove(k1,db)) is lookup(k,db) pre k ~= k1 /\ defined(k,db) end

RAISE . RAISE . : · · · · , , .
37


(refinement), . , , : · ( , ), · , · () . , . RAISE . , , . , y - , . , , , . . , () . RAISE re-writing , : 1. - : · , · , 2. - .., 3. . ( «») : 1 [[1]] ... n [[n]], , . .
38


[defined_empty] -, empty defined:
empty : Database = { }, defined : Key >< Database -> Bool defined(k,db) is (exists d : Data :- (k,d) isin db)

[defined_empty].
[ defined_empty ] all k:Key :defined(k,empty) is false - [[ ]] defined(k,empty) is false [[ empty]] defined(k,{}) is false [[ defined]] (exists d : Data :- (k,d) isin {}) is false [[ isin {}]] (exists d : Data :- false) is false [[ ]] false is false [[ ]] true

1. : · · · · , , , ( ).

2. : · · · · , , , ( ), · . : 1, 2 .

39


3. , - . . 4. , - . . 5. , ( ) .
value f1 : A >< L -~-> L, f2 : A >< L -~->, f3 : L -> Nat axiom all a : A, b : L :f3(f1(a,b)) is f3(b) + 1 pre f3(b) = 1, all a : A, b : L :f3(f2(a,b)) is 1 + f3(b) pre f3(b) = 1, all a : A, b : L :f1(a,b) is f2(a,b) pre f3(b) = 1 type L = A-list value f1 : A >< L -~-> L f1(a,b) is <. a .> ^ tl b pre b ~= <..>, f2 : A >< L -~-> L f2(a,b) is tl b ^ <. a .> pre b ~= <..>, f3 : L -> Nat f3(ls) is len ls

40


7.
. . , . . : ( )

type id = = variant1 | ... | variantn , n 1

( id) . .. , . : · ­ , · ­ , · ­ . , . , , , .. . . , - -, . :
type Colour = = black | white

:
type Colour /* */ value black : Colour, /* */ white : Colour axiom [ disjoint ] black ~= white, [ induction ] all p : Colour -> Bool :- (p(black) /\ p(white)) => (all : Colour :- p(c))

black white. ( ) , Colour
41


, .. . . , , black white, Colour. (record constructions). . , , . :
type Collection = = empty | add(Elem, Collection),

- empty add. Collection, : 1. empty, 2. , add. :
type Collection value empty : Collection, add : Elem > Collection axiom [ disjoint ] all el : Elem, : Collection :- empty ~= add(el,c), [ induction ] all p : Collection -> Bool :(p(empty) /\ (all el : Elem, : Collection :- p(c) => p (add(el,c)))) => (all : Collection :- p(c))

, , . :
type List = = empty | add(head : Elem, tail : List),

head tail, , add, «» «». :
42


type List value empty : List, add : Elem >< List -> List, head : List -~-> Elem, tail : List -~-> List axiom [ disjoint ] all el : Elem, ls : List :[ induction ] all p : List -> Bool :(p(empty) /\ (all el (all ls : List :[ head_add ] all el : Elem, ls : List :[ tail_add ] all el : Elem, ls : List :-

empty ~= add(el,ls), : Elem, ls : List :- p(ls) => p (add(el,ls)))) => p(ls)) head(add(el,ls)) is el, tail(add(el,ls)) is ls

head tail, , add. , . . List replace_head .
type List = = empty | add(head : Elem <-> replace_head, tail : List)

:
value replace_head : Elem >< List -~-> List axiom [ head_ replace_head ] all el,el1 : Elem, ls : List :- head(replace_head(el,add(el1,ls))) is el, /* */ [ tail_ replace_head ] all el : Elem, ls : List :- tail(replace_head(el,ls)) is tail(ls) pre ls ~= empty /* replace_head */

. , .

43


1. C Key Data, «» «». . : . 2. C Elem, . . : . 3. . (a) type Elem, (b) (c) (d)
Collection = = empty | add1(Elem, Collection) | add2(Elem, Elem, Collection) type Elem, Tree = = empty | node(left : Tree, val : Elem, rigth : Tree) type Elem, Tree = = empty | node(left : Tree, val : Elem <-> repl_val, rigth : Tree) type Figure = = box(length : Real, width : Real) | circle(radius : Real) | triangle(base_line : Real, left_angle : Real, right_angle : Real)

44


8.
. . . . RSL. . . . RSL , . , . . , ( ) . , .. . . RSL , . . . RSL variable, :
id : type_expr := value_expr,

id , type_expr ­ , value_expr . , , . . :
variable n : Nat := 1, s : Real = 0.0, a, b : Int

, .

45


RSL :
id := value_expr

id value_expr, () Unit. id value_expr , value_expr Unit. :
counter := counter +1

, , :
write id1, ..., idn, n 1,

( ), :
read id1, ..., idn, n 1,

. , . :
variabl value f1 : f2 : f3 : e n, m : Nat Unit -> write n Nat, Unit -> read m Nat, Nat -> write n read m Nat

f1 f2 , , , . f1 n , f2 ­ m . f3 n m . RSL :
value_expr1 ; value_expr
2

value_expr1
46


. value_expr2. value_expr1 Unit.
x := 1; x x := x + 1; x

value_expr2. :

- 1, - 1 x.

:
value_expr1 ; ... ; value_exprn , n > 1.

, value_exprn. Unit. if if :
if value_expr then value_expr1 else value_expr2 end,

, value_expr1 value_expr2 Unit. :
if value_expr then value_expr1 end

:
if value_expr then value_expr1 else skip end,

skip Unit, . :
if counter > 0 then counter := counter - 1 end

RSL , : · (while), · (until), · ( for). , , Unit, , . . while while while :
47


while value_expr do value_expr1 end,

value_expr ( Bool) , value_expr1 ( Unit) ­ ( ). while . value_expr, value_expr1, , while . until until until :
do value_expr1 until value_expr end

value_expr value_expr1 , value_expr until . for for for :
for list_limitation do value_expr1 end,

list_limitation ( ) . ( value_expr1) . :
for i in <. 1 .. n .> do result := result + 1.0 / (real i) end

. :
local variable id : t := value_expr in value_expr1 ; ... ; value_expr end, n 1.

n

, id t , value_expr ( ). , . , .

48


increase, 1 , counter.
variable counter : Nat := 0 value increase : Unit -> write counter Nat increase() is counter := counter + 1; counter

: , . RSL id', id . choose, :
variable set1 : Int-set value choose : Unit -~-> write set1 Int choose() as res post res isin set1' /\ set1 = set1' \ {res} pre set1 ~= { }

(res isin set1') , , ( set1 = set1' \ {res}) , set1 . , . , , . , , :
x = x'

1. :
(a) x := 1; x := 2 (b) (x :=1; x) + (x := 2; x) (c) (x :=2; x) + (x := 1; x)

49


2. - . : · · · · · (a) (b) , , , , ( ). . .

: · , · .
3. fract_sum,

, :
(a) (b) (c)

while, until, for.

4. :
(a)
value f : Int >< Int >< Int -> write x, y Int >< Int f(a,b,c) is if a = b then (if a + b > then else x := y; a + b end, b * (if > 0 then x :=c; else 0 ­ end)) else (y :=a + b; y,a - b) end variable v1, v2 : Int value f : Int >< Bool > -> write v1read v2 Nat >< Bool f(a,b) is local variable n : Int in if b then v1 := v2 * a; n := v1 ** 2 + v2 ** 2 else n := if v1 > v2 then v1 ** 2 ­ v2 ** 2 else v2 ** 2 ­ v1 ** 2 end end; if v1 > v2 tnen v1 := v2 end; (n, v1 = v2) end

(b)

50


9.
. . . : , , , . . . RSL . , . channel. c :
id1, ... ,idn : type_expr, n 1.

:
channel a : Nat, c, b : Int

, , RSL . :
in id1, ..., idn, n 1,

, , :
out id1, ..., idn, n 1,

, . :
channel a ,b: Nat value p : Unit -> in a out b Unit

p Nat a b.

51


RSL : , . :
channel id: T

:
id?

, - . , . , . . , :
a := c?

a , c. :
id! value_expr

value_expr, id. , - . , . value_expr id. Unit. opb, , add get. Elem add get.
scheme ONE_PLACE_BUFFER = class type Elem channel add, get : Elem value opb : Unit -> in add out get Unit axiom opb() is let v = add? in get!v end; opb() end

, .

52


RSL · · · : , , , · (interlock).

:
value_expr1 || value_expr
2

, , . Unit, . || . , :
channel c : Int variable x : Int

x := c? c!5 :
x := c? || c!5

. :
x := 5

. . , - . , :
(x := c? || c!5) || c!7

:
· ·
x := 7; c!5 x := 5; c!7

· . :
value_expr1 |=| value_expr
2

53


value_expr1 value_expr2 , . , , .. , . «». |=| . . , :
channel c , d: Int variable x : Int

:
x := c? |=| d!5

: c d. , :
(x := c? |=| d!5) || c!1

c, :
x := 1

( c!1). . () :
value_expr1 |^| value_expr2 ,

value_expr1 value_expr2 , . , . |^| . , :
(x := c? |^| d!5) || c!1

c!1 , x := c? d!5 . x:=c?, :
x:= c? || c!1,

c. d!5, :
d!5 || c!1,

54


. .





(interlock) (interlock) :
value_expr1 ++ value_expr2 ,

++ . , , , , . Unit, . (||) , , . , . , . :
value e, e1, e2 : T channel c , c1, c2: T variable x : T

:
x := c? ++ c!e is x := e x := c? || c!e is (x := e) |^| ((x := c?; c!e)|=|(c!e; x := c?)|=|(x := e))

. , . :
(x := c1? |=| c2!e2) ++ c1!e1 is x := e1 (x := c1? |^| c2!e2) ++ c1!e1 is x := e1 |^| stop

- (c2!e2 ++ c1!e1). RSL stop. , , :
x := c1? ++ c2!e is stop

55


:
x := c1? || c2!e is (x := c1?; c2!e) |=| (c2!e; x := c1?)

, , . :
value_expr1 || (value_expr2 |^| value_expr3) is (value_expr1 || value_expr2) |^| (value_expr1 || value_expr3) value_expr1 ++ (value_expr2 |^| value_expr3) is (value_expr1 ++ value_expr2) |^| (value_expr1 ++ value_expr3)

, value_expr, value_expr1 value_expr2 c1 ~= c2, :
x := c1? || c2! value_expr is (x := c1?; c2! value_expr) |=| (c2! value_expr; x := c1?) x := c? || c! value_expr is (x := value_expr) |^| ((x := c?; c! value_expr)|=|(c! value_expr; x := c?)|=|(x := value_expr)) x := c1? ++ c2! value_expr is stop x := c? ++ c! value_expr is x := value_expr (x := c1? |=| c2! value_expr2) ++ c1! value_expr1 is x := value_expr1 (x := c1? |^| c2! value_expr2) ++ c1! value_expr1 is (x := value_expr1) |^| stop

, : 1. (b!2) || (y := a?) || if (x := 1); (a!x); (true |^| false) then a!(b?) else a!(1 + b?) end
2. (b!2) || (x := a?) || if (a!3; true) |^| ((a!b? + 5); false) then a!(b?)
else a!(1 + b?) end || (a!0)

3. (if (a?) > 0 then b!1 else b!2 end ++( a!1; x := b?; b!4)) ||
(y := if (b?) = 1 then a? else (0 - a?) end) || (a!0)

4. a!(5 + b?) || ((x := (if true |^| false then x := b?; 1 else b!3; x := 2; 6 end) + x) ++
(b!4 || y := b?))

5. a!(5 + a?) || ((x := (if true |^| false then x := b?; 1 else x := b?; 6 end)) ++
(b!4 || x := a? || a!3 || y := b?))

56


6. case (1 |^| b?) of
1 2 3 4 5 end || -> x : -> x : -> y : -> y : -> x : a!1 || = a? + 1, = b?, = a? + 3, = b? + a?, = y := a?; y b!(a? + 2) || a!3

7. case (1 |^| b?) of
1 2 3 4 5 end || -> x -> x -> y -> y -> x a!0 := a? + 1, := b? |^| a?, := a? + 3, := b? + a?, := y: = a?; y || b!(a? + a?) || a!2 || a!3

8. case (a?) of
0, 1 -> x := a? + 1, 2 -> x := b?, 3 -> y := a? + 3, 4 -> y := b? + a? end || (x := a?; a!0 |=| b!(a?)) || a!4

57


10.
. . case- let-. . , , , , . , , - . , , RSL , ( ) . . , , . , : · - - ; · - · - · - . , . , /, . , . , , , , , , , . - , . , . , , , - . , . - , , , . . ,
58


. , , , . , . , , , , ­ . , , , , . , , , . , . , . ? , . -, , . -, . . , , . ( ) , , , (, ). . , , , . RSL . , ­ . :
value x : Int, y : Int :- y ~= 0 axiom y ~= 3

x . y 0 3.

59


value f : Int -> Int axiom forall x : Int :- f(x) > x

f , . , f . , , .

:
value f : Int -~-> Int axiom forall x : Int :(f(x) = x-1) \/ (f(x) = x) \/ (f(x) = x+1)

f , , . , , , . f.

value f : Int -~-> Int f(x) is let y : Nat :- x-1 <= y /\ y <= x+1 in y end value f : Int -~-> Int f(x) is x-1 |^| x |^| x+1

f, .

, () - . , f1 ( ):
value f1 : Int -> Int f1(x) as r post (r <= x+1) /\ (r >= x-1)

? : · · let- · case- let- record pattern · , , .
60


, ( ), , . . ­ , , (total):
value f : Int -> Int f(x) is 0 |^| 1 |^| 2

:
value f : Int -~-> Int f(x) is 0 |^| 1 |^| 2

­ « », :
value x : Int = 0 |^| 1 |^| 2

Value-expression RSL . , , , - , . , :
axiom let b : Bool in b end

­ ­ false.

false, , axiom . :
exists x : Char :- let y : Char in y end

false, . , :
{ x | exists x : Char :- let y : Char in y end }





. , let-. case- let- case- let-. , empty add:
type Set == empty | add(Elem, Set) axiom forall e, e1, e2 : Elem, s : Set :[no_duplicates] add(e, add(e,s)) is add(e,s) [unordered]

61


add(e1, add(e2,s)) is add(e2, add(e1,s))

,
Set () . , x ­ Set x empty


let add(x, y) = s in x end


case s of add(x, y) -> x end

, Set , , , , s= add(a, add(b, empty), [unordered], , s= add(b, add(a, empty ). , let, case a, b, ­ . 1. , . 2. , . ( ). 3. , . 4. ?
(a!1) || (b!1) || (x:=a?) || (x:=b?) ((a!1) || (b!1)) |=| ((x:=a?) || (x:=b?)) (a!1) || (b!1) || ((x:=a?) |=| (x:=b?))

5. case- let-,

. , , |^|.

62


11.
. . . RSL : - - , - - , - . , . . , .
1. ­ ­ .

: / , , (, ..), , , . : (, , ), (, ), (, ).

2. .

3. .

, , , , . , (, ).
63


4. .

, (, ). , , , , . (, ).
5. .

, . , , , , . / , (, , ..).
6. .

( ), . / , (, ..) (, , ). , , . / , , (, ..).

7. .

8. .

.

. , .
64


. . .
9. .

: , , , , (, , ). , , (, - N , ..)
10. .

, , . . , , . . , , .. , , - , .
11. .

, , ( , ), N , , . ( , ) / . , .. , . , , (, ).

65


12. .

, (, /, , , / ), / , ( ) . : , , / . , , .
13. make.

, , (, ). . , ( ), . ­ . - : «» , . 14. . , . , . / , / (, ..) 15. . , 0 . , . , , , , (, ..). 16. . . (, ..), . (/ , /
66


) (, , ..) 17. . . (, , ), , , , , . ­ / , (, ), ( , , ..) 18. . . , . , , , ( , , ). . , (, ), (, / , ..). (), . (, , ). - . RSL , . , , .. , . : · ( RSL ),
67


· , · . , () . , , , , .. . , RSL , . -, is_wf_system(sys), . , « », . is_wf_db(rs) , , « » , .. .
type Key, Data, Record = Key >< Data, DataBase={| rs : Record-set :- is_wf_db(rs)|} value is_wf_db : Record-set -> Bool is_wf_db(rs) is (all k : Key, d1,d2 : Data :((k,d1) isin rs /\ (k,d2) isin rs) => d1 = d2)

, , . , . , . :
value add : Key >< Data >< DataBase -~-> DataBase add(k,d,db) as res post (k,d) isin db pre (k,d) ~ isin db

68


, .. (k,d) db. , , , add db, , , (k,d) db res .

69


12.
1.

1. explicit . implicit- .
value f : Int >< Int -> write x read y 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:=y; c else 0-c end)) else (a+b, x:=b; a-b) end : value f : Int >< Int -> write x read y Int >< Int f(a,b,c) as (d, e) post if a=b then if a+b>c then if c>0 then d=c /\ x=y /\ e = a*b*c else d=c /\ x=x' /\ e=a*b*(0-c) end elseif c>0 then d=a+b /\ x=y /\ e= a*b*c else d=a+b /\ x=x` /\ e=a*b*(0-c) end else d=a+b /\ x=b /\ e=a-b end

2. (explicit) (implicit) ( ), :
type S, E value create : Unit -> S, add : E >< S -> S, del : S -~-> S, next : S -~-> S, get : S -~-> E, append : S >< S -> S axiom all e : E, s : S :del( add( e, s ) ) is s, all e : E, s : S :get( add( e, s ) ) is e, all e : E, s : S :next( add( e, s )) is if s = create( ) then add( e, s ) else append ( s, add( e, create( ) ) end, all e : E, s1, s2 : S :append( create(), s2 )) is s2, all e : E, s1, s2 : S :append( add(e, s1), s2 )) is add (e, append (s1, s2))

: type S, E value create : Unit -> S create is <..>,

70


add : E >< S -> S add (e,s) is <.e.> ^ s, del : S -~-> S del (s) is tl s pre s~=<..>, next : S -~-> S next (s) is tl s ^ <. hd s .> pre s~= <..>, get : S -~-> E get (s) is hd s pre s ~= <..>, append : S >< S -> S append (s1, s2) as s post if s1=<..> then s=s2 else s=add(hd s1, append( tl s1, s2)) end

3. , ( ) .
value f1 : M f2 : M f3 : E f4 : E axiom in f3(a1,p) /\ f3(b1,q) /\ f3(a2,p) /\ f3(b2,q) end is true : [ l f i [ l f i [ l f i [ all]] et (p, q) = f2(f1(f4(a1, b1), f4(a2, b2))) in 3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end s true [ f4]] et (p, q) = f2(f1([a1 +>b1], [a2+>b2])) in 3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end s true [ f1]] et (p, q) = f2([a1 +>b1, a2+>b2]) in 3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end s true type >< -> >< >< M -> M, S >< S, S -> Bool, E -> M M = E ­m-> E, S = E-set value f1 : M >< M -> M f1(m1,m2) is m1 !! m2, f2 : M -> S >< S f2(m) is (dom m, rng m), f3 : E >< S -> Bool f3(a,b) is a isin b, f4 : E >< E -> M f4(a,b) is [a +> b]

all a1, a2, b1, b2 : E :let (p,q) = f2(f1(f4 (a1,b1), f4(a2,b2)))

71


[ l f i

[ f2]] et (p, q) = if a1=a2 then ({a1, a2}, {b2}) else ({a1, a2}, {b1, b2}) end in 3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end s true

[[ f3]] let (p, q) = if a1=a2 then ({a1, a2}, {b2}) else ({a1, a2}, {b1, b2}) end in a1 isin p /\ b1isin q /\ a2 isin p /\ b2 isin q end is true [[]] let (p, q) = ({a1, a2}, if a1=a2 then {b2} else {b1, b2} end in a1 isin p /\ b1isin q /\ a2 isin p /\ b2 isin q end is true [[ let]] a1 isin {a1, a2} /\ b1 isin if a1=a2 then {b2} else {b1, b2} end /\ a2 isin {a1, a2} /\ b2 isin if a1=a2 then {b2} else {b1, b2} end end is true [[]] true /\ b1 isin if a1=a2 then {b2} else {b1, b2} end /\ true /\ b2 isin if a1=a2 then {b2} else {b1, b2} end end is true [[ /\ ]] b1 isin if a1=a2 then {b2} else {b1, b2} end /\ b2 isin if a1=a2 then {b2} else {b1, b2} end end is true [[ if]] b1 isin if a1=a2 then {b2} else {b1, b2} end /\ true is true [[ /\ ]] b1 isin if a1=a2 then {b2} else {b1, b2} end is true [[ case]] [[non_eq]] ~a1=a2 [[eq]] a1=a2 [[ non_eq ]] ~a1=a2 b1 isin {b1, b2} is true [[ ]] true is true true [[ eq ]] a1=a2 b1 isin {b2} is true [[]]

72


false is true false : , .

4. :
type Elem, Collection == empty | add (Collection <-> head, first:Elem, Elem <-> new_second)

.
: type Elem, Collection value empty : Collection, add : Collection >< Elem >< Elem -> Collection, head : Collection >< Collection -~-> Collection, first : Collection -~-> Elem, new_second : Elem >< Collection -~-> Collection axiom [disjoint] all c,c1 ; Collection, e1, e2 ; Elem :empty ~= add(c, e1, e2) [induction] all isCollection ; Collection -> Bool :isCollection(empty) /\ (all c1 : Collection, e1, e2 ; Elem :- (isCollection(c1) => isCollection(add(c1, e1, e2)))) => (all c2 : Collection :- isCollection ( c2 )) [head_add] all c1, c2 ; Collection, e1, e2 : Elem :- head (c1, add(c2, e1, e2)) is add(c1, e1, e2)) [first_add] all c: Collection, e1, e2 : Elem :- first (add(c, e1, e2)) is e1 [new_second_add] all c: Collection, e1, e2, e3 : Elem :- new_second (e1, add(e2, e3)) is add(c, e2,e1)

73


2.

1. explicit . implicit- .
value f : Int >< Int -> write x read y Int >< Int >< Int f (a, b) is local variable v : Int := 0 in x:=0; for i in <.a..b.> do x:=x+y; v := v+2*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 a = c /\ b = d /\ if a > b then e = y /\ x = 0 else x = y * (b-a+1) /\ e = (a+b)*(b-a+1)+y end

2. explicit implicit ( ), :
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

74


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]

75

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

76



1.1. 1.2. (b) (a) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (a) (b) type ST = {| n : Int:- n \ 2 = 1 |} false ( (1)) a 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.3.

: if a then ( a is chaos) else false end ( (3))

1.4.

(a) ( i j = -i) (b) ( , , i > 0) (c)
(a) (d) (a) (a) all i : Int :- exists j : Int :- j > i exists k : Nat :-n = k * k (exists i : Int :- all j : Int :- i >= j)

1.5. 2.1. 2.2.

type Points = {| (x, y) : Real >< Real :- x >= 0 /\ y >= 0 /\ y >= x |} 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) (b)

(c)

value max : Int >< Int -> Int max(i, j) is if i >= j then i else j end value max : Int >< Int -> Int max(i, j) as y post (y = i /\ y >= j) \/ (y = j /\ y >= i) value max : Int >< Int -> Int axiom all i,j : Int :- max(i, j) is if i >= j then i else j end type Complex = Real >< Real value zero : Complex = (0.0,0.0) value c : Complex :- let (x, y) = c in x = y end

2.4.

(a)

(b) (c)

77


(d)

(e)

value add : Complex >< Complex -> add((x1,y1), (x2,y2)) is (x1 + x2, y mult : Complex >< Complex -> mult((x1,y1), (x2,y2)) is (x1 x2 - value f : Complex -> Complex f(c1) as c2 post c1 ~= c2

1

Complex + y2), Complex y1 y2, x1 y2 + y1 x2)

2.5.

(a)

(b)

type Circle = Center >< Radius, Center = Position, Radius = {| r : Real :- r >= 0.0 |} 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 value circle : Circle = (origin, 3.0) value pos : Position :- on_circle(circle, pos)

(c) (d) 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 (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

2.8.

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)

3.2.
3.3.

card { n | n : Nat :- 30 \ n = 0} = card {1, 2, 3, 5, 6, 10, 15, 30} = 8 card { (x, y) | x, y : Int :- x * x + y * y < 25 }

78


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 ~= { }

3.5.

(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)),

79


/ 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)) 4.1 4.2. (a) (b) (a) 169 chaos <.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.

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.> 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)) type Elem value (a) length : Elem-list -> Nat length(k) is if k = <..> then 0 else 1 + length(tl k) end

4.4.

4.5.



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 (b) rev : Elem-list -> Elem-list

80


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.>.> (c) 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-> del(k, e) is <.x | x in k :- x (d) number_of : Elem-list >< number_of(k, e) is card {i 4.7. Elem-list ~= e.> Elem-> Nat | i : Nat :- i isin inds k /\ k(i) = e}

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 (b)

5.1.

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

scheme MAP_UNIVERSITY_SYSTEM = class type Student, Course, CourseInfos = Course -m-> Student-set, University = Student-set >< CourseInfos value /* hasStudent , */ hasStudent : Student >< University -> Bool hasStudent(s, (ss, cis)) is s isin ss, / hasCourse , */ hasCourse : Course >< University -> Bool hasCourse(c, (ss, cis)) is c isin dom cis, / studOf , / studOf : Course >< University -~-> Student-set studOf(c, (ss, cis)) is cis(c)

81


pre hasCourse(c, (ss, cis)), / attending , / attending : Student >< University -~-> Course-set attending(s, (ss, cis)) is {c | c : Course :- c isin dom cis /\ s isin cis(c)} 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 +> cis(c) \ {s} | c : Course :- c isin dom cis ]) pre hasStudent(s, (ss, cis)), / newCourse / newCourse : Course >< University -~-> University newCourse(c, (ss, cis)) is (ss, cis !! [c +> {}]) pre ~hasCourse(c, (ss, cis)), / delCourse / delCourse : Course >< University -~-> University delCourse(c, (ss, cis)) is (ss, cis \ {c}) pre hasCourse(c, (ss, cis)) end 6.1. scheme STACK_ALG = class type Elem, Stack value empty : Stack, push : Elem >< Stack -> Stack, pop : Stack -~- Stack, is_empty : Stack -> Bool, top : Stack -~-> Elem axiom [ 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 s end

82


6.3.

scheme STACK_LIST = class type Elem, Stack = Elem-list value empty : Stack = <..>, push : Elem >< Stack -> Stack push(e,s) is <. e .> ^ s, pop : Stack -~- Stack pop(s) is tl s pre s ~= empty, is_empty : Stack -> Bool is_empty(s) is s = empty, top : Stack -~-> Elem top(s) is hd s pre s ~= empty end

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

6.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 end

83


[[ if]] true 7.1. type Record = = new_record(key_of : Key, data_of: Data)

:
type Record value new_record : Key >< Data -> Record, key_of : Record -> Key, data_of : Record -> Data axiom all 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)) = d 7.2. 7.3. type Stack = = empty | push(top : Elem, pop : Stack) (b) type Tree value empty : Tree, node : Tree >< Elem >< Tree -> Tree, left : Tree -~-> Tree, val : Tree -~-> Elem, rigth : Tree -~-> Tree axiom [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 t2 x := 2 x := 2; 3 x := 1; 3 scheme I_STACK_EX = class type Elem variable st : Elem-list value empty : Unit -> write st Unit empty() is st := <..>, push : Elem -> write st Unit push(e) is st := <. e .> ^ st, pop : Unit -~-> write st Unit

8.1.

(a) (b) (c) (a)

8.2.

84


pop() is st := tl st pre st ~= <..>, is_empty : Unit -> read st Bool is_empty() is st = <..>, top : Unit -~-> read st Elem top() is hd st pre st ~= <..> end 8.2. (b) scheme I_STACK_IM = class type Elem variable st : Elem-list value empty : Unit -> write st Unit empty() post st = <..>, push : Elem -> write st Unit push(e) post st = <. e .> ^ st', pop : Unit -~-> write st Unit pop() post st = tl st' pre st ~= <..>, is_empty : Unit -> read st Bool is_empty() as b post b = (st = <..>), top : Unit -~-> read st Elem top() as e post e = hd st pre st ~= <..> end variable result : Real value fract_sum : Nat -~-> write result Unit fract_sum(n) is local variable counter : Nat := n in result := 0.0; while counter> 0 do result := result + 1.0 / (real counter); counter := counter ­ 1 end end pre n > 0 Int

8.3.

(a)

8.4.

(a) value f : Int >< Int >< Int -> write x, y Int >< f(a,b,c) as (d, e) post if a = b then y = y' /\ (if a + b > (if > 0 then x =c /\ else (x = x' /\ y =a + b /\ x := 1; (y := 1) ; (a!2) |^| x := 1; (y := 1) ; (a!3) x := 3 || a!2 || a!0 |^| x := 0 || a!3 ; a!2 |^| x := 7 ; a!(1 + b?) || a!0 |^|

then d = else x = y /\ d = a + b end) /\ d = b * else x = x' /\ d = b * (0 ­ ) end) d = a + b /\ e = a - b) end

9.1. 9.2.

85


x := 0 || a!7; a!(1 + b?) 9.3. 9.6. x := 1; y := 0 x x y y := := := := 2 || b!5 |^| 4 || b!3 |^| 1; x := 1 |^| 6

86



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_material

" ,

87



.................................................................................................................................... 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. ..............................................................35 ...............................................................................35 , ...............36 .......................................................36 RAISE . .....................................37 ...................................................................................... 38 ..............................................................................................................................39 7. ...........................................................................41 ........................................................................................41 . , ...........41 -................................................................................................... 41 ........................................................................................................ 42 88


......................................................................................................................... ................................................................................................................... .............................................................................................................................. 8. .................................................. ...................................................................... ............................................................................................................. ....................................................................................................... ...................................................................................... RSL........................................................................................... ........................................................................................ if........................................................................................................................ ............................................................................................................ while............................................................................................................................. until.............................................................................................................................. for................................................................................................................................. ......................................................................................... ..................................................... .............................................................................................................................. 9. ........................................ ..................................................................................... .............................................................................................. ................................................................................................... ................................................................................. ................................................................................................. .................................................................................................................... ............................................................................................................... (interlock)........................................................................................ .................................................................................. .............................................................................................................................. 10. ......................................................... ......................................................... ..................................................................... case- let-.............................................................................. .............................................................................................................................. 11. .................................................................................................... ................................................................................................................... .................................................................................................................... ................................................................................................. 12. .................................................... .......................................................................... .............................................................................................................................

42 43 44 45 45 45 46 46 46 46 47 47 47 48 48 48 49 49 51 51 51 52 53 53 53 54 55 56 56 58 58 60 61 62 63 63 63 67 70 77 87

89