Source : ISO 10303-54
SCHEMA set_theory_schema;
REFERENCE FROM
classification_schema -- ISO 10303-54
(class);
REFERENCE FROM
support_resource_schema -- ISO 10303-41
(identifier,
label,
text);
ENTITY complement;
id : identifier;
name : label;
description :
OPTIONAL
text;
set_1 : class;
set_2 : class;
universe : class;
WHERE
complement_different: NOT identical_sets(set_1, set_2);
END_ENTITY;
ENTITY intersection;
id : identifier;
name : label;
description :
OPTIONAL
text;
operand : SET[2:?] OF class;
resultant : class;
END_ENTITY;
ENTITY power_set;
id : identifier;
name : label;
description :
OPTIONAL
text;
base : class;
derived : class;
WHERE
derived_different: NOT identical_sets(base, derived);
END_ENTITY;
ENTITY proper_subset
SUBTYPE OF (subset);
WHERE
subset_different: NOT identical_sets(superset, subset);
END_ENTITY;
ENTITY same_membership;
id : identifier;
name : label;
description :
OPTIONAL
text;
set_1 : class;
set_2 : class;
END_ENTITY;
ENTITY subset;
id : identifier;
name : label;
description :
OPTIONAL
text;
subset : class;
superset : class;
END_ENTITY;
ENTITY union;
id : identifier;
name : label;
description :
OPTIONAL
text;
operand : SET[2:?] OF class;
resultant : class;
END_ENTITY;
ENTITY union_of_all_members;
id : identifier;
name : label;
description :
OPTIONAL
text;
operand : class;
resultant : class;
WHERE
resultant_different: NOT identical_sets(operand, resultant);
END_ENTITY;
FUNCTION identical_sets
(set_a : class; set_b : class) : BOOLEAN;
LOCAL
set_of_sets : SET OF class := [];
END_LOCAL;
IF (set_a = set_b) THEN
RETURN (TRUE);
END_IF;
set_of_sets := set_of_sets + set_b;
RETURN (identical_to_one_of_set_of_sets(set_a, set_of_sets));
END_FUNCTION;
FUNCTION identical_to_one_of_set_of_sets
(set_a : class; set_of_sets : SET OF class) : BOOLEAN;
LOCAL
i : INTEGER;
initial_size : INTEGER;
augmented_size : INTEGER;
set_of_forward_equivalences : SET OF same_membership := [];
set_of_backward_equivalences : SET OF same_membership := [];
augmented_set_of_sets : SET OF class := [];
END_LOCAL;
-- test membership of the specified set of sets
IF (set_a IN set_of_sets) THEN
RETURN (TRUE);
END_IF;
-- extend the specified set to include all sets that have the same membership
-- as an existing member
initial_size := SIZEOF(set_of_sets);
IF (initial_size = 0) THEN
RETURN (FALSE);
END_IF;
REPEAT i := 1 TO initial_size;
set_of_forward_equivalences := set_of_forward_equivalences +
USEDIN(set_of_sets[i], 'SET_THEORY_SCHEMA.SAME_MEMBERSHIP.SET_1');
set_of_backward_equivalences := set_of_forward_equivalences +
USEDIN(set_of_sets[i], 'SET_THEORY_SCHEMA.SAME_MEMBERSHIP.SET_2');
END_REPEAT;
augmented_set_of_sets := set_of_sets;
IF (SIZEOF(set_of_forward_equivalences) > 0) THEN
REPEAT i := 1 to HIINDEX(set_of_forward_equivalences);
augmented_set_of_sets := augmented_set_of_sets +
set_of_forward_equivalences[i].set_2;
END_REPEAT;
END_IF;
IF (SIZEOF(set_of_backward_equivalences) > 0) THEN
REPEAT i := 1 to HIINDEX(set_of_backward_equivalences);
augmented_set_of_sets := augmented_set_of_sets +
set_of_backward_equivalences[i].set_1;
END_REPEAT;
END_IF;
-- if the specified set of sets has been augmented, then test membership
augmented_size := SIZEOF(augmented_set_of_sets);
IF augmented_size = initial_size THEN
RETURN (FALSE);
END_IF;
RETURN (identical_to_one_of_set_of_sets(set_a, augmented_set_of_sets));
END_FUNCTION;
END_SCHEMA; -- set_theory_schema