{\small\sf class} $Student$ {\small\sf is subclass of}  $Person$
\par
\kInstanceVarDef
\parlinebr
\begin{insvar}
\assdef{Studienkonto}{\seqof*{\Char }}
\end{insvar}
\begin{insvar}\kw{public}
\assdef{immat}{\setof{Immatrikulation}}
\end{insvar}
\begin{instinvfn}
 \Card immat \Ge 1\end{instinvfn}
\begin{instinvfn}
\unique{i \In immat}{ \Not i.istGasthoerer}\end{instinvfn}
\begin{instinvfn}
\set{\kSelf } = \setcomp{i.stud}{i \In immat}\end{instinvfn}
\begin{insvar}\kw{public}
\assdef{kursnote}{\Natone  \Bmap Pruefungsergebnisvermerk}[{\Emptymap }]
\end{insvar}
\begin{instinvfn}
\all{p1,p2 \In  \Rng kursnote}{p1 \Neq p2 \Implies  \\
p1.Pruefungsnummer \Neq p2.Pruefungsnummer}\end{instinvfn}
\begin{instinvfn}
\all{p \In  \Rng kursnote}{p.stud = \kSelf }\end{instinvfn}
\begin{instinvfn}
\all{p \In  \Rng kursnote}{p = \fnapply{kursnote}{p.Pruefungsnummer}}\end{instinvfn}
\begin{instinvfn}
\all{p \In  \Rng kursnote}{p.MatrikelNummer \In  \\
\setcomp{i.MatrikelNummer}{i \In immat}}\end{instinvfn}
\par
\kOperations
\kw{\kw{public}}\begin{op}[e]{istAlumnus}%
\signature{() \Oto \Bool }
\parms{}
\annlab[o]{Student`istAlumnus}
\return{ \Not \exists{i \In immat}{i.ExmatDatum = \Nil }}
\begin{precond}
\True 
\end{precond};
\end{op}
\kw{\kw{public}}\begin{op}[e]{getOpernKarte}%
\signature{\Nat  \Oto \Bool }
\parms{Einzahlung}
\annlab[o]{Student`getOpernKarte}
\return{\True }
\begin{precond}
Einzahlung \Ge 40
\end{precond}
\end{op}
{\small\sf end} {\it Student}

