/home_Python/note_/VDM/vdmSet.py
｜INDEX｜ Python.use(better)
》作業中です《
#....+....1....+....2....+....3....+....4....+....5....+....6....+....7....+
def vdm_quote(s):
if type(s) is str:
if s[0] == "_" and s[len(s)-1] == "_":
return "<%s>"%s[1:len(s)-1]
return s
# ==========
def forall(bind,expr):
"""
forall mbd1, mbd2, ..., mbdn & e
;
; Universal quantification
; where each mbdi is a multiple bind pi in set s (or if it
; is a type bind pi : type), and e is a boolean expression
; involving the pattern identifiers of the mbdi's. It has
; the value true if e is true when evaluated in the context
; of every choice of bindings from mbd1, mbd2, ..., mbdn and
; false otherwise.
"""
s = [expr(e) for e in bind.list]
return False not in s and len(s) <> 0
# ==========
def exists(bind,expr):
"""
exists mbd1, mbd2, ..., mbdn & e
;
; Existential quantification
; where the mbdi's and the e are as for a universal
; quantification. It has the value true if e is true when
; evaluated in the context of at least one choice of
; bindings from mbd1, mbd2, ..., mbdn, and false otherwise.
"""
s = [expr(e) for e in bind.list]
return True in s
# ==========
def exists1(bind,expr):
"""
exists1 bd & e
;
; Unique existential quantification
; where bd is either a set bind or a type bind and e is a
; boolean expression involving the pattern identifiers of
; bd. It has the value true if e is true when evaluated in
; the context of exactly one choice of bindings, and false
; otherwise.
"""
s = [expr(e) for e in bind.list]
return s.count(True) == 1
# ==========
def let_be_st(bind,expr):
"""
let b be st e1 in e2
;
; let-be-such-that expression
"""
return VDM_Set([e for e in bind.list if expr(e)])
# ==========
def let_be_such_that(bind,expr1,expr2):
"""
let b be st e1 in e2
;
; let-be-such-that expression
"""
for b in [e for e in bind.list if expr1(e)]:
expr2(b)
# ==========
def iota(bind,expr):
"""
iota bd & e
;
; iota expression
; where bd is either a set bind or a type bind, and e is
; a boolean expression involving the pattern identifiers
; of bd. The iota operator can only be used if a unique
; value exists which matches the bind and makes the body
; expression e yield true (i.e. exists1 bd & e must be
; true). The semantics of the iota expression is such that
; itreturns the unique value which satisfies the body
; expression (e).
"""
s = [e for e in bind.list if expr(e)]
if len(s) == 1: return s[0]
return None
# ==========
def card(s1):
"""
card s1
; set of A -> nat
;
; Cardinality
; yields the number of elements in s1.
"""
return len(s1.list)
# ==========
def dunion(ss):
"""
dunion ss
; set of set of A -> set of A
;
; Distributed union
; the resulting set is the union of all the elements (these
; are sets themselves) of ss, i.e. it contains all the
; elements of all the elements/sets of ss.
"""
return VDM_Set(_dunion(ss))
def _dunion(ss):
s = []
for sets in ss.list:
s = [e for e in s if not e in sets.list]
s += sets.list[:]
s.sort()
return s
# ==========
def dinter(ss):
"""
dinter ss
; set of set of A -> set of A
;
; Distributed intersection
; the resulting set is the intersection of all the elements
; (these are sets themselves) of, i.e. it contains the
; elements that are in all the elements/sets of ss. ss must
; be non-empty.
"""
return VDM_Set(_dinter(ss))
def _dinter(ss):
s = [e for e in ss.list[0]]
for sets in ss.list[1:]:
s = [e for e in s if e in sets.list]
s.sort()
return s
# ==========
def power(s1):
"""
power s1
; set of A -> set of set of A
;
; Finite power set
; yields the power set of s1, i.e. the set of all subsets of
; s1.
"""
return VDM_Set([VDM_Set(e) for e in _power(s1)])
def _power(s1):
s = s1.list
return _power2([[]],s,len(s))
def _power2(acc,xlist,n):
if n < 0: return []
acc2 = []
i = len(xlist)-n
for e1 in acc:
for e2 in xlist[i:]:
acc2.append(e1+[e2])
i += 1
return acc + _power2(acc2,xlist,n-1)
def vdm_quote(s):
if type(s) is str:
if len(s) == 1:
return "'%s'"%s
else:
return '"%s"'%s
return s
class VDM_Set:
def __init__(self,enclosure=None):
self.list = self._list(enclosure)
def _list(self,enclosure):
s = []
if enclosure is None: return s
s = [e for e in enclosure if not e in s]
s.sort()
return s
def __str__(self):
s = ""
for e in self.list:
s += "%s, "%(vdm_quote(e),)
return "{%s}"%s[:len(s)-2]
# ==========
def __contains__(s1,e):
"""
e in set s1
; A * set of A -> bool
;
; Membership
; tests if e is a member of the set s1
e not in set s1
; A * set of A -> bool
;
; Not membership
; tests if e is not a member of the set s1
"""
return e in s1.list
# ==========
def union(s1,s2):
"""
s1 union s2
; set of A * set of A -> set of A
;
; Union
; yields the union of the sets s1 and s2, i.e. the
; set containing all the elements of both s1 and
; s2.
"""
return VDM_Set(s1._Union(s2))
def _Union(s1,s2):
s = [e for e in s1.list if not e in s2.list]
s += s2.list[:]
s.sort()
return s
# ==========
def inter(s1,s2):
"""
s1 inter s2
; set of A * set of A -> set of A
;
; Intersection
; yields the intersection of sets s1 and s2, i.e.
; the set containing the elements that are in both
; s1 and s2.
"""
return VDM_Set(s1._Intersection(s2))
def _Intersection(s1,s2):
s = [e for e in s1.list if e in s2.list]
s.sort()
return s
# ==========
def __sub__(s1,s2):
"""
s1 \ s2
; set of A * set of A -> set of A
;
; Difference
; yields the set containing all the elements from
; s1 that are not in s2. s2 need not be a subset
; of s1.
"""
return VDM_Set(s1._Difference(s2))
def _Difference(s1,s2):
s = [e for e in s1.list if not e in s2.list]
s.sort()
return s
# ==========
def subset(s1,s2):
"""
s1 subset s2
; set of A * set of A -> bool
;
; Subset
; tests if s1 is a subset of s2, i.e. whether all
; elements from s1 are also in s2. Notice that any set
; is a subset of itself.
"""
for e in s1.list:
if not e in s2.list:
return False
return True
def psubset(s1,s2):
"""
s1 psubset s2
; set of A * set of A -> bool
;
; Proper subset
; tests if s1 is a proper subset of s2, i.e. it is a
; subset and s2\s1 is non-empty.
"""
if not s1.subset(s2): return False
s = s2 - s1
return card(s) != 0
# =========
def __getitem__(self,index):
return self.list[index]
def __len__(self):
return len(self.list)
############
def __eq__(s1,s2):
"""
s1 = s2
; set of A * set of A -> bool
;
; Equality
"""
return s1.list == s2.list
############
def __ne__(s1,s2):
"""
s1 <> s2
; set of A * set of A -> bool
;
; Inequality
"""
return not s1 == s2
## def card(self):
## return len(self.elements)
# --
def mdunion(self):
s = self._mdunion(self.list)
return VDM_Set(s)
def _mdunion(self,sets):
if len(sets) == 0: return []
head = sets[0]; rest = sets[1:]
if head.__class__ != VDM_Set:
return [head] + self._mdunion(rest)
else:
return self._mdunion(head) + self._mdunion(rest)
# ----------
def distribute(sets):
if len(sets) == 0: return []
head = sets[0]; rest = sets[1:]
if type(head) != list:
return [head] + distribute(rest)
else:
return distribute(head) + distribute(rest)
# ==========
def min_set(s):
"""
min(s:set of nat) x:nat
pre s <> {}
post x in set s and
forall y in set s \ {x} & y < x
"""
assert _pre_min(s)
x = min(s.list)
assert _post_min(x,s)
return x
def _pre_min(s):
assert s <> VDM_Set(),(
"::: pre min\n"+
"::: (>>%s<<) <> {}"
%(s)
)
return True
def _post_min(x,s):
assert (x in s and
forall(s - VDM_Set([x]),lambda y: x < y))
return True
# ----------
from _pyRun_ import *
signature("-",__file__,'1.0.1d*')
#....+....1....+....2....+....3....+....4....+....5....+....6....+....7....+Last updated♪2010/03/11
