\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{arcs}
\usepackage{fuzz}

\thispagestyle{empty}

\title{Softwaretechnik (WS 2005/2006) - Übungsblatt 7}
\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}
Zu zeigen:
\begin{zed}
	\exists Editor @ Init
\end{zed}
Beweis: \\
\begin{argue}
	\exists Editor @ Init & Definition \\
	\Leftrightarrow left,right: TEXT | \#(left \cat right) \leq maxsize @ \\
	\t1 left=right=\left<\right> & Schema expandieren \\
	\Leftrightarrow left,right: TEXT @ \#(left \cat right) \leq maxsize \\
	\t1 \AND left=right=\left<\right> & Eingeschränktes $\exists$ \\
	\Leftrightarrow \#(\left<\right> \cat \left<\right>) \leq maxsize & Ein-Punkt-Regel \\
	\Leftrightarrow 0 \leq maxsize & $\#(\left<\right>) = 0$
\end{argue}
Beim letzten Schritt wird außerdem vorausgesetzt, dass gilt:
\begin{zed}
	\left<\right> \cat \left<\right> = \left<\right>
\end{zed}

\section*{Aufgabe 2}
%Da $Format$ nichts verändert (z.B. mit $\Delta Editor$) gibt es keine (versteckten) Vorbedingungen.
$Format$ hat lediglich Nachbedingungen, aber keine Vorbedingungen.

\newpage
\section*{Aufgabe 3}
\subsubsection*{(a)}
\begin{schema}{Documents\_1}
	checked\_out\_1: \seq Entry
\where
	\forall i \in \{1, \ldots, \#checked\_out\_1\}: checked\_out\_1 (i) \in permission
\end{schema}

\subsubsection*{(b)}
\begin{schema}{Check\_Out\_1}
	\Delta Documents\_1 \\
	p?: PERSON \\
	d?: DOCUMENT
\where
	\neg(\exists e: Entry | e \in \ran checked\_out\_1 @ e.doc = d?)
\also
	(d?, p?) \in permission
\also
	checked\_out\_1' = checked\_out\_1 \cat \left< (\mu e: Entry | e.doc = d? \AND e.pers = p?) \right>
\end{schema}

\subsubsection*{(c)}
\begin{schema}{Refine}
	Documents \\
	Documents\_1
\where
	\dom checked\_out = \{e: Entry | e \in \ran checked\_out\_1 @ e.doc\}
\also
	\forall i \in \{1, \ldots, \#checked\_out\_1\} @ \\
	\t1 checked\_out\_1(i).pers = checked\_out(checked\_out\_1(i).doc)
\end{schema}

\subsubsection*{(d)}
Beweisverpflichtung:
\begin{zed}
	\forall Documents; Documents\_1 @ \\
	\t1 InitDocuments\_1 \AND Refine \Rightarrow InitDocuments
\end{zed}
Dabei ist $InitDocuments\_1$:
\begin{schema}{InitDocuments\_1}
	Documents\_1
\where
	checked\_out\_1 = \left< \right>
\end{schema}
Expandieren der linken Seite der Implikation:
\begin{zed}
	checked\_out\_1 = \left< \right> \AND \\
	\t1 \dom checked\_out = \{e: Entry | e \in \ran checked\_out\_1 @ e.doc\} \AND \\
	\t1 \forall i \in \{1, \ldots, \# checked\_out\_1\} @ \\
	\t2 checked\_out\_1(i).pers = checked\_out(checked\_out\_1(i).doc)
\end{zed}
Wegen $checked\_out\_1 = \left< \right>$ gilt:
\begin{zed}
	\{e: Entry | e \in \ran checked\_out\_1 @ e.doc\} = \emptyset \AND \\
	\dom checked\_out = checked\_out = \emptyset
\end{zed}
Damit ist das Prädikat von $InitDocuments$ gezeigt.

\subsubsection*{(e)}
Beweisverpflichtung:
\begin{zed}
	\forall Documents; Documents\_1; p?: PERSON; d?: DOCUMENT @ \\
	\t1 \pre CheckOut \AND Refine \Rightarrow \pre CheckOut\_1
\end{zed}
Expandieren:
\begin{zed}
	d? \notin \dom checked\_out \AND (d?,p?) \in permission \AND \\
	\dom checked\_out = \{e: Entry | e \in \ran checked\_out\_1 @ e.doc\} \AND \\
	\forall i \in \{1, \ldots, \# checked\_out\_1\} @ \\
	checked\_out\_1(i).pers = checked\_out(checked\_out\_1(i).doc) \Rightarrow \\
	\t1 \neg(\exists e: Entry | e \in \ran checked\_out\_1 @ e.doc = d?) \AND (d?, p?) \in permission
\end{zed}
Aus
\begin{zed}
	d? \notin \dom checked\_out \AND \\
	\dom checked\_out = \{e: Entry | e \in \ran checked\_out\_1 @ e.doc\}
\end{zed}
schließt man
\begin{zed}
	d? \notin \{e: Entry | e \in \ran checked\_out\_1 @ e.doc\}
\end{zed}
Das lässt sich umschreiben zu
\begin{zed}
	\forall e: Entry | e \in \ran checked\_out\_1 @ e.doc \neq d?
\end{zed}
oder gleich
\begin{zed}
	\neg (\exists e: Entry | e \in \ran checked\_out\_1 @ e.doc = d?)
\end{zed}
was zu zeigen war.

\subsubsection*{(f)}
Beweisverpflichtung:
\begin{zed}
	\forall \Delta Documents; \Delta Documents\_1; p?: PERSON; d?: DOCUMENT @ \\
	\t1 \pre CheckOut \AND CheckOut\_1 \AND \Delta Refine \Rightarrow CheckOut
\end{zed}
Expandiert:
\begin{zed}
	d? \notin \dom checked\_out \AND (d?,p?) \in permission \AND \\
	\neg(\exists e: Entry | e \in \ran checked\_out\_1 @ e.doc = d?) \AND \\
	(d?, p?) \in permission \AND \\
	checked\_out\_1' = checked\_out\_1 \cat \left< (\mu e: Entry | e.doc = d? \AND e.pers = p?) \right> \AND \\
	\dom checked\_out' = \{e: Entry | e \in \ran checked\_out\_1' @ e.doc\} \AND \\
	\forall i \in \{1, \ldots, \#checked\_out\_1'\} @ \\
	checked\_out\_1'(i).pers = checked\_out'(checked\_out\_1'(i).doc) \Rightarrow \\
	\t1 d? \notin \dom checked\_out \AND \\
	\t1 (d?,p?) \in permission \AND \\
	\t1 checked\_out' = checked\_out \cup \{(d?,p?)\}
\end{zed}
Dies ist nun zu beweisen. \\
Anmerkung: Es muss lediglich
\begin{zed}
	checked\_out' = checked\_out \cup \{(d?,p?)\}
\end{zed}
gezeigt werden. Dies zeigt man mit Hilfe von
\begin{zed}
	(1) \t1 d? \in \dom checked\_out' \\
	(2) \t1 checked\_out'(d?) = p?
\end{zed}
Ziel: Wir zeigen, dass
\begin{zed}
	(1) \t1 d? \in \dom checked\_out'
\end{zed}
gilt. Wir betrachten das Prädikat
\begin{zed}
	\dom checked\_out' = \{e: Entry | e \in \ran checked\_out\_1' @ e.doc\}
\end{zed}
Hier ist $checked\_out\_1'$
\begin{zed}
	checked\_out\_1' = checked\_out\_1 \cat \left< (\mu e_1: Entry | e_1.doc = d? \AND e_1.pers = p?) \right>
\end{zed}
Folgerung: Es gibt in $checked\_out\_1'$ einen Eintrag $e_1$ mit Dokument $d?$. \\
Folge:
\begin{zed}
	(d?,p?) \in \ran checked\_out' \mbox{ und somit } d? \in \dom checked\_out'
\end{zed}
Unser nächstes Ziel ist zu zeigen, dass
\begin{zed}
	(2) \t1 checked\_out'(d?) = p?
\end{zed}
gilt. Aus $(1)$ und dem Prädikat
\begin{zed}
	\forall i \in \{1, \ldots, \#checked\_out\_1'\} @ \\
	checked\_out\_1'(i).pers = checked\_out'(checked\_out\_1'(i).doc)
\end{zed}
schließen wir, dass
\begin{zed}
	(A) \t1 checked\_out'(d?) = \{i \in \{1, \ldots, \# checked\_out\_1'\} | \\
	\t2 checked\_out\_1'(i).doc = d? @ checked\_out\_1'(i).pers\}
\end{zed}
Aus dem Prädikat
\begin{zed}
	checked\_out\_1' = checked\_out\_1 \cat \left< (\mu e_1: Entry | e_1.doc = d? \AND e_1.pers = p?) \right>
\end{zed}
wissen wir, dass
\begin{zed}
	(B) \t1 \exists i \in \{1, \ldots, \# checked\_out\_1'\} @ e.doc = d? \AND e.pers = p?
\end{zed}
Aus $(A)$ und $(B)$ folgt nun $checked\_out\_1'(d?)=p?$.

\end{document}