[SAL-HELP] Countable sets

[Anthony Simons]

Dear SAL helpers,

I'm still trying to work out how to implement countable sets.   The 
attached context file
"bitset.sal" implements sets as bit-vectors.  However, in order to allow 
the counting
of bits (via the recursive size_aux), the index-type of the bitset must 
be numerical.

Ideally, I'd like to use any scalar type T as the index type.  To do 
this, I imagine using
some kind of cache array:

    rank : ARRAY T OF NATURAL

to store the mappings from elements to indices.  However, I cannot for 
the life of me
work out how to initialise 'rank' to a unique number for each T element.

If you can help me to solve this, that would be much appreciated.

Best wishes,

-- Tony Simons (with John Derrick and Siobha'n North)

-------------- next part --------------
bitset{T : TYPE; N : NATURAL} : CONTEXT =
BEGIN

%% A bitset is a bit-vector of length N, indexed from 1..N.
%% It is used to model a set, whose elements all have a unique
%% rank in the range 1..N.  The advantage of this encoding is
%% that you can recursively count the elements in a set, in a
%% way that the SAL toolset can guarantee to terminate.

	Range : TYPE = [1..N];
	
%%	Rank : TYPE = ARRAY T OF Range;
%%	rank : Rank = ...
%%
%% How can you initialise rank to a unique Range value for each
%% distinct scalar value T ?


	Set : TYPE = ARRAY Range OF BOOLEAN;
	
	empty_set : Set = [[i : Range] FALSE];
	
	full_set : Set = [[i : Range] TRUE];
	
	size_aux(set : Set, n : NATURAL, s : Range) : Range =
		IF n = 0
		THEN s
		ELSIF set[n] 
		THEN size_aux(set, n-1, s+1)
		ELSE size_aux(set, n-1, s)
		ENDIF;
		
	size?(set : Set) : NATURAL = 
		size_aux(set, N, 0);
	
	contains? (set : Set, i : Range) : BOOLEAN = 
		set[i];
		
	empty? (set : Set) : BOOLEAN = 
		(FORALL (i : Range) : NOT set[i]);
	
	insert (set : Set, i : Range) : Set = 
		set WITH [i] := TRUE;
	
	remove (set : Set, i : Range) : Set =
		set WITH [i] := FALSE;
		
	union (aset : Set, bset : Set) : Set =
		[[i : Range] aset[i] OR bset[i]];

	intersection (aset : Set, bset : Set) : Set =
		[[i : Range] aset[i] AND bset[i]];
		
	difference (aset : Set, bset : Set) : Set =
		[[i : Range] aset[i] AND NOT bset[i]];

END