Fahrkartenkauf_am_Schalter -------------------------- self.Zielbahnhof->size()>0 self.Reisender->size>0 Fahrkartenkauf_am_Schalter::Reservierung_eines_Sitzplatzes(ZNR.Zug_Nr):Sitzplatz -------------------------------------------------------------------------------- pre : self.Sitzplatz-> exists(Sp:Sitplatz|Sp.freie_Sitzplatzanzahl>0;Sp.Zug_nr=ZNR ) post : Sp.freie_Sitzplatzanzahl=Sp.freie.Sitzplatzanzahl@pre-1