VDM++ での演算 VDM_Map.domBy）を紹介します。 m = VDM_Map({"A":1,"B":2}) s = VDM_Set(["A","C"]) print ">>> %s X = m.domBy(s) print X; assert X == VDM_Map({"B":2})写像 m の定義域から集合 s の要素を削除した写像を得るには、メソッド domBy を利…

VDM++ での演算 :-> に準拠した事例（VDM_Map.rngBy）を紹介します。 m = VDM_Map({"A":1,"B":2}) s = VDM_Set([1,3]) print ">>> %s :-> %s"%(m,s) X = m.rngBy(s) print X; assert X == VDM_Map({"B":2})写像 m の値域から集合 s の要素を削除した写像を得…

VDM++ での演算 :> に準拠した事例（VDM_Map.rngTo）を紹介します。 m = VDM_Map({"A":1,"B":2}) s = VDM_Set([1,3]) print ">>> %s :> %s"%(s,m) X = m.rngTo(s) print X; assert X == VDM_Map({"A":1})写像 m の値域を集合 s の要素に限定した写像を得るに…

VDM++ での演算 m = VDM_Map({"A":1,"B":2}) s = VDM_Set(["A","C"]) print ">>> %s domTo(s) print X; assert X == VDM_Map({"A":1})写像 m の定義域を集合 s の要素に限定した写像を得るには、メソッド domTo を利用します。このコードを実行すると、>>> {…

VDM++ での演算 :> および :-> に準拠するように、メソッド VDM_Map.rngTo/VDM_Map.rngBy を実現します。class VDM_Map: def rngTo(m,s): """ m :> s ; map A to B * set of B -> map A to B ; ; Range restricted to ; creates the map consisting of the e…

VDM++ での演算 class VDM_Map: def domTo(m,s): """ s map A to B ; ; Domain restricted to ; creates the map consisting of the elements in m ; whose key is in s. s need not be a subset of dom ; m. """ return VDM_Map(m._domain(dom(m).inter(s))…

VDM++ の map 型には、定義域および値域を限定/削除した、新たな写像を定義できます。VDM++ では、次のように表現します。 {'A', 'C'} 1, 'B' |-> 2} = {'A' |-> 1}写像 {'A' |-> 1, 'B' |-> 2} の定義域を、キー集合 {'A', 'C'} の要素に限定すると {'A' |-…

Shall_we_Agile = Java.use(better, Python) # Swing by VDM++《記事一覧》 改訂♪2008/09/12《承前》