General Information
Tutorials
Reference Manuals
Libraries
Translation Tasks
Tools
Administration
|
|
Abstract data types to be used in specifications
This module implements operations on sets over elements which are
nonnegative numbers. The range of each set value is dynamically
adapted as required by the operations.
Storage for set values is allocated when needed.
The module implementation uses efficient dynamic storage allocation
of the obstack.
The module does not implement automatic garbage collection.
Storage used by one instance of this module can be deallocated completely,
or for each single set value.
Some set operations are provided in two versions:
The functional version allocates a new result value and leaves
its operands unchanged.
The imperative version modifies one of its operands to represent
the result of the operation.
Note: In the imperative case, too, the result of the function call
rather than the operand
has to be used for subsequent accesses to the modified set value,
e. g. s = AddElemToBitSet (x, s); where s is a BitSet
variable.
The module does not have generic parameters.
It is used by writing
$/Adt/BitSet.fw
in a .specs file.
All entities exported by this module can be used in specifications
of type .lido, .init, .finl, and .con.
They can also be used in .pdl specifications or in C modules
if the interface file BitSet.h is imported there.
The module exports the following type names and macros:
BitSet
- A pointer type representing sets.
NullBitSet
- The 0 pointer representing an empty set.
Note: The empty set can be represented in different ways.
Hence, the function
EmptyBitSet must be used to check
for a set being empty.
The following set processing functions are supplied by the module:
void FreeBitSet (BitSet s)
- Deallocates the set
s.
void FreeMemBitSet (void)
- Deallocates all memory allocated for sets.
BitSet NewBitSet (void)
- Allocates an empty set.
int EqualBitSet (BitSet s1, BitSet s2)
- Yields 1 if
s1 and s2 contain the same elements; otherwise 0.
int EmptyBitSet (BitSet s)
- Yields 1 if
s is empty; otherwise 0.
int EmptyIntersectBitSet (BitSet s1, BitSet s2)
- Yields 1 if the intersection of
s1 and s2 is empty;
otherwise 0.
int ElemInBitSet (int el, BitSet s)
- Yields 1 if
el is an element of s; otherwise 0.
int CardOfBitSet (BitSet s)
- Yields the number of elements in
s.
BitSet AddElemToBitSet (int el, BitSet s)
- Imperative: Adds element
el to set s.
BitSet ElemToBitSet (int el)
- Returns a set consisting only of element
el. This function
can be used as the third (function) parameter in an application of
the CONSTITUENTS construct.
BitSet AddRangeToBitSet (int el1, int el2, BitSet s)
- Imperative: All elements in the range from
el1 to el2
are added to the set s.
BitSet SubElemFromBitSet (int el, BitSet s)
- Imperative: Subtracts element
el from set s.
BitSet UnionToBitSet (BitSet s1, BitSet s2)
- Imperative:
s1 is set to the union of s1 and s2
BitSet IntersectToBitSet (BitSet s1, BitSet s2)
- Imperative:
s1 is set to the intersection of s1 and s2.
BitSet SubtractFromBitSet (BitSet s1, BitSet s2)
- Imperative:
s2 is subtracted from s1.
BitSet ComplToBitSet (int upb, BitSet s)
- Imperative:
s is complemented with respect to the
range 0 .. upb;
no assumption can be made on elements larger than upb in s
BitSet UniteBitSet (BitSet s1, BitSet s2)
- Functional: Yields the union of
s1 and s2
BitSet IntersectBitSet (BitSet s1, BitSet s2)
- Functional: Yields the intersection of
s1 and s2
BitSet SubtractBitSet (BitSet s1, BitSet s2)
- Functional: Yields
s1 minus s2.
BitSet ComplBitSet (int upb, BitSet s)
- Functional: Yields the complement of
s with respect to the
range 0 .. upb;
no assumption can be made on elements larger than upb in the result.
int NextElemInBitSet (int elem, BitSet s)
- Yields the smallest element of
s that is larger than elem,
if any; -1 otherwise.
void ApplyToBitSet (BitSet s, void func(int))
- Applies the function
func to each element of s
void PrintBitSet (BitSet s)
- Prints
s as a string of 0 and 1 to stdout.
void PrintElemsBitSet (BitSet s)
- Prints
s as a comma separated sequence of its
elements to stdout.
|
