note
	description: "[
		Object that checks whether an implementation of {STS_BINARY_RELATION} bears the properties
		determined by set theory
	]"
	author: "Rosivaldo Fernandes Alves"
	date: "$Date$"
	revision: "$Revision$"

deferred class
	STP_BINARY_RELATION_PROPERTIES [A, B, EQ_A -> STS_EQUALITY [A], EQ_B -> STS_EQUALITY [B]]

--inherit

--	STP_ORDERED_PAIR_PROPERTIES [
--		STS_ORDERED_PAIR [STS_SET [A, EQ_A], STS_SET [B, EQ_B], STS_SET_EQUALITY [A, EQ_A], STS_SET_EQUALITY [B, EQ_B]],
--		STS_SET [STS_ORDERED_PAIR [A, B, EQ_A, EQ_B], STS_PAIR_EQUALITY [A, B, EQ_A, EQ_B]],
--		STS_PAIR_EQUALITY [STS_SET [A, EQ_A], STS_SET [B, EQ_B], STS_SET_EQUALITY [A, EQ_A], STS_SET_EQUALITY [B, EQ_B]],
--		STS_SET_EQUALITY [STS_ORDERED_PAIR [A, B, EQ_A, EQ_B], STS_PAIR_EQUALITY [A, B, EQ_A, EQ_B]]
--		]
--		rename
--			inverse_ok as pair_inverse_ok,
--			composed_with_homogeneous_ok as pair_composed_with_homogeneous_ok
--		end

--feature -- Properties (Access)

--	domain_ok (r: STS_BINARY_RELATION [A, B, EQ_A, EQ_B]): BOOLEAN
--			-- Do the properties verified within set theory hold for {STS_BINARY_RELATION}.domain?
--		do
--			u_a := u_a & r.ab -- todo: rename/redefine u_a etc?
--			u_b := u_b & r.g
--			check
--				inside_departure: 𝐝𝐨𝐦 r ⊆ r.a
--			then
--				Result := True
--			end
--		ensure
--			u_a: u_a ⊇ old (u_a & r.ab)
--			u_b: u_b ⊇ old (u_b & r.g)
--		end

--	range_ok (r: STS_BINARY_RELATION [A, B, EQ_A, EQ_B]): BOOLEAN
--			-- Do the properties verified within set theory hold for {STS_BINARY_RELATION}.range?
--		do
--			u_a := u_a & r.ab
--			u_b := u_b & r.g
--			check
--				inside_arrival: 𝐫𝐚𝐧 r ⊆ r.b
--			then
--				Result := True
--			end
--		ensure
--			u_a: u_a ⊇ old (u_a & r.ab)
--			u_b: u_b ⊇ old (u_b & r.g)
--		end

--feature -- Properties (Operation)

--	inverse_ok (r: STS_BINARY_RELATION [A, B, EQ_A, EQ_B]): BOOLEAN
--			-- Do the properties verified within set theory hold for {STS_BINARY_RELATION}.inverse?
--		do
--			u_a := u_a & r.ab
--			u_b := u_b & r.g
--			check
--				involutive: ⁻¹(⁻¹r) ≍ r
--				domain: 𝐝𝐨𝐦 ⁻¹r ≍ 𝐫𝐚𝐧 r
--				range: 𝐫𝐚𝐧 ⁻¹r ≍ 𝐝𝐨𝐦 r
--			then
--				Result := True
--			end
--		ensure
--			u_a: u_a ⊇ old (u_a & r.ab)
--			u_b: u_b ⊇ old (u_b & r.g)
--		end

--	image_ok (r: STS_BINARY_RELATION [A, B, EQ_A, EQ_B]; s: STS_SET [A, EQ_A]): BOOLEAN
--			-- Do the properties verified within set theory hold for {STS_BINARY_RELATION}.image?
--		do
--			u_a := u_a & r.ab
--			u_b := u_b & r.g
--			check
--				inside_arrival: r [s] ⊆ r.b
--			then
--				Result := True
--			end
--		ensure
--			u_a: u_a ⊇ old (u_a & r.ab)
--			u_b: u_b ⊇ old (u_b & r.g)
--		end

--	inverse_image_ok (r: STS_BINARY_RELATION [A, B, EQ_A, EQ_B]; s: STS_SET [B, EQ_B]): BOOLEAN
--			-- Do the properties verified within set theory hold for {STS_BINARY_RELATION}.inverse_image?
--		do
--			u_a := u_a & r.ab
--			u_b := u_b & r.g
--			check
--				inside_departure: r.inverse_image (s) ⊆ r.a
--			then
--				Result := True
--			end
--		ensure
--			u_a: u_a ⊇ old (u_a & r.ab)
--			u_b: u_b ⊇ old (u_b & r.g)
--		end

--	composed_with_homogeneous_ok (r: STS_BINARY_RELATION [A, B, EQ_A, EQ_B]): BOOLEAN
--			-- Do the properties verified within set theory hold for
--			-- {STS_BINARY_RELATION}.composed_with_homogeneous?
--		do
--			u_a := u_a & r.ab
--			u_b := u_b & r.g
--			check
--				identity: r ₁∘₁ 𝐼 r.a ≍ r
--			then
--				Result := True
--			end
--		ensure
--			u_a: u_a ⊇ old (u_a & r.ab)
--			u_b: u_b ⊇ old (u_b & r.g)
--		end

note
	copyright: "Copyright (c) 2012-2020, Rosivaldo Fernandes Alves"
	license: "[
		Eiffel Forum License v2
		(see http://www.eiffel.com/licensing/forum.txt)
		]"
	source: "https://launchpad.net/set-theory"
end
