<commit_before>\documentclass{article}
\begin{document}

\title{Use Cases to Predicates}
\author{<NAME>\\\texttt{<EMAIL>}}
\maketitle

\section{Sample}

Verbal form:

\begin{verbatim}
User includes: name, and photo-s.
  
Photo is a "binary file with a name".
    
UC1: User (the user) extends photo album:
  1. The user "sends image file by HTTP".
  2. "We validate received file".
  3. We create photo of the user (the photo).
  4. The user reads the photo.

UC1: 0a) If number of photos of the user is greater than 5:
  1. The user deletes photo of himself.
\end{verbatim}

Formal:
    
\newcommand{\type}[1]{\mbox{\texttt{#1}}}
\vspace*{1em}
\begin{tabular}{l}
$uc_1(u):$ \\
$\quad (u \in \type{User}) \bigwedge$ \\
$\quad \neg(\| u . \| > 5) \bigwedge$ \\
$\quad inf(\type{"The user sends image file by HTTP"}) \bigwedge$ \\
$\quad inf(\type{"We validate received file"}) \bigwedge$ \\
$\quad (\type{"We validate received file"}) \bigwedge$ \\
\end{tabular}
    
\end{document}<commit_msg>theory polished, first draft looks good<commit_after>\documentclass{article}
\begin{document}
\setlength{\parindent}{0pt}
\setlength{\parskip}{1em}
\newcommand{\type}[1]{\mbox{\texttt{#1}}}
\newenvironment{maths}
{
    \vspace*{1em}
    \begin{tabular}{l}
}
{
    \end{tabular}
    \vspace*{1em}
}

\title{Use Cases to Predicates}
\author{<NAME>\\\texttt{<EMAIL>}}
\maketitle

\newpage
\section{Classes}

    Verbal form of a type/class (C++ as an example):

    \begin{verbatim}
struct User {
    unsigned int id; // unique ID of the user
    string email; // email address
    vector<Photo> photos; // a collection of photos
    User& manager; // user's manager, if any
}\end{verbatim}

    Formal ($\Pi_i$ is a set):
    
    \begin{maths}
    $\type{User}(x) =$ \\
    $\quad \exists \Pi_1 (|\Pi_1| = 1 \wedge \forall p(p \in \Pi_1 \to \type{integer}(p) \wedge \type{composition}(x, p)) \bigwedge$ \\
    $\quad \exists \Pi_2 (|\Pi_2| = 1 \wedge \forall p(p \in \Pi_2 \to \type{string}(p) \wedge \type{composition}(x, p)) \bigwedge$ \\
    $\quad \exists \Pi_3 (|\Pi_3| \geq 0 \wedge \forall p(p \in \Pi_3 \to \type{Photo}(p) \wedge \type{composition}(x, p)) \bigwedge$ \\
    $\quad \exists \Pi_4 (|\Pi_4| < 2 \wedge \forall p(p \in \Pi_4 \to \type{User}(p) \wedge \type{aggregation}(x, p))$ \\
    \end{maths}
    
    There are a number of sub-predicates:

    \begin{maths}
    $\type{User.id}(x, \Pi) = (|\Pi| = 1 \wedge \forall p(p \in \Pi \to \type{integer}(p) \wedge \type{composition}(x, p))$ \\
    \end{maths}
    
\newpage
\section{Use Cases}

    Verbal form of a use case:
    
    \begin{verbatim}
    UC1: User (the user) extends photo album:
      1. The user creates photo of himself (the photo).
      2. We validate the photo.
      3. The user reads the photo.
    UC1: 0a) If number of photos of the user is greater than 5:
      1. The user deletes photo of himself.
    UC1: 2a) If failed with "file format is not valid":
      1. We delete the photo.
      2. Fail with "only PNG images are accepted".\end{verbatim}

    Every use case is a predicate:
    
    \begin{maths}
    $\type{UC}_1(x) = $ \\
    $\quad \type{User}(x) \leftarrow$ \\
    $\quad \exists \Pi(\type{User.photos}(x, \Pi)) \leftarrow$ \\
    $\quad ($ \\
    $\quad\quad |\Pi| > 5 \leftarrow$ \\
    $\quad\quad \exists y(y \in \Pi) \leftarrow$ \\
    $\quad\quad \type{deleted}(y)$ \\
    $\quad ) \leftarrow$ \\
    $\quad \exists p(p \in \Pi) \leftarrow$ \\
    $\quad \type{created}(p) \leftarrow$ \\
    $\quad \type{UC}_2(p) \leftarrow$ \\
    $\quad ($ \\
    $\quad\quad \type{exception}(\mbox{"file format is not valid"}) \leftarrow$ \\
    $\quad\quad \type{deleted}(p) \leftarrow$ \\
    $\quad\quad \type{throw}(\mbox{"only PNG images are accepted"})$ \\
    $\quad ) \leftarrow$ \\
    $\quad \type{read}(x, p)$ \\
    \end{maths}
    
    System functionality is defined by invariants:

    \begin{maths}
    $\forall x(\type{UC}_1(x))$ \\
    \end{maths}
    
\newpage
\section{Basic Predicates}

    Basic fundamental predicates:

    \begin{maths}
    $\type{composition}(x, y) = \dots$ \\
    $\type{aggregation}(x, y) = \dots$ \\
    $\type{created}(x) = \dots$ \\
    $\type{deleted}(x) = \dots$ \\
    $\type{read}(x) = \dots$ \\
    $\type{exception}(x) = \dots$ \\
    $\type{throw}(x) = \dots$ \\
    \end{maths}

    Primitive types:

    \begin{maths}
    $\type{integer}(x) = \dots$ \\
    $\type{string}(x) = \dots$ \\
    $\type{float}(x) = \dots$ \\
    $\type{boolean}(x) = \dots$ \\
    \end{maths}


\end{document}
{'fraction_non_alphanumeric': 0.19185022026431717, 'fraction_numerical': 0.011674008810572687, 'mean_word_length': 2.550430023455825, 'pattern_counts': {'":': 1, '<': 9, '<?xml version=': 0, '>': 10, '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': '2621714', 'n_tokens_mistral': 1711, 'n_tokens_neox': 1643, 'n_words': 465}