VDM-SL VDM++ 23 6 28 VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web 2 1 3 1.1............................................... 3 1.1.1 bool......................................... 3 1.1.2 real rat int nat nat1............................... 3 1.1.3 char.......................................... 3 1.1.4.............................................. 4 1.1.5 token....................................... 4 1.2............................................... 4 1.2.1.............................................. 4 1.2.2 nil...................................... 4 1.2.3................................................ 4 1.2.4............................................ 4 1.2.5.............................................. 5 1.2.6................................................ 6 1.2.7.............................................. 6 1.2.8.............................................. 7 2 8 2.1 if................................................. 8 2.2 cases............................................... 8 2.3 let................................................. 8 2.4 def................................................. 9 2.5 let be............................................... 9 2.6................................................... 9 2.6.1 forall.............................................. 9 2.6.2 exists.............................................. 9 2.6.3 exists1............................................. 10 1 8.1 2 http://www.vdmtools.jp/, http://www.overturetool.org/ 1
2.7................................................. 10 2.8................................................ 10 2.9................................................... 10 2.9.1.............................................. 10 2.9.2............................................ 11 2.10................................................ 11 2.11 for................................................... 11 2.11.1 for............................... 11 2.11.2 for....................................... 11 2.11.3 for........................................ 11 2.12 while.................................................. 12 2.13................................................. 12 2.13.1 trap.............................................. 12 2.13.2 tixe............................................... 12 2.13.3 exit............................................... 12 2.13.4 always............................................. 12 2.14................................................ 13 3 13 3.1............................................. 13 3.2............................................ 13 3.3 VDM-SL.................................. 14 3.4 VDM++........................... 14 3.5............................................ 14 3.6............................................ 15 3.7 VDM++................................ 17 3.8 VDM++................................ 17 2
1 VDM++ = <> 1.1 1.1.1 bool true false 1 not b a and b a or b a => b a <=> b b a b a b a b not a or b a b 1: bool 1.1.2 real rat int nat nat1 real rat int nat 0 nat1 1 3-2.5 0 11... 2 - x x abs x x absolute value floor x x x + y -, *, / x div y integer division x mod y rem mod modulus rem remainder x ** y x y a < b >, <=, >= 2: 1.1.3 char char 1.2.6 a b... 1... 3
1.1.4 1.2.1 <red> <Japan> <error-mode>... 1.1.5 token mk_token(3) mk_token({-1, true}) mk_token("vdm")... mk token 1.2 1.2.1 char int <Japan> <France> <USA>... 1.2.2 nil [bool] [<Japan> <France> <USA>]... nil 1.2.3 nat * bool * char seq of char * bool... mk_(3, true, a ) mk_({mk_token("vdm"), true})... mk t n t.#n 1.2.4 compose RecordA of key : nat description : seq of char end : :- 4
RecordA :: key : nat description : seq of char mk_recorda(5, "VDM++") mk_recorda({1, "B Method"})... mk r i r.i r mu mu( r, key1 > val1, key2 > val2,... ) R is_r 1.2.5 {1, 2, 3} { a, c, x } { }... 3 { exp pat1a, pat1b,... in set s1, pat2a, pat2b,... in set s2,... & cond } in set S : T m n {m,..., n} e in set s e s 3 in set {1,2,3} true e not in set s e s 3 in set {1,2,3} false s1 union s2 s1 s2 {1,2,3} union {2,4} {1,2,3,4} s1 inter s2 s1 s2 {1,2,3} inter {2,4} {2} s1 \s2 s1 s2 {1,2,3} \{2,4} {1,3} s1 subset s2 s1 s2 {2,3} subset {1,2,3} true s1 psubset s2 s1 s2 {2,3} psubset {2,3} false card s s card {2,5,6} 3 dunion ss ss dunion {{1,2,3}, {2,4},{1,2,5}} {1,2,3, 4,5} dinter ss ss dunion {{1,2,3}, {2,4},{1,2,5}} {2} power s s power {1,2} {{},{1}, {2},{1,2}} 3: 5
1.2.6 [1, 2, 3] [ a, c, x ] [ ]... 4 [ exp pat1a, pat1b,... in set s1, pat2a, pat2b,... in set s2,... & cond ] s1 s2 l m n l(m,..., n) l(i) l i [ a, b, c ](2) b hd l l hd [1,2,3] 1 tl l l tl [1,2,3] [2,3] len l l [1,2,3] 3 elems l l [1,2,3,2,3] {1,2,3} inds l l [1,2,3,2,3] {1,2,3,4,5} l1 ˆl2 l1 l2 [1,2]ˆ[3,2] {1,2,3,2} conc ll ll conc [[1,2], [3,2],[4,1]] [1,2,3,2, 4,1] l ++ m m l [ a, b, c, d ] ++ {1 -> x,4 -> y } [ x, b, c, y ] 4: 1.2.7 {1 -> true, 2 -> false, 3 -> true} { A -> "41", B -> "42"} { -> }... 5 6 { e1 -> e2 pat1a, pat1b,... in set s1, pat2a,... in set s2,... & cond } 6
m(d) m d {1 -> a,2 -> b }(2) b dom m m dom {1 -> a,2 -> b } {1,2} rng m m rng {1 -> a,2 -> b } { a, b } inverse m m m inmap inverse {1 -> a, 2 -> b } { a ->1, b ->2} s <: m s <-: m m :> s m :-> s m s m s m s m s {1,2} <: {1 -> a,2 -> b, 3 -> c } {1,2} <-: {1 -> a,2 -> b, 3 -> c } {1 -> a,2 -> b, 3 -> c } :> { a, b } {1 -> a,2 -> b, 3 -> c } :-> { a, b } 5: {1 -> a, 2 -> b } {3 -> c } {1 -> a, 2 -> b } {3 -> c } m1 munion m2 m1 ++ m2 merge ms m1 comp m2 m ** n m1 m2 m1 m2 ms munion map A to B m2 map B to C m1 map A to C m n {1 -> a,2 -> b } munion {1 -> a,3 -> c } {1 -> a,2 -> b } ++ {1 -> x,3 -> c } merge {{1 -> a,2 -> b }, {1 -> a,3 -> c },} {2 -> b,4 -> d }} {1 -> a,2 -> b } comp { x ->1, y ->2} {1 ->2,2 ->3} {3 ->1} ** 2 {1 -> a, 2 -> b, 3 -> c } {1 -> x, 2 -> b, 3 -> c } {1 -> a, 2 -> b, 3 -> c, 4 -> d } { x -> a, y -> b } {1 ->3, 2 ->1, 3 ->2} 6: 1.2.8 int +> bool int * seq of char +> ()... -> +> f a1 a2 an f (a1, a2,..., an) f 2 f 1 f 1 comp f 2 f n f ** n 7
2 VDM++ 2.1 if if cond1 then e1 elseif cond2 then e2 else e3 if cond1 then s1 elseif cond2 then s2 else s3 cond1 e1 s1 cond2 e2 s2 e3 s3 elseif VDM++ Toolbox if else VDM-SL 2.2 cases cases e : p11, p12,..., p1n -> e1, p21, p12,..., p2n -> e2,..., pm1, pm2,..., pmn -> em, others -> eo end cases e : p11, p12,..., p1n -> s1, p21, p12,..., p2n -> s2,..., pm1, pm2,..., pmn -> sm, others -> so end e p11 p12 p1n e1 s1 others others 2.3 let let p1 : T1 = e1, p2 : T2 = e2,..., pn : Tn = en in e let p1 : T1 = e1, p2 : T2 = e2,..., pn : Tn = en in s 8
T1 p1 e1 p2 e2 e slet 2.4 def def p1 : T1 = e1; p2 : T2 = e2;...; pn : Tn = en in e def p1 : T1 = e1; p2 : T2 = e2;...; pn : Tn = en in s T1 p1 e1 p2 e2 e s in set S 2.5 let be let p in set S let p in set S be st cond in e be st cond in s p S cond e s in set S : T 2.6 2.6.1 forall forall pat1a, pat1b,... in set s1, pat2a, pat2b,... in set s2,... patna, patnb,... in set sn, & cond forall pat1a pat1b s1 s2 cond true bool 2.6.2 exists exists pat1a, pat1b,... in set s1, pat2a, pat2b,... in set s2,... & cond exists pat1a pat1b s1 s2 cond true bool 9
2.6.3 exists1 exists1 pat1a, pat1b,... in set s1, pat2a, pat2b,... in set s2,... & cond exists1 pat1a pat1b s1 s2 cond true bool 2.7 lambda pat1 : T1, pat2 : T2,..., patn : Tn & e pat1 patn e T1 Tn n 1 n 1 2.8 iota 1 is is_bool(x) is_token(x) is(x, bool) new VDM++ new VDM++ isofclass isofbaseclass samebaseclass sameclass undefined 2.9 2.9.1 var := e var e 10
2.9.2 atomic( var1 := e1 var2 := e2... varn := en ) 2.10 ( ) dcl var1:t 1 := e1, var2:t 2 := e2,..., varn:t n := en; s1; s2;... sn dcl s1 s2 sn dcl 2.11 for 2.11.1 for for id = e1 to e2 by e3 do s id e1 e3 e2 s 2.11.2 for for all pat in set S do s S pat s 2.11.3 for for all pat in l do s l pat s in reverse l pat pat in set S pat : T 11
2.12 while while cond do s cond s 2.13 2.13.1 trap trap pat with s1 in s2 s2 s2 trap pat s1 trap 2.13.2 tixe tixe pat1 -> s1, pat2 -> s2,..., patn -> sn in s s s tixe pat1 pat2 patn si 2.13.3 exit exit e e 2.13.4 always always s1 in s2 s2 s1 12
2.14 return return exp skip error start VDM++ startlist VDM++ 3 3.1 types Tname1 = T1; Tname1 = T1 inv pat == cond; Tname1 T1 pat cond VDM++ static Tname1 = :: 1.2.4 3.2 values pat1 : T 1 = exp1; exp1 pat1 T1 VDM++ static pat1 13
3.3 VDM-SL state state statename of id1 : T1 id2 : T2... idn : Tn inv inv pat == inv cond init init pat == init cond end statename id1 T1 inv p at inv c ond init p at init c ond 3.4 VDM++ instance variables var1 : T 1 = exp1; T1 var1 := exp1 T1 VDM++ static var1 cond inv cond; 3.5 functions f un1 [@tv1, @tv2,..., @tvm] (pat1 : T1, pat2 : T2,..., patn : Tn) varret : T ret pre precond post postcond; 14
1 f un1 2 @tv1 3 pat1 T1 4 varret Tret 5 precond 6 postcond f un1 [@tv1, @tv2,..., @tvm] (pat1 : T1, pat2 : T2,..., patn : Tn) varret : T ret == exp pre precond post postcond; 5 exp f un1 [@tv1, @tv2,..., @tvm] : T1 * T2 *... * Tn -> Tret f un1 (pat1, pat2,..., patn) == exp pre precond post postcond; 1 f un1 2 @tv1 3 T1 Tret 1.2.8 -> +> 4 pat1 5 exp 6 precond 7 postcond RESULT VDM++ static var1 is not yet specified is subclass responsibility 3.6 functions op1 (pat1 : T1, pat2 : T2,..., patn : Tn) varret : T ret ext mode1 var1a, var1b,..., var1p : Te1 15
mode2 var2a, var3b,..., var2q : Te2... modem varma, varmb,..., varmr : Tem pre precond post postcond; 1 op1 2 pat1 T1 3 varret Tret 4 8 VDM-SL VDM++ mode1 rd wr Te1 2 precond postcond op1 (pat1 : T1, pat2 : T2,..., patn : Tn) varret : T ret == s ext mode1 var1a, var1b,..., var1p : Te1 mode2 var2a, var3b,..., var2q : Te2... modem varma, varmb,..., varmr : Tem pre precond post postcond; 4 s op1 : T1 * T2 *... * Tn ==> Tret op1 (pat1, pat2,..., patn) == exp pre precond post postcond; 1 op1 2 T1 Tret 3 pat1 4 exp 5 precond 6 postcond RESULT VDM++ static var1 is not yet specified is subclass responsibility 16
3.7 VDM++ sync op1 cond1 per op1 => cond1 #req(op) #act(op) #fin(op) #active(op) #waiting(op) op op op op = #act(op) - #fin(op) op = #req(op) - #act(op) mutex(op1, op2,..., opn) mutex(all) 3.8 VDM++ thread s 17