<commit_before>\section{Zielbestimmung}%

% TODO Nachverfolgbarkeit der Anforderungen: Jeder funktionalen Anforderung muss eine Zielbestimmung zuzuordnen sein $\Rightarrow$ evtl. Zielbestimmungen ergänzen

\subsection{Interpreter}%

Der \see{Interpreter} ermöglicht die (schrittweise) Ausführung eines Programms und die Inspektion des aktuellen Programmzustands durch den Benutzer.%

\begin{description}%
    \item[Wunsch] Der Benutzer kann den Programmzustand w"ahrend der Ausf"uhrung "andern.%
    \item[Wunsch] Während eines Programmdurchlaufs können benutzerdefinierte Ausdr"ucke "uber dem Programmzustand ausgewertet werden.%
\end{description}%

\subsection{Run-time-checker}%

Der \see{Run-time-checker} erlaubt die Pr"ufung von \see{Zusicherungen} in Programmen f"ur einen konkreten Programmdurchlauf, d.~h.\ zur Laufzeit.%

\begin{description}%
    \item [Muss] Die im Programm eingebetteten (quantorenfreien) \see{Annotationen} werden ausgewertet. Im Fehlerfall erfolgt die Rückmeldung "uber die grafische Benutzeroberfl"ache.
    \item [Soll] Formeln mit Quantoren "uber einem eingeschr"ankten Bereich werden ausgewertet.%
    \item [Wunsch] Unbeschränkte Formeln mit Quantoren werden mit Hilfe eines \see{Beweisers} ausgewertet. Der aktuelle Programmzustand wird dazu dem Beweiser "ubergeben.
\end{description}%

\subsection{Grafische Benutzeroberfl"ache}%

Die grafische Benutzeroberfl"ache dient zur Steuerung der einzelnen Komponenten des Systems sowie der Anzeige von R"uckmeldungen der (externen) Module des Werkzeugs.%

\begin{description}%
    \item [Muss] Die Sprache der Benutzeroberfläche ist Englisch.%
    \item [Abgrenzung] Die Benutzeroberfläche enthält nur Optionen und Funktionen, die der besseren oder einfacheren Eingabe und Analyse des Programms durch den Benutzer zutr"aglich sind.%
    \item [Wunsch] Es werden zur besseren Lesbarkeit Unicode-Symbole f"ur logische Operatoren und Quantoren angezeigt.%
\end{description}%

\subsection{WHILE-Sprache}%

Die vom \textit{Worthwhile}-Interpreter erkannte Programmiersprache ist eine \see{WHILE-Sprache}.

\begin{description}%
    \item [Muss] Grundlegende Sprachkonstrukte: \texttt{if}-Anweisungen und \texttt{while}-Schleifen
    \item [Muss] Variablen mit Ganzzahlen~(\texttt{Integer}), Wahrheitswerten~(\texttt{Boolean}) sowie Arrays von \texttt{Integer} und \texttt{Boolean} als Datentypen%
    \item [Wunsch] Definition und Aufruf von eigenen Funktionen%
    \item [Abgrenzung] Weder Strings, Gleitkommazahlen, Zeiger noch eigene Datentypen%
    \item [Abgrenzung] Kein Heap%
    \item [Abgrenzung] Keine Nebenl"aufigkeit%
\end{description}%

\subsection{Annotationssprache}%

In der \see{Annotationssprache} werden die vom Beweiser gepr"uften WHILE-Programme spezifiziert. Zu einer Spezifikation geh"oren sowohl Zusicherungen als auch Invarianten.%

\begin{description}%
    \item [Muss] Spezifikationen sind im Quelltext des Programms eingebettet, aber durch spezielle Syntax klar vom Programm getrennt.%
    \item [Muss] Syntax und Semantik von Ausdr"ucken werden, soweit m"oglich, aus der Programmiersprache "ubernommen.%
    \item [Muss] Zusicherungen erlauben Aussagen der \see{Prädikatenlogik} "uber den Zustand einer Programmausf"uhrung.%
    \item [Muss] Grundlegende Annotationen: \texttt{\_assert} f"ur Zusicherungen und \texttt{\_assume} f"ur Voraussetzungen%
    \item [Soll] Spezielle Syntax~("`syntactic sugar"'), um die Verst"andlichkeit von Annotationen zu verbessern und ihre Formulierung intuitiver zu gestalten:%
        \begin{itemize}%
            \item Vor- und Nachbedingungen an Funktionen%
            \item (In-)Varianten an Schleifen%
            \item Globale Annahmen in Programmspezifikationen%
        \end{itemize}%
    \item [Wunsch] M"oglichkeit, mehrere Vor- und Nachbedingungen f"ur eine Funktion anzugeben%
\end{description}%

\subsection{Beweiserschnittstelle}%

\begin{description}%
    \item [Muss] Übersetzung aller Sprachkonstrukte außer Schleifen in eine vom Beweiser beweisbare prädikatenlogische Formel
    \item [Muss] Aufrufen des Beweisers
    \item [Abgrenzung] Keine automatische Findung von Schleifeninvarianten
\end{description}%

\subsection{Dokumentation und Beispielsammlung}%

\begin{description}%
    \item [Muss] Dokumentation f"ur die verwendete Programmier- und Annotationssprache%
    \item [Muss] Mitgelieferte Sammlung von kommentierten und spezifizierten Beispielprogrammen zur Verdeutlichung der Funktionalit"at von \textit{Worthwhile}%
\end{description}%<commit_msg>[pf] Change Beweiserschnittstelle to a more generic point<commit_after>\section{Zielbestimmung}%

% TODO Nachverfolgbarkeit der Anforderungen: Jeder funktionalen Anforderung muss eine Zielbestimmung zuzuordnen sein $\Rightarrow$ evtl. Zielbestimmungen ergänzen

\subsection{Interpreter}%

Der \see{Interpreter} ermöglicht die (schrittweise) Ausführung eines Programms und die Inspektion des aktuellen Programmzustands durch den Benutzer.%

\begin{description}%
    \item[Wunsch] Der Benutzer kann den Programmzustand w"ahrend der Ausf"uhrung "andern.%
    \item[Wunsch] Während eines Programmdurchlaufs können benutzerdefinierte Ausdr"ucke "uber dem Programmzustand ausgewertet werden.%
\end{description}%

\subsection{Run-time-checker}%

Der \see{Run-time-checker} erlaubt die Pr"ufung von \see{Zusicherungen} in Programmen f"ur einen konkreten Programmdurchlauf, d.~h.\ zur Laufzeit.%

\begin{description}%
    \item [Muss] Die im Programm eingebetteten (quantorenfreien) \see{Annotationen} werden ausgewertet. Im Fehlerfall erfolgt die Rückmeldung "uber die grafische Benutzeroberfl"ache.
    \item [Soll] Formeln mit Quantoren "uber einem eingeschr"ankten Bereich werden ausgewertet.%
    \item [Wunsch] Unbeschränkte Formeln mit Quantoren werden mit Hilfe eines \see{Beweisers} ausgewertet. Der aktuelle Programmzustand wird dazu dem Beweiser "ubergeben.
\end{description}%

\subsection{Grafische Benutzeroberfl"ache}%

Die grafische Benutzeroberfl"ache dient zur Steuerung der einzelnen Komponenten des Systems sowie der Anzeige von R"uckmeldungen der (externen) Module des Werkzeugs.%

\begin{description}%
    \item [Muss] Die Sprache der Benutzeroberfläche ist Englisch.%
    \item [Abgrenzung] Die Benutzeroberfläche enthält nur Optionen und Funktionen, die der besseren oder einfacheren Eingabe und Analyse des Programms durch den Benutzer zutr"aglich sind.%
    \item [Wunsch] Es werden zur besseren Lesbarkeit Unicode-Symbole f"ur logische Operatoren und Quantoren angezeigt.%
\end{description}%

\subsection{WHILE-Sprache}%

Die vom \textit{Worthwhile}-Interpreter erkannte Programmiersprache ist eine \see{WHILE-Sprache}.

\begin{description}%
    \item [Muss] Grundlegende Sprachkonstrukte: \texttt{if}-Anweisungen und \texttt{while}-Schleifen
    \item [Muss] Variablen mit Ganzzahlen~(\texttt{Integer}), Wahrheitswerten~(\texttt{Boolean}) sowie Arrays von \texttt{Integer} und \texttt{Boolean} als Datentypen%
    \item [Wunsch] Definition und Aufruf von eigenen Funktionen%
    \item [Abgrenzung] Weder Strings, Gleitkommazahlen, Zeiger noch eigene Datentypen%
    \item [Abgrenzung] Kein Heap%
    \item [Abgrenzung] Keine Nebenl"aufigkeit%
\end{description}%

\subsection{Annotationssprache}%

In der \see{Annotationssprache} werden die vom Beweiser gepr"uften WHILE-Programme spezifiziert. Zu einer Spezifikation geh"oren sowohl Zusicherungen als auch Invarianten.%

\begin{description}%
    \item [Muss] Spezifikationen sind im Quelltext des Programms eingebettet, aber durch spezielle Syntax klar vom Programm getrennt.%
    \item [Muss] Syntax und Semantik von Ausdr"ucken werden, soweit m"oglich, aus der Programmiersprache "ubernommen.%
    \item [Muss] Zusicherungen erlauben Aussagen der \see{Prädikatenlogik} "uber den Zustand einer Programmausf"uhrung.%
    \item [Muss] Grundlegende Annotationen: \texttt{\_assert} f"ur Zusicherungen und \texttt{\_assume} f"ur Voraussetzungen%
    \item [Soll] Spezielle Syntax~("`syntactic sugar"'), um die Verst"andlichkeit von Annotationen zu verbessern und ihre Formulierung intuitiver zu gestalten:%
        \begin{itemize}%
            \item Vor- und Nachbedingungen an Funktionen%
            \item (In-)Varianten an Schleifen%
            \item Globale Annahmen in Programmspezifikationen%
        \end{itemize}%
    \item [Wunsch] M"oglichkeit, mehrere Vor- und Nachbedingungen f"ur eine Funktion anzugeben%
\end{description}%

\subsection{Beweiserschnittstelle}%

\begin{description}%
    \item [Muss] Übersetzung des Programms in eine vom Beweiser beweisbare prädikatenlogische Formel
    \item [Muss] Aufrufen des Beweisers
    \item [Abgrenzung] Keine automatische Findung von Schleifeninvarianten
\end{description}%

\subsection{Dokumentation und Beispielsammlung}%

\begin{description}%
    \item [Muss] Dokumentation f"ur die verwendete Programmier- und Annotationssprache%
    \item [Muss] Mitgelieferte Sammlung von kommentierten und spezifizierten Beispielprogrammen zur Verdeutlichung der Funktionalit"at von \textit{Worthwhile}%
\end{description}%
{'fraction_non_alphanumeric': 0.08177699193281025, 'fraction_numerical': 0.0, 'mean_word_length': 5.267313019390581, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '104629', 'n_tokens_mistral': 3099, 'n_tokens_neox': 3102, 'n_words': 876}