Algorithmen und Datenstrukturen 2011 WS

ADT

Type Permutation

Import int, String, Bool, Menge, Sequenz

Literals idn (für jede Permutationsgruppe Sn)

Operations

Permutation:	Sequenz ---> Permutation	Erzeugt eine Permutation
sigma:	int x Permutation -/-> int	Gibt das gewählte Abbild
cycle:	Permutation x int -/-> Sequenz<int>	Gibt den gewählten Zyklus
allCycles:	Permutation ---> Menge<Sequenz<int>>	Gibt alle Zyklen aus der Permutation
fixedPoints:	Permutation ---> Menge<Sequenz<int>>	Gibt alle Fixpunkt aus der Permutation
inverse:	Permutation ---> Permutation	Gibt die invertierte Permutation
toString:	Permutation ---> String	Darstellung als String
toCycleNotationString:	Permutation ---> String	Darstellung der Zyklen als String
equals:	Permutation x Permutation ---> Bool	Prüft strukturelle Gleichheit
compose:	Permutation x Permutation -/-> Permutation	Gibt die Komposition der beiden Permutation wieder
permutationClass:	Permutation ---> int	Gibt die Anzahl der Elemente der Permutation

Axioms

σ: Permutation σ ∈ S1

cycle(σ ,1) = fixedPoints(σ)

inverse(σ) = σ

inverse(σ) = compose(σ,σ)

compose(σ,inverse(σ)) = σ

equals(σ,σ) = true

σ1,σ2, σ3 :Permutation σ1,σ2, σ3 ∈ Sn

compose(σ1,compose(σ2,σ3)) = compose(compose(σ1,σ2),σ3)

equals(σ1,id) = true & equals(σ1,σ2) = false => fixedPoints(σ1) != fixedPoints(σ2)

inverse(inverse(σ3)) = σ3

equals(σ1,σ2) = equals(σ2,σ1)

equals(σ1,σ2) = equals(cycle(σ1), cycle(σ2))

equals(σ1,σ2) => equals(inverse(σ1), inverse(σ2))