<commit_before>\section{Sprachdefinition}

\subsection{Trennung von Befehlen}

Die Trennung aufeinanderfolgender Befehle wird dadurch erreicht, dass in jeder Zeile höchstens ein Befehl stehen darf. Dies dient der Übersichtlichkeit, da hiermit Befehlstrenner wie das Semikolon unnötig werden.

\subsection{Operatorreihenfolge}

Die folgende Tabelle gibt die Reihenfolge an, in der Operatoren ausgewertet werden. Dabei werden die Operatoren mit höchster Priorität zuerst ausgewertet.

Operatoren mit gleicher Priorität werden von links nach rechts ausgewertet. Durch Klammersetzung kann die Auswertungsreihenfolge beeinflusst werden.

\begin{figure}[H]
\begin{tabular}{|l|l|}
\hline
\textbf{Priorität} & \textbf{Operatoren} \\
\hline
8 & \texttt{{[}\,{]}} \\
\hline
7 & $\neg, -, +$ (unäre Operatoren)\\
\hline
6 & $\cdot, \div, \%$\\
\hline
5 & $+, -$\\
\hline
4 & $<, \leq, \geq, >$\\
\hline
3 & $=$\\
\hline
2 & $\wedge$ \\
\hline
1 & $\vee$ \\
\hline
\end{tabular}
\end{figure}

\subsection{Formale Definition der Grammatik}

Ein Worthwhile-Programm besteht aus genau einem Element des Typs \textit{program}.

\setlength{\grammarindent}{12em} % increase separation between LHS/RH

\begin{grammar}

<program> ::= (<funcdecl> | <statement> | <axiom>)* 

<funcdecl> ::= `function' <type> <name> `('<parameter>*`)' \\ (<requires> | <ensures>)* \\ <block>

<statement> ::= <vardecl> | <assign> | <block> | <annotation> | <funccall> | <conditional> | <loop> | <return>

<axiom> ::= `_axiom' <quantifiedexpr>

<requires> ::= `_requires' <predformula>

<ensures> ::= `_ensures' <predformula>

<block> ::= `{' <statement>* `}'

<vardecl> ::= <type> <name> ( `:=' <expr> )?

<assign> ::= <varref> `:=' <expr>

<varref> ::= <name> (`[' <expr> `]' )?

<annotation> ::= (`_assert' | `_assume') <predformula>

<funccall> ::= <name> `(' (<expr> (`,' <expr>)* )? `)'

<conditional> ::= `if' <expr> \\ <block>  \\ (`else' \\ <block>)?

<loop> ::= `while' <expr> \\ <invariant> \\ <block>

<invariant> ::= `_invariant' <predformula>

<return> ::= `return' <expr>

<predformula> ::= <expr> | <quantifiedexpr>

<quantifiedexpr> ::= (\lit{$\forall$} | \lit{$\exists$} ) <type> <name> (`,' <expr>) (<quantifiedexpr> | `:' <expr>)

<expr> ::= <prefixop> <expr> | <expr> <binop> <expr> | <expr> <postfixop> | `(' <expr> `)' | <arraylen> | <literal> | <varref> | <funccall>

<arraylen> ::= `length' `(' <expr> `)'

<literal> ::= `false' | `true' | <integer>

<type> ::= <primitivetype> | <arraytype>

<primitivetype> ::= `Integer' | `Boolean'

<arraytype> ::= <primitivetype> `[' <expr> `]'

<parameter> ::= <type> <name>

<binop> ::= $\vee$ | $\wedge$ | $\textless$ | $\leq$ | $=$ | $\geq$ | $>$ | $+$ | $-$ | $\cdot$ | $/$

<prefixop> ::= $-$ | $+$ | $\neg$

<postfixop> ::= `[' <expr> `]'

<name> ::=  [`A--Za--z'][`A--Za--z0--9']*

\end{grammar}

\subsection{Reservierte Schlüsselwörter}

Folgende Schlüsselwörter sind für die Verwendung innerhalb der Sprache reserviert und dürfen daher nicht als Bezeichner für Variablen oder Funktionen verwendet werden:

\begin{itemize}
	\item \texttt{function}
	\item \texttt{Integer}
	\item \texttt{Boolean}
	\item \texttt{false}
	\item \texttt{true}	
	\item \texttt{\_axiom}
	\item \texttt{\_assert}
	\item \texttt{\_assume}
	\item \texttt{\_requires}
	\item \texttt{\_ensures}
	\item \texttt{if}
	\item \texttt{else}	
	\item \texttt{while}		
	\item \texttt{return}	
\end{itemize}

\subsection{Semantische Einschränkungen}
Aus der Semantik der Sprache ergeben sich weitere Einschränkungen, die nicht in der Sprachdefinition abgebildet sind:

\begin{itemize}
	\item Eine Variable kann nur in Anweisungen referenziert werden, die nach der Deklaration stehen (insbesondere also nicht in der Deklaration selbst).
	\item Eine Funktion kann nur in Anweisungen referenziert werden, die nach der Funktionsdefintion stehen (insbesondere also nicht in der Funktion selbst). Damit wird effektiv die Verwendung von Rekursion verunmöglicht.
	\item Eine \textit{return}-Anweisung kann nur innerhalb einer Funktion stehen.
	\item Eine Funktion muss einen Rückgabewert haben; es müssen also alle möglichen Codepfade innerhalb der Funktion eine \textit{return}-Anweisung beinhalten.
	\item Nach Ausführung der \textit{return}-Anweisung wird die Funktion verlassen und keine weiteren Anweisungen der Funktion werden ausgeführt.
	\item Wenn bei der Deklaration einer Variablen kein Wert festgelegt wird, wird ein Standardwert angenommen. Dieser ist 0 für Variablen vom Type \int{}, \texttt{false} für Variablen vom Typ \bool{} und ein Array mit Standardwerten des jeweiligen Typs für Arrays.
\end{itemize}

\subsection{Alternative Darstellungsweisen für mathematische Symbole}
\label{textrep}
Einige mathematische Symbole sind auf Tastaturen nicht verfügbar. Daher sind folgende textuelle Alternativen vorgesehen, um die Sprache auch ohne die Hilfe einer IDE editieren zu können:

\begin{figure}[H]
\begin{tabular}{|l|l|}
\hline
\textbf{Symbol} & \textbf{Alternative} \\<commit_msg>[entwurf] Passe Sprachdefinition an AST-Modell an<commit_after>\section{Sprachdefinition}

\subsection{Trennung von Befehlen}

Die Trennung aufeinanderfolgender Befehle wird dadurch erreicht, dass in jeder Zeile höchstens ein Befehl stehen darf. Dies dient der Übersichtlichkeit, da hiermit Befehlstrenner wie das Semikolon unnötig werden.

\subsection{Operatorreihenfolge}

Die folgende Tabelle gibt die Reihenfolge an, in der Operatoren ausgewertet werden. Dabei werden die Operatoren mit höchster Priorität zuerst ausgewertet.

Operatoren mit gleicher Priorität werden von links nach rechts ausgewertet. Durch Klammersetzung kann die Auswertungsreihenfolge beeinflusst werden.

\begin{figure}[H]
\begin{tabular}{|l|l|}
\hline
\textbf{Priorität} & \textbf{Operatoren} \\
\hline
8 & \texttt{{[}\,{]}} \\
\hline
7 & $\neg, -, +$ (unäre Operatoren)\\
\hline
6 & $\cdot, \div, \%$\\
\hline
5 & $+, -$\\
\hline
4 & $<, \leq, \geq, >$\\
\hline
3 & $=$\\
\hline
2 & $\wedge$ \\
\hline
1 & $\vee$ \\
\hline
\end{tabular}
\end{figure}

\subsection{Formale Definition der Grammatik}

Ein Worthwhile-Programm besteht aus genau einem Element des Typs \textit{program}.

\setlength{\grammarindent}{12em} % increase separation between LHS/RH

\begin{grammar}

<program> ::= (<funcdecl> | <axiom>)* <block>? (<funcdecl> | <axiom>)*

<funcdecl> ::= `function' <type> <name> `(' <parameter>* `)' \\ (<precondition> | <postcondition>)* \\ `{' <block> `}'

<statement> ::= <vardecl> | <assign> | <block> | <annotation> | <funccall> | <conditional> | <loop> | <return>

<axiom> ::= `_axiom' <predformula>

<precondition> ::= `_requires' <predformula>

<postcondition> ::= `_ensures' <predformula>

<block> ::= <statement>*

<vardecl> ::= <type> <name> ( `:=' <expr> )?

<assign> ::= <varref> `:=' <expr>

<varref> ::= <name> (`[' <expr> `]' )?

<annotation> ::= (`_assert' | `_assume') <predformula>

<funccall> ::= <name> `(' (<expr> (`,' <expr>)* )? `)'

<conditional> ::= `if' <expr> \\ `{' <block> `}'  \\ (`else' \\ `{' <block> `}')?

<loop> ::= `while' <expr> \\ <invariant> \\ `{' <block> `}'

<invariant> ::= `_invariant' <predformula>

<return> ::= `return' <expr>

<predformula> ::= <expr> | <quantifiedexpr>

<quantifiedexpr> ::= (\lit{$\forall$} | \lit{$\exists$} ) <type> <name> (`,' <expr>) (<quantifiedexpr> | `:' <expr>)

<expr> ::= <prefixop> <expr> | <expr> <binop> <expr> | <expr> <postfixop> | `(' <expr> `)' | <arraylen> | <literal> | <varref> | <funccall>

<arraylen> ::= `length' `(' <expr> `)'

<literal> ::= `false' | `true' | <integer> | `{' <expr>* `}'

<type> ::= <primitivetype> | <arraytype>

<primitivetype> ::= `Integer' | `Boolean'

<arraytype> ::= <primitivetype> `[' <expr> `]'

<parameter> ::= <type> <name>

<binop> ::= $\vee$ | $\wedge$ | $\textless$ | $\leq$ | $=$ | $\geq$ | $>$ | $+$ | $-$ | $\cdot$ | $/$

<prefixop> ::= $-$ | $+$ | $\neg$

<postfixop> ::= `[' <expr> `]'

<name> ::=  [`A--Za--z'][`A--Za--z0--9-\_']*

\end{grammar}

\subsection{Reservierte Schlüsselwörter}

Folgende Schlüsselwörter sind für die Verwendung innerhalb der Sprache reserviert und dürfen daher nicht als Bezeichner für Variablen oder Funktionen verwendet werden:

\begin{itemize}
	\item \texttt{function}
	\item \texttt{Integer}
	\item \texttt{Boolean}
	\item \texttt{false}
	\item \texttt{true}	
	\item \texttt{\_axiom}
	\item \texttt{\_assert}
	\item \texttt{\_assume}
	\item \texttt{\_requires}
	\item \texttt{\_ensures}
	\item \texttt{if}
	\item \texttt{else}	
	\item \texttt{while}		
	\item \texttt{return}
	\item \texttt{length}
\end{itemize}

\subsection{Semantische Einschränkungen}
Aus der Semantik der Sprache ergeben sich weitere Einschränkungen, die nicht in der Sprachdefinition abgebildet sind:

\begin{itemize}
	\item Eine Variable kann nur in Anweisungen referenziert werden, die nach der Deklaration stehen (insbesondere also nicht in der Deklaration selbst).
	\item Eine Funktion kann nur in Anweisungen referenziert werden, die nach der Funktionsdefintion stehen (insbesondere also nicht in der Funktion selbst). Damit wird effektiv die Verwendung von Rekursion verunmöglicht.
	\item Eine \textit{return}-Anweisung kann nur innerhalb einer Funktion stehen.
	\item Eine Funktion muss einen Rückgabewert haben; es müssen also alle möglichen Codepfade innerhalb der Funktion eine \textit{return}-Anweisung beinhalten.
	\item Nach Ausführung der \textit{return}-Anweisung wird die Funktion verlassen und keine weiteren Anweisungen der Funktion werden ausgeführt.
	\item Wenn bei der Deklaration einer Variablen kein Wert festgelegt wird, wird ein Standardwert angenommen. Dieser ist 0 für Variablen vom Type \int{}, \texttt{false} für Variablen vom Typ \bool{} und ein Array mit Standardwerten des jeweiligen Typs für Arrays.
\end{itemize}

\subsection{Alternative Darstellungsweisen für mathematische Symbole}
\label{textrep}
Einige mathematische Symbole sind auf Tastaturen nicht verfügbar. Daher sind folgende textuelle Alternativen vorgesehen, um die Sprache auch ohne die Hilfe einer IDE editieren zu können:

\begin{figure}[H]
\begin{tabular}{|l|l|}
\hline
\textbf{Symbol} & \textbf{Alternative} \\
{'fraction_non_alphanumeric': 0.1720419469726949, 'fraction_numerical': 0.0025722200237435692, 'mean_word_length': 4.724235560588902, 'pattern_counts': {'":': 0, '<': 202, '<?xml version=': 0, '>': 204, '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': '4123645', 'n_tokens_mistral': 3792, 'n_tokens_neox': 3771, 'n_words': 998}