Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://sp.cs.msu.ru/courses/fmsp/rslbook99.pdf Äàòà èçìåíåíèÿ: Thu Dec 8 02:40:02 2011 Äàòà èíäåêñèðîâàíèÿ: Mon Oct 1 21:40:30 2012 Êîäèðîâêà:

..


.. , ..

RSL
( )

1999


2



« ». . , RAISE , , RAISE . - . , , . SDL MSC. . , , , . , , . , , . , , , , . , , , , , . , . . , , , , , , , : . RSL. RAISE - Rigorous Approach to Industrial Software Engineering. RAISE
3


, 80- , , . RSL, , , VDM/Meta-IV, Z, LOTOS, CSP, , , . RSL . , RAISE . [1]. , . RSL. , , . RSL, , , - - , , .

4


1. RSL
1.1. RSL. RSL

- RSL, RSL . RSL . 1.1.1. RSL RSL : Bool ­ , Int ­ , Nat ­ , Real ­ , Char ­ , Text ­ , Unit ­ (). Bool true false, , , , , , . Int , , , /, , \, abs, real, , \ ­ , abs ­ real ­ Int Real. , , , , , . Nat Int : Nat = { i : Int · i 0 }. , Int. Real , , , /, , , , , , , , abs, int, int ­ Real Int, 0 . : int 4.6 = 4 int 4.6 = 4 (1 .0, 12.35 ..). Char , , Char ( : f, Z .. ). Text , . , ABC, ­ . , .

5


Unit . 1.1.2. RSL RSL, . RSL chaos, () , - , - . chaos RSL , . , 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

6

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

a



b

, , RSL , .. e1 e2 e2 e1 e1 e2 e2 e1 . RSL , : if value_expr then value_expr1 else value_expr2 end, value_expr , value_expr1 value_expr2 , . : if true then expr1 else expr2 end expr1 (1) if false then expr1 else expr2 end expr2 (2) if a then expr1 else expr2 end if a then expr1[true/a] else expr2[false/a ] end (3) if chaos then expr1 else expr2 end chaos (4) expr1[true/a] expr1 true a. RSL . : , , .
1.

, . RSL?
(a) (b) (c) (d) (e) (f)

(a) a true a true a true true a true true a b a b a a true
7


(g) (h) (i) (j) (k)

(a (a (a (a (a



a) false b) c a (b c) b) c a (b c) a) true a) true

: 1.1.2 ; , chaos. , (c): chaos true chaos, (chaos true) false , (c) RSL.
2. : (a) if true then false else chaos end ? (b) if a then ( a chaos) else false end ?

: (1) - (4) 1.1.2.
3.

?
(a) (b) (c)

i : Int · j : Int · i+j 0 i : Int · j : Nat · i+j 0 i : Int · j : Int · i+j 0

4.

RSL , , . : RSL. , , . is_even : Nat Bool is_even(n) ... : . \ ( )

5.

8


1.2.



- RSL , . RSL (explicit), (implicit) (axiomatic) . 1.2.1. ( products ) , , , : (1,2) (1,true,John). , .. (1,2) (2,1) . , , : type_expr1 ... type_exprn, n2. n (v1,...,vn), vi ­ type_expri. : (true,p q) : Bool Bool (x + 1, 0, this is a text) : Nat Nat Text = . 1.2.2. RSL , , value. (value definition) RSL : (explicit), (implicit), . , . , RSL- : value x : Int = 1 x=1. , , . : value x : Int · x > 0
9


x, . . (under-specification) , - . , , . , , . , x : value x : Int axiom x 1 ( ), value x : Int axiom x > 0 ( ). 1.2.3. RSL , .. , , . 1.2.3.1.

f, T1 T2, (total function), T1 f T2, .. f : x : T1 · ! y : T2 · f(x) y f : f : T1 T2 . f, T1 T2, (partial function), v T1, f(v) ( f(v) chaos), , f v T2. f : f : T1 T2 .

10


. 1.2.3.2.

(explicit function definition) , . RSL : value f : Int Int f(x) x + 1 p(x), 1/x: value p : Real Real p(x) 1.0/x pre x 0.0 , . 1.2.3.3.

(implicit function definition), , , , .. , . , , , , . 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

11


, , . 1.2.3.4.

, , , , . , , , . , (, f(g(x), x) h(x)), .. . f(x), : value f : Int Int axiom x : Int · f(x) x + 1 square_root(x), : value square_root : Real Real axiom x : Real · x 0.0 s : Real · square_root(x) = s /\ s s = x /\ s 0.0 1.2.3.5.

, : 1. ; 2. : (a) , (b) , (c) : ( ), ( ) ; 3. : (a) ( ), (b) ( ),

12


(c) ( ,

).
1. : (a) `Complex' , (b) `zero' 0 + 0i, (c) `c', x + xi; (d) `add' `mult'

, `f', , . : (b) (d) (explicit) , .. ; (c) (e) (implicit) , ; (c) (d) let. , , (c) c : let (x, y) = c in x = y end 2. : SYSTEM_OF_COORDINATES= class type Position = Real Real value origin : Position = (0.0,0.0), distance : Position Position Real distance((x1, y1),(x2, y2)) ((x2 ­ x1)2.0 + (y2 ­ y1)2.0)0.5 end `Position' , `origin' , `distance' . , `origin' `distance' (explicit definition), .. .
(e)

13


: (a) `Circle' ; (b) `on_circle', ; (c) 3.0 ; (d) `pos' , . : (a) `Center' `Radius' , `Center' `Position', `Radius' : Radius = { r : Real · r 0.0 }, ; (b) (c) (explicit definition), let ; (d) (implicit) .
3.

`max', , : (a) , (b) , (c) . : , 1.2.3.5; RSL if _ then else end. `approx_sqrt', `eps' ( ) . , square_root(x) [approx_sqrt(x,eps),approx_sqrt(x,eps) + eps[. : , .. ; , , .. .

4.

14


5. :

value f : Int Int f(x) f(x) ? (a) value f : Int Int f(x) chaos

(b) value f : Int Int f(x) 1 (c) value f : Int Int f(x) 1

: ; , .

1.3.



- RSL . . 1.3.1. . : {1,3,5} {Mary,John,Peter} , , {1,3,5}, {5,3,1} {3,5,1,1} . RSL type_expr-set type_expr-infset ,

15


type_expr . , Bool-set : {} {true} {false} {true, false}, {}. type_expr-infset , , type_expr. , T T-set T-infset. , Nat-infset ( ) . RSL : ,,\,,,,,, card, . card , .. : card : T-infset Nat card chaos. : card {1,4,56} = 3 card {} = 0 card {n n : Nat} chaos 1.3.2. , , , , {v1,...,vn}, n0. , , , , ( ). , {3 .. 7} {3,4,5,6,7}, {3 .. 3} ­ {3} {3 .. 2} ­ {}. , , , : { value_expr set_limitation }, (compehended) , value_expr , set_limitation ­ , . : {2n n : Nat · n 3}, {0,2,4,6}.

16


1. , , 0 10. : : .
2.

( ): scheme UNIVERSITY_SYSTEM = class type Student, Course, CourseInfo = Course Student-set, University = Student-set CourseInfo-set value allStudents , allStudents : University Student-set, hasCourse , hasCourse : Course University Bool, numberOK true, 5 100 numberOK : University Bool, studOf , studOf : Course University Student-set, attending , attending : Student University Course-set, newStud newStud : Student University University, dropStud dropStud : Student University University end , .

17


: .
3. ?

1.4.



- RSL . . 1.4.1. , : 1,3,3,1,5 true,false,true . , .. 1,3,5 5,3,1 (1,3,5 5,3,1). , ( ), 1,3,3,1,5 1,3,5. RSL type_expr*, type_expr . , Bool* ( ) . type_expr , type_expr. , T, T* T. 1.4.2. , . , . v1,...,vn, n0 vi , , . , , .. v1..v2, v1 v2 , v1 v2 . : 3..7 3,4,5,6,7 3..3 3 3..2

18


(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 , . , , , : value all_natural_numbers : Nat axiom all_natural_numbers(1) = 0, idx : Nat · idx 2 all_natural_numbers(idx) = all_natural_numbers(idx 1) 1 . , , , : n n in all_natural_numbers · is_a_prime(n)

19


1.4.3. RSL : ^ : T* T T hd : T T tl : T T len : T Nat elems : T T-infset inds : T Nat-infset ^ , . hd tl , . len , chaos. elems , . , L card elems L. inds . , fl: inds fl = {1 .. len fl}, il: inds il = {idx idx : Nat · idx 1}. 1. : (a) `length' ­ len, (b) `rev' ­ . : hd tl; case.
2.

`pascal', n . n , . , n = 5 : 1 1 , 1 1 , 2 , 1 1 , 3 , 3 , 1 1 , 4 , 6 , 4 , 1
20


k- (k1) 1, i- (1ik) (i1)- i- (k-1)- . : N1 ; ^; .
3.

: , - . `PAGE', : (a) `Page', 'Line', 'Word' , , (b) `is_on', , , (c) `number_of', . : (a) `Page' 'Line', (b) inds elems, (c) ( , ), , card.

1.5.

(maps)

- (map), RSL . . 1.5.1. , , (domain) , , , (range). : [3 true, 5 false]

21


[Klaus 7, John 2, Mary 7] Bool, ­ Text Nat. () {3,5}, ­ {true,false}, {Klaus,John,Mary} {2,7}. : type_expr1 m type_expr2 , , . : [v1 w1,...,vn wn], : [v1 w1,...,vn wn,...], n 0, vi wi ­ type_expr1 type_expr2 . . : vi vj wi wj , vi vj ­ . , Nat m Bool Text m Nat . : [3 true,3 false], Nat m Bool. 1.5.2. RSL , , : . , : [v1 w1,...,vn wn], n 0. , n 0 []. . , , , : [3 true,5 false] [5 false,3 true] ( ).

22


(comprehended map expression) , : [ value_expr_pair set_limitation ], value_expr_pair , set_limitation () . , : [ n 2n n : Nat · n 2 ] [ n 2n n : Nat ] [0 0,1 2,2 4].

[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, ^ . 1.5.3. : dom : (T1 m T2) T1-infset rng : (T1 m T2) T2-infset : (T1 m T2) (T1 m T2) (T1 m T2) : (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) dom , . : dom [3 true, 5 false, 5 true] {3,5} dom [] {} dom [ n 2n n : Nat ] { n n : Nat }

23


rng . , , , .. , , . : [3 true, 5 false] [5 true] [3 true, 5 true] [3 true] [5 false] [3 true, 5 false] [3 true] [] [3 true] : ,

[3 true, 5 false] [5 true] [3 true, 5 false, 5 true] \ / , : \

, / , , , . : m \ s [d m(d) d : T1 · d dom m d s] m / s [d m(d) d : T1 · d dom m d s] : [3 true, 5 false] \ {5,7} [3 true] [3 true, 5 false] / {5,7} [5 false] [3 true, 5 false] \ {3,5,7} [] [3 true, 5 false] / {3,5,7} [3 true, 5 false] , .. m1 m2 : m1 m2 [x m1(m2(x)) x : T1 · x dom m2 m2(x) dom m1] : [3 true, 5 false] [Klaus 3, John 7] [Klaus true] [3 true] [Klaus 5] []

24


1. ( ): scheme MAP_UNIVERSITY_SYSTEM = class type Student, Course, CourseInfos = Course m Student-set, University = Student-set CourseInfos value allStudents , allStudents : University Student-set, hasCourse , hasCourse : Course University Bool, numberOK true, 5 100 numberOK : University Bool, studOf , studOf : Course University Student-set, attending , attending : Student University Course-set, newStud newStud : Student University University, dropStud dropStud : Student University University end , . : .

25


2.
RSL . .

2.1.



RSL: . , . . , .

2.2.



1. ­ ­ . : / , , (, ..), , , . 2. . : (, , ), (, ), (, ). 3. . , ,
26

, , .

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

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

27


7. / . ( ), . / / , (, ..) (, , ). 8. . , , . / , , (, ). 9. . . , . , . . . . 10. . : , , , , (, , ). , , (, - N , ..) 11. . , , . . , , . .

28


, , .. , , - , . 12. . , , ( , ), N , , . ( , ) / . , .. , . , , (, ). 13. . , (, /, , , / ), / , ( ) . : , , / . , , . 14. . , , , , , , . 15. make. , , (, ). . ,

29


( ), . ­ . - : «» , .

2.3.



(), . , . , , .. , . : , . , () . , , , . , RSL , . , , . , .

30


3. eden
RAISE ­ eden (entity editor), RSL. Computer Resources International ­ CRI.

3.1.



eden , .. RSL . UNIX. . () ( RSL), (.. ) , . ( ) , . , , . , . , , .. ( ). QUEUE, : QUEUE class type Element, Queue Element* value empty : Queue , enq : Element Queue Queue enq(e,q) q ^ e,

31


deq : Queue Queue Element dec(q) (tl q,hd q) pre q empty end UNIX . : raise_eden QUEUE, QUEUE ­ . , , 1.

. 1

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

32


lib_module, ( ). . , . , ( ), , RSL.

3.2.



. 2.

. 2

, , , , . , , , .

33










: transforms ­ RSL, . , , .. , . edit ­ , . errors ­ , .. . save ­ , , ( , write) ( save). file ­ ( ) , , ASCII . exit ­ .

3.3.



1. lib_module, ( ). transforms lib_scheme, .. RSL. 3. , , . class_expr, . , class_expr. eden . , . .

34


. 3

, class end . , , , . ^B () ^F (), Delete , ^D. , , . ( RETURN) , , , QUEUE . class . 4.

35


. 4

, ( ) class_expr . , (. . 3) basic_class_expr . RETURN, . 5. RETURN ( decl_string) type_decl. 6.

36


. 5

. 6

37


Element ( ) RETURN. ( ) (. . 7).

. 7

3.4.



. , , , Queue RETURN. 8.

38


. 8

, , . . -, , , , . -, undo edit , ( , ) . , . , T RETURN. 9.

39


. 9

9 , , ( RETURN) , . T , , . ( T) cut-to-clipped edit . ( type_expr), . delete_selection . , undo , .. . Queue Element. list_type_expr finite_list_type_expr.
40


Element RETURN. 10.

. 10

3.5.



. RETURN, (. . 11) value_decl . value value_def .

41


. 11

QUEUE , , . : ­ ( ) ( ); ­ ESC ^B; ­ ESC RETURN. , . explicit_value_def, value_def, explicit_function_def.
42


, QUEUE , value_expr RETURN. 12.

. 12 . . write-file save . QUEUE.rsl . exit. QUEUE.rsl . , ( QUEUE) . eden .

43


1
1.1. (a ) (b) (c) (d) (e) (f) (g) (h) (i) (j) (k) (1) 1.1.2.) a a a a then then then then ( a chaos) else false end ( (3)) ( true chaos) else false end true else false end ( (3)) a else a end a

1.2.

(a) false ( (b) a : if if if if

1.3.

(a) ( i j i) (b) ( , , i 0) (c) i : Int · j : Int · j i ( i : Int · j : Int · i j)

1.4. 1.5.

is_even : Nat Bool is_even(n) ( m : Nat · n 2 m) : is_even : Nat Bool is_even(n) n \ 2 0 (a ) (b) (c) (d) type Complex Real Real value zero : Complex (0.0,0.0) value c : Complex · let (x,y) = c in x = y end value add : Complex Complex Complex add((x1,y1), (x2,y2)) (x1 x2, y1 y2), mult : Complex Complex Complex mult((x1,y1), (x2,y2)) (x1 x2 y1 y2, x1 y2 y1 x2) (e) value f : Complex Complex f(c1) as c2 post c1 c2

2.1.

44


2.2.

(a) type Circle Center Radius, Center Position, Radius = { r : Real · r 0.0 } (b) value on_circle : Circle Position Bool on_circle((c,r), p) distance(c,p) = r : value on_circle : Circle Position Bool on_circle(circ, p) let (c,r) = circ in distance(c,p) = r end (c) value circle : Circle = (origin, 3.0) (d) value pos : Position · on_circle(circle, pos) (a) value max : Int Int Int max(i,j) if i j then i else j end (b) value max : Int Int Int max(i,j) as y post (y = i y j) (y j y i) (c) value max : Int Int Int axiom i,j : Int · max(i,j) if i j then i else j end value approx_sqrt : Real Real Real approx_sqrt(x, eps) as s post s 2 x x (s eps) 2 pre x 0.0 eps 0.0 : value f : Int Int f(x) f(x)

2.3.

2.4.

2.5.

45


: value f : Int Int axiom x : Int · f(x) f(x), : value f : Int Int
, ( , ) Int Int.

3.1. 3.2.

{1,3,5,7,9} {s s : Nat · (s 10) ( n : Nat · s 2 n)} scheme UNIVERSITY_SYSTEM = class type Student, Course, CourseInfo = Course Student-set, University = Student-set CourseInfo-set value allStudents : University Student-set allStudents(ss, cis) ss, hasCourse : Course University Bool hasCourse(c, (ss, cis)) ( (c, ss) : CourseInfo · (c, ss) cis c = c), numberOK : University Bool numberOK(ss, cis) ( (c, ss) : CourseInfo · (c, ss) cis (card ss 100 card ss 5)), studOf : Course University Student-set studOf(c, (ss, cis)) {s s : Student · ss : Student-set · s ss (c, ss) cis } pre hasCourse(c, (ss, cis)), attending : Student University Course-set attending(s, (ss, cis)) {c c : Course · ss : Student-set · (c, ss) cis s ss} pre s allStudents(ss, cis), newStud : Student University University newStud(s, (ss, cis)) (ss {s}, cis) pre s ss,

46


dropStud : Student University University dropStud(s, (ss, cis)) (ss \ {s}, {(c, ss \ {s}) (c, ss) : CourseInfo · (c, ss) cis }) pre s ss end 4.1. type Elem value (a) length : Elem* Int length(k) if k then 0 else 1 length(tl k) end length : Elem* Int length(k) card (inds k) length : Elem* Int length(k) case k of 0, i ^ lr length(lr) 1 end (b) rev : Elem* Elem* rev(k) if k then else rev(tl k) ^ hd k end rev : Elem* Elem* rev(k) k(len k i 1) i in 1 .. len k rev : Elem* Elem* rev(k) case k of , i ^ lr rev(lr) ^ hd k end 4.2. type N1 { n : Nat · n 1 } value pascal : N1 (N1*)* pascal(n) if n 1 then 1 else let p pascal(n 1) in p ^ 1 ^ p(n 1) (i 1) p(n 1) (i) i in 2 .. n 1 ^ 1 end end

47


4.3.

scheme PAGE class type Page Line*, Line Word*, Word value is_on : Word Page Bool is_on(w, p) ( i : Nat · i inds p w elems p(i)), number_of : Word Page Nat number_of(w, p) card {(i, j) i, j : Nat · i inds p j inds p(i) w p(i)(j)} end scheme MAP_UNIVERSITY_SYSTEM = class type Student, Course, CourseInfos = Course m Student-set, University = Student-set CourseInfos value allStudents : University Student-set allStudents(ss, cis) ss, hasCourse : Course University Bool hasCourse(c, (ss, cis)) c dom cis, numberOK : University Bool numberOK(ss, cis) ( c : Course · c dom cis (card cis(c) 100 card cis(c) 5)), studOf : Course University Student-set studOf(c, (ss, cis)) cis(c) pre hasCourse(c, (ss, cis)), attending : Student University Course-set attending(s, (ss, cis)) {c c : Course · c dom cis s cis(c)} pre s allStudents(ss, cis), newStud : Student University University newStud(s, (ss, cis)) (ss {s}, cis) pre s ss, dropStud : Student University University dropStud(s, (ss, cis)) (ss \ {s}, [ c cis(c) \ {s} c : Course · c dom cis ]) pre s ss end

5.1.

48



RSL ASCII . 1. , . value f : Nat Nat Nat f(a,b) as c post if (exists n : Nat :- is_divisor(a,n) /\ is_divisor(b,n)) then is_divisor(a,c) /\ is_divisor(b,c) /\ all c1:Nat :- is_divisor(a,c1) /\ is_divisor(b,c1) => (c1<=c) end, is_divisor : Nat > Nat is_divisor(a,b) is b ~= 0 /\ a > b /\ a - (a / b) * b = a, f : Nat > Nat f(a,b) is if a=b then a elsif a-b > 0 then f(a-b,b) else f(a,b-a) end : value f : Nat > Nat f(a,b) is if a=b then a elsif a-b > 0 then f(a-b,b) else f(a,b-a) end 2. , S2 S1: scheme S1 = class type A,B,C value f1 : A >< B -> Bool, f2 : A >< B -~-> C, f3 : C -~-> A >< B axiom all a: A, b: B :f3( f2(a, b))is (a,b) pre f1(a,b) = true end
49


scheme S2 = class type A=Int, B=Nat, C=Int value f1 : A >< B -> Bool f1(i,n) is i * i = n, f2 : A >< B -~-> C f2(i,n) is i, f3 : C -~-> A >< B f3(cc) as (a,b) post (cc = a) /\ b = (cc * cc) end : all a: A, b: B :f3( f2(a, b))is (a,b) pre f1(a,b) = true all_assumption_inf: [[ if f1(a,b) = true then f3( f2(a, b)) is (a,b) end ]] unfold_true: [[ if f1(a,b) then f3( f2(a, b)) is (a,b) end ]] unfold_f1: [[ if a*a = b then f3( f2(a, b)) is (a,b) end ]] unfold_f2: [[ if a*a = b then f3( a ) is (a,b) end ]] unfold_f3: [[ if a*a = b then (a, a*a))is (a,b) end ]] if_annihilation: [[ (a, b)is (a,b) ]] is_annihilation: true 3. , get. scheme EXAM = class type R, value empty put : R del : R

Key, Val : Unit -> R, >< Key >< Val -> R, >< Key >< Val -~-> R,

50


get: R >< Key -~-> Val-set, find: R >< Key -> Bool, axiom forall r : R, k1, k2 : Key, v1, v2 : Val :[find_empty] find (empty(), k1) is false, [find_put] find (put(r, k1, v1), k1) is true, [get _put] get (put(r, k1, v1), k1) is if find (r, k1) then get (r, k1) union {v1} else {v1} end, [del_put_1] del(put(r, k1, v1), k1, v1) is if find (r, k1) /\ v1 isin get (r, k1) then del(r, k1, v1) else r end, [put_put] put(put(r, k1, v1), k2, v2) is if (k1 = k2) /\ (v1 = v2) then put(r, k1, v1) else put(put(r, k2, v2), k1, v1) end end : type R = Key-m->Val-set, Key, Val value get: R >< Key -~-> Val-set get(r,k) as vs post vs = r(k) pre k isin dom r 4. (b!2) || (y:=a?) || if (x:=1); (a!x); (true |^| false) then a!(b?) else a!(1+b?) end : x:=1; (y:=1) ; (a!2) |^| x:=1; (y:=1) ; (a!3)

51


5. f, " " (AFDNF) post if (a > 5) /\ (b < 3) then ... elsif ((a > b) /\ (b=0)) \/ (b<3) then ... else ... end : 1: m1 m2 2: 3: m1~m2 m3~m4~m2 m1 ~m2 ~m3~m2 ~m1 m3 ~m4 ~m1~m3 m2 ~m1 m3 ~m4 m2 ~m1 m3 ~m4 ~m2 ~m1 ~m3 ~m2 1 2 2 2 3 3 3 3 3 3 3 m1 = a>5 true true true true true true false false false false false m2 = b<3 true false false false false false true false true true false true false true true false true false false false false false true true false false true true true false false 6 6 5 1 5 5 3 4 6 1 2 2 3 3 m1~m2 m3~m4~m2 m1 ~m2 ~m3~m2 ~m1 m3 ~m4 ~m1~m3 m2 ~m1 m3 ~m4 m2 ~m1 m3 ~m4 ~m2 ~m1 ~m3 ~m2 m3 = a>b m4 = b=0 m2 = b<3 a 6 b 2 m1 m2

. .
52


.
. 1. AFDNF . 2. . : AFDNF . : f, " " (AFDNF). 1. value f : Int >< Int-list >< Nat -~-> Nat >< Bool f (a,b,c) as (q,p) post if (a + len b > c) /\ (a isin elems b) then ... elsif (a>=c) /\ (a isin inds b) then ... else ... end pre (a < c) \/ (a isin inds b) m1 m2 m3 m4 a (a < c) (a isin (a + len b (a isin inds b) > c) elems b) 1 true true false 1 false true true true 2 false true false 2 false true true false 3 true false 3 true true false 2. post if (a > 4) /\ (b < 4) then ... elsif (a > b) /\ (b=4) then ... else ... end pre b<= 4 : post if m2 /\ m3 then ... elsif m4 /\ m5 then ... else ... end pre m1
53

b

m1m3m4 ~m1m2m3m4 ~m1m2~m3 ~m1m2m3~m4 m1~m3 m1m3~m4


B1 ­ m1m2m3 B2 ­ m1m2~m3m4m5 B3 ­ m1~m2~m4 \/ m1~m2m4~m5 3. post if (b > 5) /\ (a < 3) then ... elsif ((a > b) /\ (b=0)) \/ (b<5) then ... else ... end pre a+b<=7 : post if m2 /\ m3 then ... elsif (m4 /\ m5) \/ m6 then ... else ... end pre m1 B1 ­ m1m2m3 B2 ­ m1~m2m4m5 m1~m2m4~m5m6 m1~m2~m4m6 B3 ­ m1~m2~m4~m6 4. post if (a isin dom b) /\ (b (a) = a) then ... elsif ((rng b inter dom b) = {}) \/ b(a+1) < 0 then ... else ... end pre (a isin dom b) /\ ((a+1) isin dom b) : post if m1 /\ m3 then ... elsif m4 \/ m5 then ... else ... end pre m1 /\ m2 B1 ­ m1m2m3 B2 ­ m1m2~m3~m4m5 m1m2~m3m4 B3 ­ m1m2~m3~m4~m5

54


5. post if (a > 5) /\ (b < 3) then ... elsif (a > b) \/ (b<3) then ... else ... end pre (a>2*b) : post if m2 /\ m3 then ... elsif m4 \/ m3 then ... else ... end pre m1 B1 ­ m1m2m3 B2 ­ m1m2~m3m4 \/ m1~m2m4 \/ m1~m2~m4m3 : . 1. (b!2) || (x:=a?) || if (a!3; true) |^| ((a!b?+5); false) then a!(b?) else a!(1+b?) end || (a!0) : x:=3 x:=0 x:=7 x:=0 || || ; || a!2 || a!0 |^| a!3 ; a!2 |^| a!(1+b?) || a!0 a!7; a!(1+b?)

2. (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) : x:=1; y:=0 3. (b!2) || (x:=a? |^| y:=b?) || (y:=a?) || if (true |^| false) then a!(b?) else a!(1+b?) end : x:=2 || (y:=a?) |^| x:=3 || (y:=a?) |^| y:=2 || x:=a? |^| y:=3 || x:=a? |^| y:=2 || y:=b? |^| y:=3 || y:=b? |^| y:=2 || y:=a? || a!b? |^| y:=2 || y:=a? || a!(1+b?)

55


4. (b!2) || (a!4; x:=a?) || (y:=a?) || if (true |^| false) then a!(b?) else a!(1+b?) end : x:=2 || (y:=4) |^| x:=3 || (y:=4) |^| y:=2 || a!4; x:=a? |^| y:=3 || a!4; x:=a? 5. a!(5+b?) || ((x:=(if true |^| false then x:=b?;1 else b!3;x:=2;6 end)+x) ++ (b!4 || y:=b?)) : a!(5+b?) || x:=5; y:=b? |^| y:=3; x:=8; a!9 |^| a!8 || x:=8 || y:=4 6. case (1 |^| b?) of 1 -> x:=a?+1, 2 -> x:=b?, 3 -> y:=a?+3, 4 -> y:=b?+a?, 5 -> x:=y:=a?;y end || a!1 || b!(a?+2) || a!3 7. case (1 |^| b?) of 1 -> x:=a?+1, 2 -> x:=b? |^| a?, 3 -> y:=a?+3, 4 -> y:=b?+a?, 5 -> x:=y:=a?;y end || a!0 || b!(a?+a?) || a!2 || a!3 8. (b!4 || y:=b?) || (a!(5+b?) ++ (x:=( x:=b!2; a? |^| b!3;x:=2;6)+x) ) : y:=4 || x:=14 |^| y:=4 || x:=8 || a!8


1. The RAISE specification language. Prentice Hall, 1992. 2. RAISE Tools Reference Manual. LACOS/CRI/DOC/13/1/V2, 1994. 3. B. Beizer. Software Testing Techniques, 2/e . New-York: Van Nostrand Reinhold, 1990. 4. B. Marick. The Craft of software Testing, PTR Prentice Hall, 1995.
56



........................................................................................................................ 3 1. RSL .................................................................... 5 1.1. RSL. RSL ........................................................ 5 1.1.1. RSL .................................................................... 5 1.1.2. RSL .................................................................................... 6 ............................................................................................................. 7 1.2. ........................................................................................... 9 1.2.1. ( products ) ....................................................... 9 1.2.2. ..................................................................................... 9 1.2.3. ................................................................................... 10 1.2.3.1. ................. 10 1.2.3.2. ....................................................... 11 1.2.3.3. ................................................... 11 1.2.3.4. ............................................... 12 1.2.3.5. ............................................................ 12 ........................................................................................................... 13 1.3. ....................................................................................................... 15 1.3.1. .................................................................................. 15 1.3.2. ............................................................ 16 ........................................................................................................... 17 1.4. ............................................................................................................. 18 1.4.1. ......................................................................................... 18 1.4.2. ............................................................... 18 1.4.3. ........................................................................... 20 ........................................................................................................... 20 1.5. (maps) ....................................................................................... 21 1.5.1. .............................................................................. 21 1.5.2. ...................................................... 22 1.5.3. ................................................................ 23 ........................................................................................................... 25 2. ..................................................................................... 26 2.1. .......................................................................................... 26 2.2. ........................................................................................... 26 2.3. ........................................................................ 30 3. eden ......................................................... 31 3.1. ......................................................................... 31 3.2. ........................................................................... 33 3.3. ................................................................................. 34 3.4. ............................................................. 38 3.5. ............................................................ 41 1 .............................................................. 44 .............................................................................................................. 49 ............................................................................................................. 56
57