|
/*
A module that specifies and defines general purpose functions over sets.
All functions are explicit and executable. Where a non-executable condition adds value, it
is included as a comment.
*/
module Set
imports from Numeric all,
from Seq all
exports functions sum: set of real +> real
prod: set of real +> real
min: set of real +> real
max: set of real +> real
toSeq[@a]: set of @a +> seq of @a
xform[@a,@b]: (@a +> @b) * set of @a +> set of @b
fold[@a]: (@a * @a +> @a) * @a * set of @a +> @a
fold1[@a]: (@a * @a +> @a) * set of @a +> @a
pairwiseDisjoint[@a]: set of set of @a +> bool
isPartition[@a]: set of set of @a * set of @a +> bool
permutations[@a]: set of @a +> set of seq1 of @a
xProduct[@a,@b]: set of @a * set of @b +> set of (@a * @b)
definitions
functions
-- The sum of a set of numerics.
sum: set of real +> real
sum(s) == fold[real](Numeric`add,0,s);
-- The product of a set of numerics.
prod: set of real +> real
prod(s) == fold[real](Numeric`mult,1,s);
-- The minimum of a set of numerics.
min: set of real +> real
min(s) == fold1[real](Numeric`min, s)
pre s <> {}
post RESULT in set s and forall e in set s & RESULT <= e;
-- The maximum of a set of numerics.
max: set of real +> real
max(s) == fold1[real](Numeric`max, s)
pre s <> {}
post RESULT in set s and forall e in set s & RESULT >= e;
-- The sequence whose elements are those of a specified set, with no duplicates.
-- No order is guaranteed in the resulting sequence.
toSeq[@a]: set of @a +> seq of @a
toSeq(s) ==
cases s:
{} -> [],
{x} -> [x],
t union u -> toSeq[@a](t) ^ toSeq[@a](u)
end
post len RESULT = card s and forall e in set s & Seq`inSeq[@a](e,RESULT);
-- Apply a function to all elements of a set. The result set may be smaller than the
-- argument set if the function argument is not injective.
xform[@a,@b]: (@a+>@b) * set of @a +> set of @b
xform(f,s) == { f(e) | e in set s }
post (forall e in set s & f(e) in set RESULT) and
(forall r in set RESULT & exists e in set s & f(e) = r);
-- Fold (iterate, accumulate, reduce) a binary function over a set.
-- The function is assumed to be commutative and associative, and have an identity element.
fold[@a]: (@a * @a +> @a) * @a * set of @a +> @a
fold(f, e, s) == cases s:
{} -> e,
{x} -> x,
t union u -> f(fold[@a](f,e,t), fold[@a](f,e,u))
end
--pre (exists x:@a & forall y:@a & f(x,y) = y and f(y,x) = y)
--and (forall x,y:@a & f(x, y) = f(y, x))
--and (forall x,y,z:@a & f(x,f(y,z)) = f(f(x,y),z))
measure size2;
-- Fold (iterate, accumulate, reduce) a binary function over a non-empty set.
-- The function is assumed to be commutative and associative.
fold1[@a]: (@a * @a +> @a) * set of @a +> @a
fold1(f, s) == cases s:
{e} -> e,
t union u -> f(fold1[@a](f,t), fold1[@a](f,u))
end
pre s <> {}
--and (forall x,y:@a & f(x,y) = f(y,x))
--and (forall x,y,z:@a & f(x,f(y,z)) = f(f(x,y),z))
measure size1;
-- Are the members of a set of sets pairwise disjoint.
pairwiseDisjoint[@a]: set of set of @a +> bool
pairwiseDisjoint(ss) == forall x,y in set ss & x<>y => x inter y = {};
-- Is a set of sets a partition of a set?
isPartition[@a]: set of set of @a * set of @a +> bool
isPartition(ss,s) == pairwiseDisjoint[@a](ss) and dunion ss = s;
-- All (sequence) permutations of a set.
permutations[@a]: set of @a +> set of seq1 of @a
permutations(s) ==
cases s:
{e} -> {[e]},
- -> dunion { { [e]^tail | tail in set permutations[@a](s\{e}) } | e in set s }
end
pre s <> {}
post -- for a set of size n, there are n! permutations
card RESULT = prod({1,...,card s}) and
forall sq in set RESULT & len sq = card s and elems sq = s
measure size;
-- The cross product of two sets.
xProduct[@a,@b]: set of @a * set of @b +> set of (@a * @b)
xProduct(s,t) == { mk_(x,y) | x in set s, y in set t }
post card RESULT = card s * card t;
-- Measure functions.
size[@a]: set of @a +> nat
size(s) == card s;
size1[@a]: (@a * @a +> @a) * set of @a +> nat
size1(-, s) == card s;
size2[@a]: (@a * @a +> @a) * @a * set of @a +> nat
size2(-, -, s) == card s;
end Set
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
