{\small\sf class} $Adresse$
\par
\kInstanceVarDef
\parlinebr
\begin{insvar}\kw{private}
\assdef{Strasse}{\seqof*{\Char }}
\end{insvar}
\begin{instinvfn}
Strasse \Neq \Dquote  \Dquote \end{instinvfn}
\begin{insvar}\kw{private}
\assdef{Hausnummer}{\Natone }
\end{insvar}
\begin{insvar}\kw{private}
\assdef{PLZ}{\Natone }
\end{insvar}
\begin{instinvfn}
0 < PLZ \And PLZ < 100000\end{instinvfn}
\begin{insvar}\kw{private}
\assdef{Ort}{\seqof*{\Char }}
\end{insvar}
\begin{instinvfn}
Ort \Neq \Dquote  \Dquote \end{instinvfn}
\begin{insvar}\kw{private}
\assdef{Region}{\seqof*{\Char }}[{\Dquote NRW \Dquote }]
\end{insvar}
\begin{insvar}\kw{private}
\assdef{Land}{\seqof*{\Char }}[{\Dquote Deutschland \Dquote }]
\end{insvar}
\begin{instinvfn}
Land \Neq \Dquote  \Dquote \end{instinvfn}
\begin{insvar}\kw{private}
\assdef{Stockwerk}{\seqof*{\Char }}
\end{insvar}
\begin{insvar}\kw{public}
\assdef{person}{\setof{Person}}[{\set{}}]
\end{insvar}
\begin{instinvfn}
 \Card person > 0 \Implies  \\
\kSelf  \In  \Dunion \setcomp{ \Elems pers.Wohnsitz}{pers \In person}\end{instinvfn}
\par
\kOperations
\kw{\kw{public}}\begin{op}[e]{get-Strasse}%
\signature{() \Oto \seqof*{\Char }}
\parms{}
\annlab[o]{Adresse`get-Strasse}
\return{Strasse};
\end{op}
\kw{\kw{public}}\begin{op}[e]{set-Strasse}%
\signature{\seqof*{\Char } \Oto ()}
\parms{s}
\annlab[o]{Adresse`set-Strasse}
\ass{Strasse}{s}
\end{op}
{\small\sf end} {\it Adresse}

