Polish

Trajectories/Documentation_texfol/documentation.tex

@@ -9,6 +9,7 @@
 
 \usepackage{algorithmic}
 \usepackage{babel}
+\usepackage{latexsym}
 \usepackage{graphicx}
 
 \usepackage[np]{numprint}
@@ -199,6 +200,54 @@ ré-utilisons le tableau properties. Cela aurait dégradé la lisibilité
 de l'algorithme et la différence de performance doit être faible dans
 la mesure où le coût de calcul d'une date est faible.
 
+Fonction \verb+search_beg+. Notons :
+\begin{equation*}
+  i_0 = \min(\mathtt{max\_delta} + 1, \mathtt{len}(\mathtt{inst\_eddies}))
+\end{equation*}
+Montrons que :
+\begin{equation*}
+  \forall e \in \mathtt{inst\_eddies}[i_0:], d(e) > d_\mathrm{max}
+\end{equation*}
+Si $i_0 < \mathtt{len}(\mathtt{inst\_eddies})$ alors :
+\begin{equation*}
+  i_0 = \mathtt{max\_delta} + 1
+\end{equation*}
+Donc $\mathtt{max\_delta} + 1$ est dans la plage d'indices de
+\verb+inst_eddies+. Puisque les tourbillons instantanés dans un
+segment sont toujours séparés d'au moins 1 en indice de date :
+\begin{align*}
+  d(\mathtt{inst\_eddies}[\mathtt{max\_delta} + 1])
+  & \ge d(\mathtt{inst\_eddies}[0]) + \mathtt{max\_delta} + 1 \\
+  & > d_\mathrm{max}
+\end{align*}
+Par ailleurs, si $i_0 = \mathtt{len}(\mathtt{inst\_eddies})$ alors
+$\mathtt{inst\_eddies}[i_0:]$ est vide. $\Box$
+
+Fonction \verb+search_end+. Notons :
+\begin{equation*}
+  i_0 = \max(i_\mathrm{max} - \mathtt{max\_delta}, 0)
+\end{equation*}
+Montrons que :
+\begin{equation*}
+  \forall e \in \mathtt{inst\_eddies}[:i_0], d(e) < d_\mathrm{min}
+\end{equation*}
+Si $i_0 > 0$ alors :
+\begin{equation*}
+  i_0 = i_\mathrm{max} - \mathtt{max\_delta}
+\end{equation*}
+Donc $i_0 - 1$ est dans la plage d'indices de
+\verb+inst_eddies+. Puisque les tourbillons instantanés dans un
+segment sont toujours séparés d'au moins 1 en indice de date :
+\begin{align*}
+  d(\mathtt{inst\_eddies}[i_0 - 1])
+  & = d(\mathtt{inst\_eddies}[i_\mathrm{max} - \mathtt{max\_delta} -
+    1]) \\
+  & \le d(\mathtt{inst\_eddies}[i_\mathrm{max}]) - \mathtt{max\_delta} - 1 \\
+  & < d_\mathrm{min}
+\end{align*}
+Par ailleurs, si $i_0 = 0$ alors $\mathtt{inst\_eddies}[:i_0]$ est
+vide. $\Box$
+
 \section{Script \texttt{trajectory.py}}
 
 Les trajectoires sont presque toujours, mais pas toujours, des

Trajectories/cost_function.py

@@ -122,7 +122,8 @@ def search_beg(inst_eddies, max_delta, avg_fix, e_overestim):
             )
             + max_delta
         )
-        # {date(elem) > d_max for elem in inst_eddies[ip:]}
+        # assertion: date(inst_eddies[0]) <= d_max
+        # assertion: date(elem) > d_max for elem in inst_eddies[ip:]
 
         while (
             ip >= 2
@@ -133,10 +134,10 @@ def search_beg(inst_eddies, max_delta, avg_fix, e_overestim):
         ):
             ip -= 1
 
-        # {date(elem) <= d_max for elem in inst_eddies[:ip] and
-        # date(elem) > d_max for elem in inst_eddies[ip:]}
+        # assertion: date(elem) <= d_max for elem in inst_eddies[:ip]
+        # and date(elem) > d_max for elem in inst_eddies[ip:]
 
-    # {1 <= ip <= min(max_delta + 1, len(inst_eddies))}
+    # assertion: 1 <= ip <= min(max_delta + 1, len(inst_eddies))
     return ip
 
 
@@ -160,7 +161,8 @@ def search_end(inst_eddies, max_delta, avg_fix, e_overestim):
             )
             - max_delta
         )
-        # {date(elem) < d_min for elem in inst_eddies[:ip]}
+        # assertion: date(inst_eddies[i_max]) >= d_min
+        # assertion: date(elem) < d_min for elem in inst_eddies[:ip]
 
         while (
             ip < i_max
@@ -171,10 +173,11 @@ def search_end(inst_eddies, max_delta, avg_fix, e_overestim):
         ):
             ip += 1
 
-        # {date(elem) < d_min for elem in inst_eddies[:ip] and
-        # date(elem) >= d_min for elem in inst_eddies[ip:]}
+        # assertion: date(elem) < d_min for elem in inst_eddies[:ip] and
+        # date(elem) >= d_min for elem in inst_eddies[ip:]
 
-    # {max(len(inst_eddies) - max_delta - 1, 0) <= ip <= len(inst_eddies) - 1}
+    # assertion: max(len(inst_eddies) - max_delta - 1, 0) <= ip <=
+    # len(inst_eddies) - 1
     return ip
 
 
@@ -304,6 +307,8 @@ for n in g.vertices():
 
             last_av_rad[n], last_av_ros[n] = calculate_radii_rossby(properties)
         else:
+            # assertion: ip_beg == len(g.vp.inst_eddies[n])
+            # assertion: len(g.vp.inst_eddies[n]) <= max_delta + 1
             # The number of eddies in the segment is lower than or
             # equal to the number of days over which to average. The
             # values for the end of the segment will be the same as