VDM-SL VDM VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web bool

Size: px

Start display at page:

Download "VDM-SL VDM VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web bool"

こごろうはにうだ
6 years ago
Views:

1 VDM-SL VDM VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web bool real rat int nat nat char token nil if cases let def let be forall exists exists

2 for for for for while trap tixe exit always VDM-SL VDM VDM VDM

3 1 VDM++ = <> 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 real rat int nat nat1 real rat int nat 0 nat 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: char char a b

4 <red> <Japan> <error-mode> token mk_token(3) mk_token({-1, true}) mk_token("vdm")... mk token char int <Japan> <France> <USA> nil [bool] [<Japan> <France> <USA>]... nil nat * bool * char seq of char * bool... mk_(3, true, a ) mk_({mk_token("vdm"), true})... mk t n t.#n compose RecordA of key : nat description : seq of char end : :- 4

5 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, 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

6 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 -> true, 2 -> false, 3 -> true} { A -> "41", B -> "42"} { -> } { e1 -> e2 pat1a, pat1b,... in set s1, pat2a,... in set s2,... & cond } 6

7 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: 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

8 2 VDM 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

9 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 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 exists exists pat1a, pat1b,... in set s1, pat2a, pat2b,... in set s2,... & cond exists pat1a pat1b s1 s2 cond true bool 9

10 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 iota 1 is is_bool(x) is_token(x) is(x, bool) new VDM++ new VDM++ isofclass isofbaseclass samebaseclass sameclass undefined var := e var e 10

11 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 for for id = e1 to e2 by e3 do s id e1 e3 e2 s for for all pat in set S do s S pat s for for all pat in l do s l pat s in reverse l pat pat in set S pat : T 11

12 2.12 while while cond do s cond s trap trap pat with s1 in s2 s2 s2 trap pat s1 trap tixe tixe pat1 -> s1, pat2 -> s2,..., patn -> sn in s s s tixe pat1 pat2 patn si exit exit e e always always s1 in s2 s2 s1 12

13 2.14 return return exp skip error start VDM++ startlist VDM types Tname1 = T1; Tname1 = T1 inv pat == cond; Tname1 T1 pat cond VDM++ static Tname1 = :: values pat1 : T 1 = exp1; exp1 pat1 T1 VDM++ static pat1 13

14 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 (pat1 : T1, pat2 : T2,..., patn : Tn) varret : T ret pre precond post postcond; 14

15 1 f un1 3 pat1 T1 4 varret Tret 5 precond 6 postcond f (pat1 : T1, pat2 : T2,..., patn : Tn) varret : T ret == exp pre precond post postcond; 5 exp f : T1 * T2 *... * Tn -> Tret f un1 (pat1, pat2,..., patn) == exp pre precond post postcond; 1 f un1 3 T1 Tret > +> 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

16 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

17 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

形式手法入門VDM++チュートリアル.key

形式手法入門VDM++チュートリアル.key 目的 n 世界的に成功したほとんどの形式手法仕様システムは以下の導入方法で成功している n 参考資料 : IPA 形式手法適用調査調査概要資料 l https://www.ipa.go.jp/files/000004548.pdf) l 1 週間程度のセミナー受講 l 経験ある専門家のコンサルティング n 今回のチュートリアルは上記導入方法の肝を紹介することで形式手法導入のための基礎知識を得ることを目的としている