class Person

values private

MaennlicheVornamen = {"Hans", "Georg"};

private

WeiblicheVornamen = {"Heidrun", "Cornelia"}

functions private

istMaennlicherVorname : char^{∗} → 𝔹 istMaennlicherVorname (v) \underline{△}

v ∈ MaennlicheVornamen;

private

istWeiblicherVorname : char^{∗} → 𝔹 istWeiblicherVorname (v) \underline{△}

v ∈ WeiblicheVornamen;

private

keineZeitweiseBigamie : Hochzeit-set → 𝔹 keineZeitweiseBigamie (s) \underline{△}

∀ h1, h2 ∈ s · h1 ≠ h2 ⇒ h1.Hochzeitsdatum.groesserGleich (h2.Scheidungsdatum) ∨

h2.Hochzeitsdatum.groesserGleich (h1.Scheidungsdatum);

private

initNachname : Person-set → char^{∗} initNachname (e) \underline{△}

if card e = 1

then let m ∈ e in

m.Nachname else if card e = 2

then let Mutter ∈ e be st Mutter.Geschlecht = weiblich in let aktuelleEheDerMutter ∈ Mutter.hochzeit be st

aktuelleEheDerMutter.Scheidungsdatum = Datum‘invalidDatum in let aktuellerEhemannDerMutter = aktuelleEheDerMutter.ehemann in if aktuellerEhemannDerMutter ∈ e then aktuelleEheDerMutter.Familienname else Mutter.Nachname

else "NameVomGericht"

instance variables

public Nachname : char^{∗} := initNachname (elter);

Geburtsname : char^{∗};

Vorname : char^{∗};

inv Geschlecht = maennlich ⇒ istMaennlicherVorname (Vorname) inv Geschlecht = weiblich ⇒ istWeiblicherVorname (Vorname) public Geschlecht : Util‘Genus; Geburtsort : char^{∗}; public Geburtsdatum : Datum; Staatsbuergerschaft : Util‘Nation := de; Bekenntnis : char^{∗}; Status : Util‘Personenstand := ledig; inv Status = tot ⇔ Sterbedatum = Datum‘invalidDatum Sterbedatum : Datum; Beruf : char^{∗}; BiometrischeMerkmale : Util‘BioDaten; Ausweisnummer : ℕ := 0; public Wohnsitz : Adresse^{∗} := []; inv len Wohnsitz > 0 ⇒

self ∈ ⋃ {adr.person | adr ∈ elems Wohnsitz} public hochzeit : Hochzeit-set; inv card hochzeit > 1 ⇒

if Geschlecht = maennlich then {self} = {h.ehemann | h ∈ hochzeit} else {self} = {h.ehefrau | h ∈ hochzeit}

inv card hochzeit > 0 ⇒ keineZeitweiseBigamie (hochzeit) inv card hochzeit > 0 ⇒

card {h | h ∈ hochzeit · h.Scheidungsdatum = Datum‘invalidDatum} ≤ 1

elter : Person-set; inv card elter ≤ 2 inv card elter > 0 ⇒ self ∈ ⋃ {e.kind | e ∈ elter} inv card elter = 0 ⇒ Vormund ≠ nil inv card elter > 0 ⇒ ∀ e ∈ elter ·

Geburtsdatum.minus (e.Geburtsdatum) ≥ 8

inv card elter = 1 ⇒ let e ∈ elter in

Nachname = e.Nachname

inv card elter = 2 ⇒

∀ e ∈ elter · card e.hochzeit > 0 ⇒ ∀ h ∈ e.hochzeit · Geburtsdatum.inbetween (h.Hochzeitsdatum, h.Scheidungsdatum) ⇒ Nachname = h.Familienname

kind : Person-set; inv card kind > 0 ⇒ self ∈ ⋃ {k.elter | k ∈ kind} Vormund : [Person]; inv Vormund ≠ nil ⇒ self ∈ Vormund.Muendel Muendel : Person-set; inv card Muendel > 0 ⇒

(∀ m ∈ Muendel · m.Vormund ≠ nil ) ∧ ({self} = {m.Vormund | m ∈ Muendel})

operations public

getOpernKarte : ℕ →^{o} 𝔹 getOpernKarte (Einzahlung) \underline{△}

return true

pre Einzahlung ≥ 100 ;

public

Alter : Datum →^{o} ℕ Alter (amDatum) \underline{△}

return amDatum.minus (Geburtsdatum) pre amDatum.groesserGleich (Geburtsdatum) ;

public

sammleVorfahren : ℕ →^{o} Person^{∗} sammleVorfahren (level) \underline{△}

if (level = 0) ∨ (card elter = 0)

then return []

elseif (card elter = 1)

then let e1 ∈ elter in

return [e1] ↷ e1.sammleVorfahren (level − 1) else let e1 ∈ elter in

let e2 ∈ elter be st e2 ≠ e1 in return [e1, e2] ↷

e1.sammleVorfahren (level − 1) ↷ e2.sammleVorfahren (level − 1)

pre level ≥ 0 ;

private

istNeffe : Person →^{o} 𝔹 istNeffe (n) \underline{△}

let Geschwister =

⋃ {e.kind | e ∈ elter} \ {self} in let NeffenUndNichten = ⋃ {g.kind | g ∈ Geschwister} in return (n ∈ NeffenUndNichten) ∧

(n.Geschlecht = maennlich);

private

Cousins : () →^{o} Person-set Cousins () \underline{△}

let Grosseltern = ⋃ {e.elter | e ∈ elter} in

let OnkelUndTanten =

⋃ {g.kind | g ∈ Grosseltern} \ elter in let CousinsUndCousinen = ⋃ {o.kind | o ∈ OnkelUndTanten} in return {c | c ∈ CousinsUndCousinen ·c.Geschlecht = maennlich};

private

istStiefvater : Person →^{o} 𝔹 istStiefvater (s) \underline{△}

let Mutter = ι e ∈ elter · e.Geschlecht = weiblich in let GattenDerMutter = {h.ehemann | h ∈ Mutter.hochzeit} in let HochzeitenVonSMitMutter =

{h | h ∈ s.hochzeit · h.ehefrau = Mutter} in return (s.Geschlecht = maennlich) ∧

(s ∈ (GattenDerMutter \ elter)) ∧ (∃ h ∈ HochzeitenVonSMitMutter ·

h.Scheidungsdatum.groesserGleich (Datum‘today ()))

end Person