\documentclass[12pt,a4paper,serif]{article}
%\documentclass[10pt,a4paper,DIV15]{scrartcl}

%\usepackage{ngerman,a4}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{amsmath}
%\usepackage{stmaryrd}
\usepackage{enumerate}
%\usepackage{alltt}
\usepackage[latin1]{inputenc}
%\usepackage{graphicx}
\usepackage{cancel}
\usepackage{fuzz}

\thispagestyle{empty}

\title{Softwaretechnik (WS 2005/2006) - Übungsblatt 6}
\author{Jan Hendrik Dithmar - Matrikelnummer 2031259 \\
		Übungsgruppe Mi, 8-10 Uhr \\
		Dirk Heine - Matrikelnummer 2030941 \\
		Übungsgruppe Di, 14-16 Uhr \\\\
		Rückgabe: Übungsgruppe Mi, 8-10 Uhr
	}
\date{}

\begin{document}

\newcommand{\AND}{\ensuremath{\wedge}}
\newcommand{\OR}{\ensuremath{\vee}}
\newcommand{\SetR}{\ensuremath{\mathbb{R}}}
\newcommand{\SetN}{\ensuremath{\mathbb{N}}}
\newcommand{\SetC}{\ensuremath{\mathbb{C}}}
\newcommand{\SetZ}{\ensuremath{\mathbb{Z}}}
\newcommand{\SetQ}{\ensuremath{\mathbb{Q}}}
\newcommand{\SetB}{\ensuremath{\mathbb{B}}}
\newcommand{\R}{\ensuremath{\mathbb{R}}}
\newcommand{\N}{\ensuremath{\mathbb{N}}}
\newcommand{\C}{\ensuremath{\mathbb{C}}}
\newcommand{\Z}{\ensuremath{\mathbb{Z}}}
\newcommand{\Q}{\ensuremath{\mathbb{Q}}}
\newcommand{\B}{\ensuremath{\mathbb{B}}}
\newcommand{\QED}{\ensuremath{\hspace*{\fill}\square}}
\newcommand{\FLASH}{\ensuremath{\hspace*{\fill}\lightning}}
\newcommand{\OnotO}{\ensuremath{\mathcal{O}}}
\newcommand{\bild}[4]{
	\begin{figure}[htpb]
		\centering
			\includegraphics[width=#1cm]{#2}\\[0.2cm]
			\caption{#3}
			\label{#4}
	\end{figure}
	}

\maketitle

\newpage
\section*{Aufgabe 1}
\subsubsection*{(a)}
\begin{zed}
	[FORUM, PERSON, PASSWORT].
\end{zed}

\subsubsection*{(b)}
\begin{schema}{Permissions}
	permissions: (FORUM \fun PASSWORT) \times (FORUM \rel PERSON)
\end{schema}
%\begin{schema}{Permissions}
%	permissions: FORUM \rel PERSON \times PASSWORT
%\end{schema}

\subsubsection*{(c)}
\begin{schema}{Active}
	Permissions \\
	active: FORUM \pfun PERSON
\where
	\forall ((a,b),(a,c)) \in permissions @ (a,c) \in active
%	\forall ((a?,b?),(c?,d?)) \in permissions @ (c?,d?) \in active
\end{schema}

\subsubsection*{(d)}
\begin{schema}{Login}
	\Delta Active \\
	f?: FORUM \\
	p?: PERSON
\where
	active' = active \cup (f?,p?)
\end{schema}

\begin{schema}{NotActive}
	\Xi Active \\
	f?: FORUM \\
	p?: PERSON
\where
	(f?,p?) \notin active
\end{schema}

\begin{schema}{NoPermission}
	\Xi Permissions \\
	f?: FORUM \\
	pe?: PERSON \\
	pa?: PASSWORT
\where
	((f?,pa?),(f?,pe?)) \notin permissions
\end{schema}

\begin{zed}
	T\_enter-forum \defs NoPermission \OR Login \OR NotActive
\end{zed}

\subsubsection*{(e)}
\begin{schema}{Kick}
	\Delta Active \\
	f?: FORUM \\
	p?: PERSON
\where
	active' = active \setminus (f?,p?)
\end{schema}

\begin{schema}{DelPermission}
	\Delta Permissions \\
	f?: FORUM \\
	pe?: PERSON
\where
	\forall pa: PASSWORT @ permissions' = permissions \setminus ((f?,pa),(f?,pe?))
\end{schema}

\begin{zed}
	T\_kick-out \defs NoPermission \OR (DelPermission \AND (Kick \OR NotActive))
\end{zed}

\newpage
\section*{Aufgabe 2}
\subsubsection*{(a)}
\begin{schema}{Rooks}
	squares: COLUMN \fun ROW
\where
	\forall c_1, c_2: COLUMN; c_1 \neq c_2 @ \dom squares(c_1) \neq \dom squares(c_2)
\also
	\forall r_1, r_2: ROW; r_1 \neq r_2 @ \ran squares(r_1) \neq \ran squares(r_2)
\end{schema}

\subsubsection*{(b)}
\begin{schema}{UpDown}
	r?,r'?: ROW \\
	c?,c'?: COLUMN
\where
	c'? = c?
\also
	r'? \neq r?
\end{schema}

\begin{schema}{LeftRight}
	r?,r'?: ROW \\
	c?,c'?: COLUMN
\where
	r'? = r?
\also
	c'? \neq c?
\end{schema}

\begin{schema}{NoMove}
	r?,r'?: ROW \\
	c?,c'?: COLUMN
\where
	r'? = r?
\also
	c'? = c?
\end{schema}

\begin{zed}
	T\_Move \defs NoMove \OR UpDown \OR LeftRight
\end{zed}

\newpage
\section*{Aufgabe 3}
\subsubsection*{(a)}
\begin{zed}
	[CHAR]
\end{zed}

\begin{zed}
	TEXT == \seq CHAR \\
%	SPACE == \seq_1 blank \\
%	WORD == \seq_1 (CHAR \setminus blank) \\
	LINE == \seq_1 (CHAR \setminus \{nl\})
\end{zed}

\begin{axdef}
	lines: TEXT \fun \seq LINE
\where
	\forall l: LINE; t,b: TEXT @ \\
	\t1 lines(\left< \right>) = \left< \right> \AND \\
	\t1 lines(nl) = \left< \right> \AND \\
	\t1 lines(l) = \left< l \right> \AND \\
	\t1 lines(nl \cat b) = lines(b) \AND \\
	\t1 lines(t \cat nl) = lines(t) \AND \\
	\t1 lines(t \cat nl \cat b) = lines(t) \cat lines(b)
\end{axdef}

\subsubsection*{(b)}
\begin{schema}{Justify}
	\Delta Fill \\
\where
	\forall l: \ran lines(t'), \# l < width @ space \cat l
\end{schema}

\begin{schema}{Justified}
	\Xi Fill
\where
	\forall l: \ran lines(t') @ \#l = width
\end{schema}

\begin{zed}
	 T\_Justify \defs Justify \OR Justified
\end{zed}

\end{document}