-- Autor: Matthias Ansorg -- MatrNr: 678306 -- Datum: 2003-12-03 -- Lizenz: public domain -- zugehoeriges UML-Diagramm: HUebg1-Namensrecht.UML.MatthiasAnsorg.png context Person inv: -- Jede Person hat einen Geburtsnamen: self.nameRolleObj->exists(n|n.oclIsTypeOf(GeburtsName)) and -- Ein Ehepartner kann einen Ehenamen haben: self.personRolleObj->exists(n|n.oclIsTypeOf(EhePartner)) implies self.nameRolleObj->exists(n|n.oclIsTypeOf(EheName)) and -- Ein Ehepartner kann höchstens einen Ehenamen haben: self.personRolleObj->select(oclIsTypeOf(EheName))->size(1) context EheName inv: -- Der Ehename ist der eigene Geburtsname oder der Geburtsname des Ehepartners: self.person.personRolleObj->select(oclIsTypeOf(EhePartner)).familie.personRolleObj-> select(oclIsTypeOf(EhePartner))->exists(person.nameRolleObj->select(oclIsTypeOf(GeburtsName)).name = self.name.oclAsType(OclAny)) and -- Ein Kind hat keinen Ehenamen, es sei denn es ist auch Ehepartner in einer eigenen Familie self.person.personRolleObj->exists(oclIsTypeOf(Kind)) implies self.person.personRolleObj->exists(oclIsTypeOf(Ehepartner)) context Ehepartner inv: let meinEheName : Name = self.person.nameRolleObj->select(oclIsTypeOf(EheName)).name let deinEheName : Name = self.familie.personRolleObj-> select(p | p.oclIsTypeOf(EhePartner) and p <> self.oclAsType(OclAny)) .person.nameRolleObj->select(oclIsTypeOf(EheName)).name -- Wenn ein Ehepartner einen Ehenamen hat, so hat auch der andere Ehepartner diesen Ehenamen. self.person.nameRolleObj->exists(oclIsTypeOf(EheName)) implies meinEheName = deinEheName context BegleitName inv: let meinEhePartner : Person = self.person.personRolleObj->select(oclIsTypeOf(Ehepartner)) .familie.personRolleObj->select(p | p.oclIsTypeOf(EhePartner) and p.person <> self.person. oclAsType(OclAny)).person let meinEheName : Name = self.person.nameRolleObj->select(oclIsTypeOf(EheName)).name -- Ein Begleitname ist nur dann möglich (aber nicht zwingend), wenn ein Ehepartner -- einen Ehenamen hat self.person.nameRolleObj->exists(oclIsTypeOf(Ehename)) and -- Ein Begleitname ist identisch mit dem eigenen Geburtsnamen. self.name = self.person.nameRolleObj->select(oclIsTypeOf(GeburtsName)).name and -- Der Begleitname darf nicht identisch mit dem Ehenamen sein. self.name <> meinEheName and -- Wenn ein Ehepartner einen Begleitnamen hat, so darf der andere Ehepartner keinen Begleitnamen haben. not self.person.meinEhePartner.nameRolleObj->exists(oclIsTypeOf(BegleitName)) and -- Ein Kind hat keinen Begleitnamen, es sei denn es ist auch Ehepartner in einer eigenen Familie self.person.personRolleObj->exists(oclIsTypeOf(Kind)) implies self.person.personRolleObj->exists(oclIsTypeOf(Ehepartner)) context Familie inv: -- Alle Kinder derselben Familie haben denselben Geburtsnamen. -- formuliert als: Menge der unterschiedlichen Namen der Kinder hat ein Element self.personRolleObj->select(oclIsTypeOf(Kind)) ->iterate(k:Kind; acc:Name = Set{} | acc->including(k.person.nameRolleObj->select(oclIsTypeOf(GeburtsName))->Name)) ->size() = 1 -- Ein geschiedener Ehepartner kann einen Ehenamen haben. -- implizit möglich, indem eine Person die beiden Rollen "Ehepartner" und "Geschieden" hat context GeburtsName inv: let eltern : Set(Ehepartner) = self.person.personRolleObj->select(oclIsTypeOf(Kind)). familie.personRolleObj->select(oclIsTypeOf(Ehepartner)) -- Der GeburtsName eines Kindes ist stets der GeburtsName eines Elternteils. Impliziert: wenn die -- Eltern einen Ehenamen führen, so ist der GeburtsName des Kindes der Ehename; denn der Ehename -- ist ja gleich dem Geburtsnamen eines Elternteils! eltern->exists(self.name = person.nameRolleObj->select(oclIsTypeOf(GeburtsName))) and -- Führen die Eltern keinen Ehenamen, so darf der Geburtsname des Kindes keinen Bindestrich und kein -- Leerzeichen enthalten. contains() ist eine Operation des selbst definierten Typs String! (not eltern->exists(person.nameRolleObj->select(oclIsTypeOf(EheName)))) implies (not (self.name.nameString.contains('-') or self.name.nameString.contains(' ')))