spark2014/docs/papers/loop-patterns/loop_patterns.tex

\documentclass[a4paper,10pt]{article}

%%packages
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{mathpartir}
\usepackage{amsmath}
\usepackage{xspace}
\usepackage{xcolor}
\usepackage{url}
\usepackage{amssymb}
\usepackage{stmaryrd}
%%
%%colors of the remarks
\newcommand{\yannick}[1]{{\color{red} #1}}
\newcommand{\Virginia}[1]{{\color{blue} #1}}
\newcommand{\Pierre}[1]{{\color{violet} #1}}
%%
%%abbreviations
\newcommand{\eg}{\textit{e.g.,}\xspace}
\newcommand{\etal}{\textit{et al.}\xspace}
\newcommand{\etc}{\textit{etc.}\xspace}
\newcommand{\p}[1]{\ensuremath{#1^{'}}\xspace}
%%
%%Commands used for defining syntax
\newcommand{\prog}{\ensuremath{\mathcal{L}}\xspace}
\newcommand{\idx}{\ensuremath{i}\xspace}
%\newcommand{\idxinitial}{\ensuremath{\mathit{initial}}\xspace}
\newcommand{\idxinitial}{\ensuremath{\alpha}\xspace}
%\newcommand{\idxfinal}{\ensuremath{\mathit{final}}\xspace}
\newcommand{\idxfinal}{\ensuremath{\omega}\xspace}
%\newcommand{\Init}{\ensuremath{\mathrm{Init_{0}}}}
\newcommand{\KWloop}{\ensuremath{\mathrm{\textbf{loop}}~}}
\newcommand{\KWdo}{\ensuremath{\mathrm{\textbf{do}}~}}
\newcommand{\KWend}{\ensuremath{\mathrm{\textbf{end}}}}
\newcommand{\KWover}{\ensuremath{\mathrm{\textbf{over}}~}}
\newcommand{\KWin}{\ensuremath{~\mathrm{\textbf{in}}~}}
\newcommand{\KWfor}{\ensuremath{\mathrm{\textbf{for}}~}}
\newcommand{\KWwhile}{\ensuremath{\mathrm{\textbf{while}}~}}
\newcommand{\KWexit}{\ensuremath{\mathrm{\textbf{exit when}}~}}
\newcommand{\KWassign}{\ensuremath{\mathrm{\textbf{assign}}~}}
\newcommand{\KWor}{\ensuremath{\mathrm{\textbf{or}}~}}
\newcommand{\KWskip}{\ensuremath{\mathrm{\textbf{skip}}~}}
\newcommand{\SG}{\ensuremath{\mathrm{G_{loc}}~}}
\newcommand{\Sga}{\ensuremath{\mathrm{ga_{loc}}~}}
\newcommand{\SB}{\ensuremath{\mathit{B}}}
\newcommand{\Sloc}{\ensuremath{loc~}}
\newcommand{\SLoc}{\ensuremath{\mathrm{\textbf{Loc}}~}}
\newcommand{\Sstate}{\ensuremath{\mathrm{\textbf{State}}~}}
\newcommand{\SZ}{\ensuremath{\mathrm{\textbf{Z}}~}}
\newcommand{\ST}{\ensuremath{\mathrm{\textbf{T}}~}}
\newcommand{\SAexp}{\ensuremath{\mathrm{\textbf{Aexp}}~}}
\newcommand{\SBexp}{\ensuremath{\mathrm{\textbf{Bexp}}~}}
\newcommand{\gexit}{\ensuremath{\mathit{g_{exit}~}}}
%%
%%Commands used for defining semantic
\DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
\newcommand{\SemF}[3]{\ensuremath{#1 \llbracket #2 \rrbracket_{#3} \xspace}}
\newcommand{\SemFA}[2]{\SemF{\mathpzc{A}}{#1}{#2}}
\newcommand{\SemFB}[2]{\SemF{\mathpzc{B}}{#1}{#2}}
\newcommand{\cadre}[1]{\fbox{\begin{minipage}{\textwidth} #1 \end{minipage}}}
\newcommand{\env}{\ensuremath{\sigma}\xspace}
\newcommand{\eval}[2]{<#1, #2>}
%%
%%Predicates
\newcommand{\Pbetween}{\ensuremath{\mathit{between}}\xspace}
\newcommand{\betweens}[3]{\ensuremath{\mathit{between}{(#1,#2,#3)}}\xspace}
\newcommand{\Pinbounds}[1]{\ensuremath{\mathit{inbounds}_{#1}}\xspace}
\newcommand{\inbounds}[2]{\ensuremath{\mathit{inbounds}_{#1}(#2)}\xspace}
\newcommand{\inrange}[1]{\ensuremath{\mathit{inrange}(#1)}\xspace}
\newcommand{\Pseen}{\ensuremath{\mathit{seen}}\xspace}
\newcommand{\seen}[2]{\ensuremath{\mathit{seen}{(#1,#2)}}\xspace}
\newcommand{\tocount}[1]{\ensuremath{\mathit{tocount}(#1)}\xspace}
\newcommand{\Ftocount}{\ensuremath{\mathit{tocount}}\xspace}
\newcommand{\update}[3]{\ensuremath{\mathit{update}{(#1,#2,#3)}}\xspace}
\newcommand{\group}[2]{\ensuremath{\mathit{G}_{#1}(#2)}\xspace}
\newcommand{\Inv}[1]{\ensuremath{\mathit{Inv}(#1)\xspace}}
\newcommand{\inv}{\ensuremath{\textsc{inv}}\xspace}
\newcommand{\pat}{\ensuremath{\textsc{pat}}\xspace}
\newcommand{\writedisjoint}[2]{\ensuremath{\mathit{W_D}(#1,#2)}\xspace}
\newcommand{\var}[1]{\ensuremath{\mathit{Var}_{#1}}\xspace}
\newcommand{\at}[1]{{(#1)}}
\newcommand{\capture}[2]{\ensuremath{\mathit{Capture}(#1,#2)}\xspace}
\newcommand{\sli}[1]{\ensuremath{\mathit{SLI}_{#1}}\xspace}

\newcommand{\initcond}[1]{\ensuremath{\mathit{Init_{#1}}}}
\newcommand{\framecond}[1]{\ensuremath{\mathit{Frame_{#1}}}}
\newcommand{\preservecond}[2]{\ensuremath{\mathit{Preserve_{#1}(#2)}}}

%%
%%keywords
\newcommand{\loopform}{\textsc{loop-form}\xspace}
\newcommand{\loopinvariant}{\noindent\textit{Loop invariant:}\xspace}
\newcommand{\patterndef}{\noindent\textit{Definition:}\xspace}
\newcommand{\patternexample}{\noindent\textit{Example:}\xspace}
\newcommand{\patternnote}{\noindent\textit{Note:}\xspace}
\newcommand{\patternproof}{\noindent\textit{Proof:}\xspace}
\newcommand{\symdef}{\ensuremath{\overset{\mathit{def}}{=}}}
\newcommand{\N}{\ensuremath{N}\xspace}
\newcommand{\true}{\ensuremath{\mathit{true}}}
\newcommand{\false}{\ensuremath{\mathit{false}}}
\newcommand{\impl}{\ensuremath{\Longrightarrow}}
%%
%%Proof preliminaires
\newcommand{\maxinv}{\textsc{max-inv}\xspace}
\newcommand{\sppost}{\textsc{sp-post}\xspace}
\newcommand{\spstrong}{\textsc{sp-strg}\xspace}
\newcommand{\spmonoton}{\textsc{sp-mono}\xspace}
\newcommand{\vpp}{\textsc{vpp}\xspace}
\newcommand{\spexit}{\textsc{sp-exit}\xspace}
\newcommand{\spscalar}{\textsc{sp-scalar}\xspace}
\newcommand{\sparray}{\textsc{sp-array}\xspace}
\newcommand{\spseq}{\textsc{sp-seq}\xspace}
\newcommand{\sppar}{\textsc{sp-par}\xspace}
\newcommand{\mcdiff}{\textsc{mc-diff}\xspace}
\newcommand{\mcsame}{\textsc{mc-same}\xspace}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{hypothesis}[theorem]{Hypothesis}
\newcounter{proofnum} % proof numbering
\newcounter{subproofnum}[proofnum] % subproof numbering
\newcommand{\subproof}[1]{\refstepcounter{subproofnum}~\\\noindent\arabic{subproofnum}. #1\\}
\newcounter{subsubproofnum}[subproofnum] % subsubproof numbering
\newcommand{\subsubproof}[1]{\refstepcounter{subsubproofnum}~\\\noindent\arabic{subproofnum}.\arabic{subsubproofnum}. #1\\}

\newcounter{pc} % pattern counter
\newcommand{\curpattern}{\ensuremath{\textsc{pat}\mathrm{\arabic{pc}}}\xspace}
\newcommand{\curinv}{\ensuremath{\textsc{inv}\mathrm{\arabic{pc}}}\xspace}
\newcommand{\anyinv}{\ensuremath{\textsc{inv}\mathrm{x}}\xspace}

\newenvironment{proof}[1][Proof.]{\refstepcounter{proofnum}\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{definition}[1][Definition]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{example}[1][Example]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
\newenvironment{remark}[1][Remark]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}

\newcommand{\spostsym}{\ensuremath{sp}\xspace}
\newcommand{\spost}[2]{\ensuremath{\spostsym(#1,#2)}}
\newcommand{\subst}[3]{\ensuremath{#1[#2 \leftarrow #3]}}

\newcommand{\qed}{\nobreak \ifvmode \relax \else
      \ifdim\lastskip<1.5em \hskip-\lastskip
      \hskip1.5em plus0em minus0.5em \fi \nobreak
      \vrule height0.75em width0.5em depth0.25em\fi}

\lstset{language=Ada}

\sloppy

%==================================================================================
%==================================================================================
\begin{document}

% Title Page
\title{Simple Loop Patterns and Rich Loop Invariants}
\author{Marc Sango, Maria-Virginia Aponte, \\ Pierre Courtieu and Yannick Moy}
\date{}

\maketitle

\begin{abstract}
  Most works in automatic generation of loop invariants are limited to simple
  forms of invariants without quantifiers. In this paper, we describe patterns
  of loops for which it is possible to generate rich loop invariants with
  quantifiers.
\end{abstract}

%==================================================================================
%==================================================================================
\section{Introduction}

In the following, we only consider techniques that generate loop invariants for
programs with scalar and array variables. There is a wealth of different
techniques that generate invariants regarding the shape of
dynamically-allocated data structures (shape analysis, separation logic) that
are irrelevant in our context. We also ignore all techniques for generating
invariants for hybrid programs, in which a program implements a control part
which is related to an outside world obeying continuous differential equations.

There have been two approaches to loop invariant generation: a
\textit{template} approach which takes only code as input and generates the
best loop invariants in some predefined template family; a \textit{directed}
approach which also takes as input a goal or some hint formulas, and generates
either a sufficient loop invariant to prove the goal or a loop invariant based
on the hints provided. Typically, template approaches are based on abstract
interpretation or algebraic techniques while directed approaches are based on
theorem proving or model checking techniques.

%==================================================================================
%==================================================================================
\subsection{Simple Loop Invariants}

Most techniques generate loop invariants in the form of conjunctions of
(dis)equalities between polynomials in the program variables. The form of an
individual (dis)equality ranges from constant variable bounds for a variable
(sign, interval) to polynomial linear (dis)equalities of various complexity (2
or 3 variables, templates of polynomials) and non-linear polynomials.

Abstract interpretation~\cite{cousot:1978:popl, mine:2006:hosc} works on an
abstraction of the program using predefined domains which restrict the kind of
(dis)equalities we are looking for. Non-relational domains such as intervals
define (dis)equalities between a single program variable and
constants. Relational domains such as octagons or polyhedra define
(dis)equalities between program variables. An abstract state represents all
known (dis)equalities in the abstract domain. Abstract interpretation simulates
execution over this abstract state to reach a fixpoint which defines invariants
at each program point.

Predicate abstraction~\cite{graf:1997:cav} applies abstract interpretation to a
domain of predefined base formulas, typically collected from guards present in
the program (tests in branch and loop statements). A theorem prover is used to
compute the transition function for each statement of the program. The final
invariants are conjunctions over the initial base formulas.

An obvious limitation of predicate abstraction is its dependency on the initial
base formulas. In a goal-directed approach where the invariant computed by
predicate abstraction is not sufficient to prove the goal, Craig's
interpolation~\cite{mcmillan:2003:cav, mcmillan:2006:cav} allows to generate
intermediate formulas from two inconsistent formulas. In the CEGAR
(Counter-Example Guided Abstraction Refinement) approach, predicate abstraction
can then be reapplied on these intermediate formulas until a sufficient
invariant is found.

Algebraic techniques~\cite{colon:2003:cav, sankaranarayanan:2004:popl,
  kovacs:2008:csr} first extract polynomial (dis)equalities over program
variables and unknown constants from a template loop invariant defining these
unknowns. Then, algebraic techniques such as Faskas lemma or Gröbner bases are
used to solve these (dis)equations and give values to unknowns.

%==================================================================================
%==================================================================================
\subsection{Richer Loop Invariants}

\subsubsection*{Disjunctions}

Various works have defined disjunctive abstract domains on top of base abstract
domains. The implication domain only deals with one disjunction at a time,
while disjunctive completion~\cite{Mauborgne:trace-partitioning} allows to
treat larger disjuncts. The need to define converging operators for these
domains means that they are not very precise. New techniques are invented each
year to treat disjunctions in static analyzers~\cite{Harris:2010:PAV,
  Sharma:2011:cav}.

\subsubsection*{Quantifiers}

A few works have targeted the generation of loop invariants with a richer
boolean structure and quantifiers, based on techniques for quantifier-free
invariants.

Halbwachs and Péron~\cite{halbwachs:2008:pldi} describe an abstract domain to
reason about array contents over \textit{simple programs} that they describe as
\textit{``one-dimensional arrays, traversed by simple for loops''}. They are
able to represent facts like $(\forall i)(2 \leq i \leq n \impl A[i] \geq
A[i−1]$, in which a pointwise relation is established between elements of array
slices, where the relation is one supported by a quantifier-free base abstract
domain.

Gulwani \etal~\cite{gulwani:2008:popl} describe a general lifting procedure
that creates a quantified disjunctive abstract domain from quantifier-free
domains. They are able to represent facts like $(\forall i)(0 \leq i < n \impl
a[i] = 0)$, in which the formula is universally quantified over an implication
between quantifier-free formulas of the base domains.

McMillan~\cite{mcmillan:2008:tacas} describes an instrumentation of a
resolution-based prover that generates quantified invariants describing facts
over simple arrays manipulating arrays. Using a similar technique, Kov\'acs and
Voronkov~\cite{kovacs:2009:fli} generate invariants containing quantifier
alternation.

%==================================================================================
%==================================================================================
\section{Simple loops on guarded assignments}
\label{sec:simple-loops}
We base our developpement on the intermediate language shown in figure~\ref{syntax}.
The language includes arithmetic and boolean  expressions, guarded assignments on
locations $l$, and for-like loops with exit conditions. Locations  correspond
either to scalar (noted $x$) or to array locations (with syntax $X[a]$).
\begin{figure}
\centering
\begin{lstlisting}[mathescape, frame=single, flexiblecolumns=false]{}
 $\KWloop \idx \KWin \idxinitial .. \idxfinal ~ \KWexit \gexit ~ \KWdo$
    $\KWassign l_1$ {
       $g_{l_{11}} \rightarrow l_1 := e_{l_{11}} \; ~\KWor$
        $\vdots$
       $g_{l_{1k}} \rightarrow l_1 := e_{l_{1k}}$
    }
      $\vdots$
    $\KWassign l_m$ {
       $g_{l_{m1}} \rightarrow l_m := e_{l_{m1}} \; ~\KWor$
        $\vdots$
       $g_{l_{mp}} \rightarrow l_m := e_{l_{mp}}$
    }
 $\KWend$
\end{lstlisting}
\caption{A simple loop program scheme}\label{program-scheme}
\end{figure}
%
Figure \ref{program-scheme} shows a typical loop program scheme in our language \prog.
A program in this language over an index \idx ranging from \idxinitial to \idxfinal values,
and possibly stating an exit condition \gexit.
A loop body $B$ consists in a (possibly empty) unordered collection of \emph{simultaneous}
\textit{group-assignments} on different locations $l_1, \ldots, l_m$.
A group-assignment declares a location $l_j$ to assign, that we note $G_{l_j}$.
It is meant to group together all guarded assignments on its declared location,
and it is formed by  a collection of unordered guarded assignments
$g_{l_{jk}} \rightarrow l_j := e_{l_{jk}}$ on $l_j$, such that any  two different guards
$g_{l_{jk1}}$, $g_{l_{jk2}}$ belonging to the same group-assignment are mutually exclusive.

\begin{figure}
\cadre{
$$
\begin{array}{lllr}
\prog & ::= &   \KWloop  \idx \KWin \idxinitial ..\idxfinal ~ \KWexit
b & \mathrm{for-loops}\\
          &       &   ~ \KWdo ~ {B} ~    \KWend \\
{B}           & ::= & \KWskip  ~|~ \SG [ \SG ]^*   & \mathrm{loop~
  body}\\
\SG & ::= & \KWassign ~ \Sloc ~ \{\Sga [ \KWor ~ \Sga ]^* \} &
\mathrm{group~assigns}\\
\Sga    & ::= & b  \rightarrow \Sloc :=  a &
\mathrm{guarded~assigns}\\
\Sloc   & ::= & x ~|~ X[a]  &
\mathrm{locations}\\
a       &  ::= &  n  ~|~ \Sloc  ~|~ a_1 + a_2 ~|~ a_1 - a_2 ~|~ a_1 *
e_2  &
\mathrm{arithmetic~expressions}\\
b       & ::= &  t ~|~ b_1 \wedge  b_2 ~|~ b_1 \vee  b_2  ~|~  \neg  b
~|~ a_1 \bullet a_2  &
\mathrm{boolean~expressions}\\
\end{array}
$$
\noindent where $\bullet \in \{<, \leq, >, \geq \}, n \in \SZ,
t \in \{\mathrm{true}, \mathrm{false} \}$
}
\caption{Syntax of the \prog  language }\label{syntax}
\end{figure}

\subsection{Semantic constraints on loops}

Let ${ B}$ be a loop body. We assume that any group-assignment $G_l$ in ${ B}$
contains only assignments on its specified location $l$, and that any other
group-assignment $G_{l'}$ in ${ B}$ is such that $l \neq l'$. We also assume
that there are no conflicting writes during simultaneous assignments,
which amounts to the following conditions:
\begin{enumerate}
\item For any two assignments to scalar variable $a$, whose guards are $g_j$
  and $g_k$, then $g_j \land g_k$ is unsatisfiable.
\item For any two assignments to array variable $A$ at indexes $e_j$ and $e_k$,
  with guards $g_j$ and $g_k$, then $(e_j = e_k) \land g_j \land g_k$ is
  unsatisfiable.
\end{enumerate}
Thus, guards occurring in the same group assignment are mutually unsatisfiable.
It follows that a group-assignment $G_l$ groups together all assignments on $l$
occuring in ${ B}$. Furthemore, on each iteration, only one assignments on $l$ will be performed.
Group assignments are executed simultaneously: expressions and guards are evaluated all together,
\textit{before} all assignments, with at most one assignment on each location.\\
The conditions on guarded assignments are essentially the same as the ones described by Kov\'acs
and Voronkov with a slightly different formalism~\cite{kovacs:2009:fli}.

\begin{definition} \emph{(Disjoints writings and well-formeness)}\\
A group assign $G_l$ is \textit{write-disjoint}, if
\begin{itemize}
\item[i.] $G_l$  contains only guarded assigns on $l$, and
\item[ii.] for any two different guards $g_{lp}$, $g_{lk}$ belonging to $G_l$,
           then $g_{lp} \land g_{lk}$ is unsatisfiable.
\end{itemize}
A loop body $B$ is \textit{write-disjoint} if
\begin{itemize}
\item[i.] all group assignments $G_{l_1}, \ldots, G_{l_n} \in B$ are declared
          on different locations, i.e., $l_k \neq l_p$ for any two different $k,p$, and
\item[ii.] all group assignments $G_{l_1}, \ldots, G_{l_n} \in B$ are write-dsjoint.
\end{itemize}
A loop $L$ with body $B$ is \textit{well-formed} if $B$ is write disjoint.
\end{definition}

%==================================================================================
\subsection{Naming Conventions}
\label{sec:naming-conventions}

We use the following conventions: lower-case letters $a$, $b$, $c$,
... correspond to  integer
variables; \idx is the loop index, which is not a variable and cannot be
assigned; upper-case letters $A$, $B$, $C$, ... are array variables; $e$ is an
expression; $K$ is a constant expression; $f$ is a pure function (it does not
write to variables). The guards expressions of assignment to variable $x$ (scalar variable or
array variable) denoted by letters $g_x$. Subscripted variables $a_0$ and $A_0$ denote
respectively the initial values before the loop of variables $a$ and $A$.
For simplicity, if we have an array A that is never updated in the loop, we
treat such an array A as a constant and simply use $A$ instead of $A_0$.
Expression $e_0$ denotes the expression $e$ where all variables have been replaced by their
initial values (this does not apply to the loop index \idx).
The special expression $e^?$ denotes an unknown value, and expression.
For simplicity, we denote the group assignment to variable $x$
$\group{x}{g_{x1} .. g_{xn}}$ instead of
{
\begin{lstlisting}[mathescape]{}
    $\KWassign x$ {
       $g_{x_{11}} \rightarrow x_1 := e_{x_{11}} \; ~\KWor$
        $\vdots$
       $g_{x_{1k}} \rightarrow x_1 := e_{x_{1k}}$
    }
\end{lstlisting}
}

Given an array $A$ with index bounds $\mathit{low}$ and $\mathit{up}$, we
define a predicate \Pinbounds{A} as follows:

$$\inbounds{A}{j} \equiv \mathit{low} \leq j \leq \mathit{up}$$

Given the loop index \idx ranging between $\idxinitial$ and $\idxfinal$,
we define a predicate \inrange{\idx} as follows:

$$\inrange{\idx} \equiv \idxinitial \leq \idx \leq \idxfinal$$

We define a predicate \Pseen which characterizes indexes which have already
been treated in the loop:

$$\seen{j}{\idx} \equiv \idxinitial \leq j <\idx$$

To treat the iteration monotonicity properties we define a predicate \Pbetween
and a logical function \Ftocount which count the number of loop round from increasing
loop, knowing that we can deduce the case of strictly decreasing by affine transformation.

\begin{eqnarray*}
&\betweens{j}{k}{\idx} \equiv j < k < \idx\\
\and
&\tocount{i} = i - \idxinitial + 1
\end{eqnarray*}

%==================================================================================
%==================================================================================
\section{Semantics}

In this section, we give two alternative semantics to the \prog  loop language.
Strongest postcondition semantics will be useful to show that each one of our
invariants is the strongest possible one. Operational semantics  will allow us to show
the soundness of the strongest postcondition semantics.

\subsection{Operational semantics}

We define a \textit{state} $\sigma$ as a partial function from locations to relative
integer values and $\Sstate$ as the set of all possible states:
$$\Sstate : \SLoc \hookrightarrow \SZ$$

We assume given two total \textit{semantic functions} $\mathpzc{A}$ and $\mathpzc{B}$
respectively giving the meaning of arithmetic and boolean expressions on a given state.
As usually, to apply these functions to particular expressions $e_a$ and $e_b$ and
state $\sigma$, we  use "semantic" brackets $\llbracket \rrbracket$, namely:
$\SemFA{e_a}{\sigma}$ and $\SemFB{e_b}{\sigma}$.
%$\mathpzc{A}\llbracket e_a \rrbracket_{\sigma}$.
\begin{eqnarray*}
\mathpzc{A}: & \SAexp \rightarrow (\Sstate \hookrightarrow \SZ)\\
\mathpzc{B}: & \SBexp \rightarrow (\Sstate \hookrightarrow \ST)\\
\end{eqnarray*}

We note $\sigma[l \mapsto v]$ the usual notion of substitution (or updating) on states,
defined to be the state equals to $\sigma$ except for location $l$ which is bound to value $v$:
$$
\sigma[l \mapsto v] (x)= \left \{
\begin{array}{ll}
v & \mathrm{if ~} x=l\\
\sigma(x) & \mathrm{otherwise}\\
\end{array}
\right.
$$
Notation $\sigma[l_1, l_2 \mapsto v_1, v_2]$ corresponds to simultaneous substitution
for locations $l_1$, $l_2$, provided that $l_1 \neq l_2$. Notation $\sigma - i$ stands
for the state $\sigma$ where index \idx, has been removed (becomes undefined):
$$
\sigma - i (x)= \left \{
\begin{array}{ll}
\mathrm{undef}  & \mathrm{if~} x=i\\
\sigma(x) & \mathrm{otherwise}\\
\end{array}
\right.
$$

As we translate for-loops from \prog into while loops, we introduce while loop syntax on
top of \prog and corresponding operational semantic rules. As while loops can only appear
while unrolling the semantics of a \prog loop, we restrict while-loops to those that execute
a for-loop body {B}  and finally increment the same loop index \idx:
$$
\begin{array}{lllr}
W_i & ::= &   \KWwhile  ~b~  \KWdo ~ {B}; i =i+1 ~    \KWend \\
\end{array}
$$

The For-loop rule performs an initialization step on index \idx and then loops as a while loop.
As index are local to the loop body, they not appear in the final state.
\begin{eqnarray*}
&
\inferrule[For-loop]{
\SemFA{\idxinitial}{\sigma} = v
\quad    \quad \sigma_o = \sigma[i \mapsto v] \\
\eval{\KWwhile (i \leq \idxfinal \wedge \neg b)~\KWdo  ~ {B}; ~i =i+1 ~\KWend }{\env_0} \rightsquigarrow \sigma_1\\
\sigma_2 = \sigma_1 - i \\
}{
\eval{\KWloop  \idx \KWin \idxinitial ..\idxfinal ~ \KWexit b ~ \KWdo B ~    \KWend}{\env} \rightsquigarrow \env_2
}\\
\end{eqnarray*}

Rules While-T and While-F are classical rules dealing with while loops except
that their body executes first a for-loop ${\cal B}$ and then proceeds by incrementing the loop index \idx.
\begin{eqnarray*}
&
\inferrule[While-T]{
\SemFB{b}{\sigma} = \mathrm{true}  \\
\eval{B}{\sigma}\rightsquigarrow \sigma_1\\
\sigma_2 = \sigma_1[i \mapsto \SemFA{i+1}{\sigma_1}]\\
\eval{\KWwhile~ b~\KWdo  ~ {B}; ~i =i+1 ~\KWend}{\sigma_2}\rightsquigarrow \sigma_3\\
}{
\eval{\KWwhile~ b~\KWdo  ~ { B}; ~i =i+1 ~\KWend}{\sigma} \rightsquigarrow \sigma_3
}\\
\end{eqnarray*}

\begin{eqnarray*}
&
\inferrule[While-F]{
\SemFB{b}{\sigma} = \mathrm{false}
%\eval{\KWwhile~ b~\KWdo  ~ {B}; ~i =i+1 ~\KWend}{\sigma_2}\rightsquigarrow \sigma\\
}{
\eval{\KWwhile~ b~\KWdo  ~ { B}; ~i =i+1 ~\KWend}{\sigma} \rightsquigarrow \sigma
}\\
\end{eqnarray*}

Rules B-empty and B-body deal with \prog loop bodies. B-empty correponds to an empty body.
In rule B-body, all group assignments $G_{l_k}$ are considered to assign on different
locations and are evaluated in a common state. Each group assignment $G_{l_k}$ results
in a singleton environnement corresponding to a new binding for location $l_k$.
Those binding are simultaneously updated in the final state.

{\small
$$
\begin{array}{cc}
%
\inferrule[B-empty]{ }
{\eval{\KWskip}{\sigma} \rightsquigarrow \sigma
}

&
\inferrule[B-body]{
k, j \in [1..n]  \; k \neq j \Rightarrow l_k \neq l_j \\
\eval{G_{l_k}}{\sigma} \rightsquigarrow \sigma[l_k \mapsto v_k] \\
\sigma_1 = \sigma[l_1, .., l_n \mapsto v_1,.., v_n]
}{
\eval{G_{l_1} ..\; G_{l_n}}{\sigma} \rightsquigarrow \sigma_1
}\\
%
\end{array}
$$
}
\bigskip

We define a predicate $\mathrm{gSat}_{\sigma}(\vec{g_k})$ on a state $\sigma$
and a set of boolean expressions $\vec{g_k}$,  as the set of expressions in
$\vec{g_k}$ satisfied by the state $\sigma$. We abbreviate the group of guarded assigns
$\{g_1 \rightarrow l_1 = e_1 ~\KWor~g_2 \rightarrow l_2 = e_2  ..\}$ by
$\{\overrightarrow{g_k \rightarrow l_k = e_k} \}$.
In rule G-assign-T all guarded assignments must assign on the location $l$,
and there is exactly one guard which is satisfied by the current state.
In rule G-assign-F, no guard is satisfied, and the result binding
corresponds to the one in the initial state.
\begin{eqnarray*}
&
\inferrule[G-assign-T]{
\forall k. l_k=l \\
\mathrm{gSat}_{\sigma}(\vec{g_k}) = \{g_r \} \\
\SemFA{e_r}{\sigma} = v \\
}{
\eval{\KWassign ~l ~\{ \overrightarrow{g_k \rightarrow l_k = e_k} \}
}{\env} \rightsquigarrow \sigma[l \mapsto v]
}\\
\end{eqnarray*}
%
\begin{eqnarray*}
&
\inferrule[G-assign-F]{
\forall k. l_k=l \\
\mathrm{gSat}_{\sigma}(\vec{g_k}) = \emptyset \\
}{
\eval{\KWassign ~l ~\{ \overrightarrow{g_k \rightarrow l_k = e_k} \}
}{\env} \rightsquigarrow \sigma[l \mapsto \sigma(l)]
}\\
\end{eqnarray*}

The semantics of loops in \prog is given by the (partial) semantic function
${\cal S_P}:  {\cal P} \rightarrow (\Sstate \hookrightarrow \Sstate)$,
defined for each loop $p$ in \prog. Notice that in this semantics we do not
distinguish between diverging loops and loops where the semantics restrictions
on group assigns are violated.
$$
\SemF{{\cal S}_P}{p}{\sigma} = \left \{
\begin{array}{ll}
\sigma' & \mathrm{if ~} \eval{p}{\sigma} \rightsquigarrow \sigma'\\
\mathrm{undef}  & \mathrm{otherwise}\\
\end{array}
\right.
$$

\subsection{General definitions and properties on $sp$}
We rely on Hoare's partial correctness semantics to reason on invariants and recall
some fondamental definitions we use. In particular, we use the partial correctness
satisfaction relation $\vDash_{par}$ to define our invariants.
As we are interested in showing that our invariants for a given body loop pattern are
the strongest among all possible invariants, we exhibit in section \ref{sec:sp-semantics}
a strongest postcondition semantics for  loop bodies {B}.

\begin{definition} \emph{(Satisfaction under partial correctness $\vDash_{par}$ )}\\
We say that a Hoare triple $\{\phi\} P \{ \psi \}$ is \textit{satisfied under partial correcteness},
noted $\vDash_{par} \{\phi\} P \{ \psi \}$, \textbf{iff} for all states which satisfies $\phi$,
the state resulting from executing P satisfies $\psi$, provided that P actually terminates.
\end{definition}

We rely as well on the \textit{strongest postcondition semantics}
\cite{Gannod:1995:SPS:832303.836920} of  loop programs in \prog in order to show that
the invartiants we exhibit in  section \ref{sec:list-loop-patterns} are indeed the most
precise ones under the same initialization conditions for their corresponding loop patterns.
To this end, we use the \textit{strongest postcondition \spost{C}{P}  predicate transformer}
\cite{dijkstra(scholten:1990}, for a command $C$ and predicate $P$.
\spost{C}{P}  corresponds to the set of all states in which \textit{there exists}
a computation of $C$ that begins whith $P$ true. That is, given that $P$ holds, execution of $C$
results in \spost{C}{P} true, if $C$ terminates (that is, $sp$ assumes partial correctness).
In this section we introduce a general definition of $sp$
(i.e. independent on the structure of commands $C$) and some of its general properties.\\

\begin{definition} \emph{Predicate \spost{C}{P}}\\
For any command $C$ and predicate $P$ we define the predicate
\spost{C}{P} as being such that:
$$
\sigma' \vDash  \spost{C}{P}  \Leftrightarrow \exists
\sigma. (\eval{C}{\sigma} \rightsquigarrow \sigma' \land \sigma \vDash P)
$$
\end{definition}

\begin{corollary}[Properties on $sp(c,P)$] The following are useful properties of predicate \spost{C}{P}:
\begin{align*}
[\sppost]  &   \quad \vDash_{par} \{P\} ~C ~ \{ \spost{C}{P} \} & \textnormal{ ~is actually a postcondition} \\
[\spstrong] &  \quad \vDash_{par} \{P\} ~C~ \{ Q\} \Rightarrow (\spost{C}{P} \Rightarrow Q )  & \textnormal{ is the strongest one} \\
[\spmonoton] &   \quad  (P \Rightarrow Q) \Rightarrow (\spost{C}{P} \Rightarrow \spost{C}{Q} ) & \textnormal{ ~monotonicity}\\
\end{align*}
\end{corollary}

\begin{proof}
\subproof{
To verify that $[\sppost]$ holds let $\sigma'$ states, there exists $\sigma$ such that
$\{C,\sigma\} \rightsquigarrow \sigma'$ and $\sigma \vDash P$.
From the definition of $\spost{S}{P}$ we get that $\sigma' \vDash \spost{C}{P}$ as required.
}
\subproof{
To verify that $[\spstrong]$ holds let assume that $\sigma' \vDash \spost{C}{P}$ for any state $\sigma'$.
From the definition $\spost{C}{P}$ we get that
$\exists \sigma, \{C,\sigma\} \rightsquigarrow \sigma' \land \sigma \vDash P$.
If $\{C,\sigma\} \rightsquigarrow \sigma'$ then $\sigma' \vDash Q$ (because $\vDash_{par} \{ P \} C \{ Q \}$).
Therefore, for any state $\sigma'$ we get $(\sigma' \vDash \spost{C}{P}) \Rightarrow (\sigma' \vDash  Q)$
which holds $\spost{C}{P} \Rightarrow Q$
}
\subproof{
To verify that $[\spmonoton]$ holds let $\sigma'$ states, such that
$\sigma' \vDash \spost{C}{P}$. From the definition of $\spost{C}{P}$ we get that
$\exists \sigma, \{C,\sigma\} \rightsquigarrow \sigma' \quad \mathsf{(a)}$ and
$\sigma \vDash P \quad \mathsf{(b)}$.\\
As $(P \Rightarrow Q)$ we get that $\sigma \vDash Q \quad \mathsf{(c)}$.
Now with $(a)$ and $(c)$ we get that
$ \exists \sigma, \{C,\sigma\} \rightsquigarrow \sigma' \land \sigma \vDash Q$,
so clearly $\sigma' \vDash \spost{C}{Q}$ by the definition of $\spost{C}{Q}$.
Therefore, for any state $\sigma'$ we get $(\sigma' \vDash \spost{C}{P}) \Rightarrow (\sigma' \vDash \spost{C}{Q})$
which holds $\spost{C}{P} \Rightarrow \spost{C}{Q}$
}
\end{proof}

\ifdefined\longversion
\begin{corollary}[$sp$ on non changing variables] \label{cor:sp-indep}
  Let $C$ be a command that
  does not change on a variable $x$, that is, for any $\sigma, \sigma'$
  such that $\eval{C}{\sigma} \rightsquigarrow \sigma' $, then
  $\sigma(x) = \sigma'(x)$. Let  $k$ be some integer value. Then:
\begin{align*}
sp(C, x=k \land P) \Leftrightarrow x=k \land \spost{C}{P} & \quad \quad \textnormal{[Sp-indep]}
\end{align*}
\end{corollary}
\fi

\subsection{Strongest postcondition semantics}
\label{sec:sp-semantics}
\vspace{0.5 cm}
Following is the definition of stronguest loop invariant in our parallel loop semantic model.
We have two definitions (\sppar):
\begin{enumerate}
 \item the first definition concerns to the loop intermediate form
where the loop body (groups of guarded assignments) is empty;
 \item the second concerns to the general definition when we know
all the value of expression used in the groups of guarded assignments.
\end{enumerate}

\patternnote
In the general definition case when an expression is a unkown expression we quantified
this expression, this mean that the definition must be true for any kind of this unkown expression.
% If the expression $e$ is a degraded expression $e^?$, i.e an unknown value expression,
% then we degraded the strongest postcondition computation by eliminating the degraded
% expression in (SP-PAR) and the equality becomes degraded equality $\simeq$.

\begin{eqnarray*}
    && \spost{skip}{P} \symdef P
\end{eqnarray*}

\begin{eqnarray*}
    && \spost{\group{a}{g_{a1} .. g_{an}} || .. || \group{A}{g_{A1} .. g_{An}} || ..}{P} \symdef
   (\neg \gexit) \land (\exists \p{a}..\p{A}..)\\
    &&~~~\\
    &&\begin{array}{cc}
        \left(\begin{array}{cc}
                \p{P}\\
                \land\\
                \left(\begin{array}{cc}
                & \p{g_{a1}} \impl a = \p{e_{a1}} \\
                \land & ...\\
                \land & \p{g_{an_a}} \impl a = \p{e_{an_a}}\\
                \land & \neg \p{g_{a1}} ... \neg \p{g_{an_a}} \impl a = \p{a}\\
              \end{array}\right)\\
              \land\\
              ...\\
              ...\\
              \land\\
              \left(\begin{array}{cc}
                & \p{g_{A1}} \impl A[\p{\upsilon_{A1}}] = \p{e_{A1}} \\
                \land & ...\\
                \land & \p{g_{An_a}} \impl A[\p{\upsilon_{An_a}}] = \p{e_{An_a}}\\
                &~~~~~~~~~~~~~~~~\\
                \land & (\forall j)
              \left(\begin{array}{cc}
                &\inbounds{A}{j} \\
                \land & \neg (\p{g_{A1}} \land j =  \p{\upsilon_{A1}})\\
                ...\\
                \land & \neg (\p{g_{An_a}} \land j =  \p{\upsilon_{An_a}})\\
                \end{array}\right) \impl A[j] = \p{A}[j]
              \end{array}\right)\\
              \land\\
              ...\\
              ...\\
        \end{array}\right)
    \end{array}
\end{eqnarray*}

\vspace{0.5cm}
In the second terms of the righ-hand side of the formulation any expression \p{e}
represents the expression $e$ where all the occurence of variables modified (a, .., A, ..)
occurring in $e$ are replaced by the existential variable \p{a}, .., \p{B}, ...
Indeed, by notation $\p{e} = \subst{e}{a..A..}{\p{a}..\p{B}..}$

If the expression $e$ is a value-preserving expression, by definition $e=e_0$,
and we recall that $e_0$ denotes the expression $e$ where all variables have been
replaced by their initial values then $\p{e_0} = e_0$.

\vspace{0.5cm}
Notice that the rule $SP$ for sequential composition of statements is the
usual rule associated with a sequential execution semantics for statements.
As our semantics guarded assignments are parallel, we should start with proving
that rule \sppar indeed computes the desired strongest postcondition.

\begin{lemma}
\label{lem:sp-correctness}
  \emph{(\spostsym Correctness over \loopform)} Operator \spostsym as defined in \sppar,
  computes the strongest postcondition over parallel group assignments in our loop model.
\end{lemma}

\begin{proof}
 TODO
\end{proof}


%==================================================================================
%==================================================================================
\section{Invariants and body loop patterns}

%==================================================================================
\subsection{Loop Predicates Conventions}
Given the loop program $L$ we define the following predicates
\begin{enumerate}
\item \initcond{L} : describes the vacuously fact that any location $l$
(excepting the loop index \idx) occurring in  a loop has $l_0$ as initial value at loop entry.
\item \framecond{L} : describes the variables which are never assigned in the loop.
\item \preservecond{L}{\idx} : describes an inductive invariant such that we have the following relations
\end{enumerate}

$$\initcond{L} \Rightarrow (\preservecond{L}{\idxinitial} \Rightarrow \framecond{L})$$
$$(\forall \idx) (\idxinitial \leq \idx \leq \idxfinal \land \preservecond{L}{\idx} \Rightarrow \framecond{L})$$
%==================================================================================
\subsection{Value-preserving Expressions}

We define \textit{value-preserving expressions} as those expressions
such that there is an inductive invariant \preservecond{L}{\idx} such that:
$$\preservecond{L}{\idx} \Rightarrow (e = e_0)$$
%
Consequently the \textit{value-preserving expressions} as those expression
whose value at the program point before group assignments is such that ($e=e_0$)
is a loop invariant. Let us call the corresponding property \textit{value-preserving property}:
\begin{equation}
 e=e_0 \tag{\vpp}
\end{equation}
%
Given a loop index \idx, we denote a \textit{value-preserving expression} $e$
as $e^\at{\idx}$, so that we can express the same expression for differents
values of the loop index (\eg $e^\at{j}$, $e^\at{k}$, \etc). Such an expression
only depends on the number of iterations and initial values of variables
before the loop. Notice that ($e^\at{j} = e_0^\at{j}$) is not necessarily a
loop invariant for $j \neq i$.  For instance in the following example:
$$\begin{array}{l}
  \KWloop \KWover i \KWin 1 .. N \\
  ~~~~ \mathit{true} \rightarrow A[i] := 0\\
  \KWend
\end{array}$$
$e^\at{\idx} \symdef A[\idx]$ (with current index \idx) is a
value-preserving expression, because ($A[\idx]=A_0[\idx]$) is a loop
invariant. But ($A[0]=A_0[0]$) is not a loop invariant.
%
Sufficient conditions for an expression $e$ to be a value-preserving expression
are the following:
\begin{enumerate}
\item $e$ does not refer to scalar variables that are assigned in the loop;
\item $e$ may refer to an array variable $A$ that is modified in the loop,
  provided it does so at index \idx or indexes that are known to be greater
  than \idx (\eg $\idx + 1$), and all assignments to $A$ are at index \idx or
  indexes that are known to be less than \idx (\eg $\idx - 1$). This ordering
  can be more complex, and necessitate a special analysis, like in the case of
  array filtering where the array is assigned at index $v$ where $v$ is
  incremented less often than the loop index; in this case
$$\preservecond{L}{\idx} = \framecond{L} \land (\forall j)(\idx \leq j \leq \idxfinal \Rightarrow A[j]=A_0[j])$$
\end{enumerate}
\patternnote
Consequently, $e$ may refer to (array or scalar) variables that are not modified in the loop.

%==================================================================================
\subsection{Invariant definitions}

\begin{definition} \emph {(Inductive loop invariant under initialization conditions)}\\
A formula $\Phi$ is an \textit{inductive invariant under initialization conditions} \initcond{L} for the loop
\hspace{1cm} $L = \KWloop  \idx \KWin \idxinitial ..\idxfinal ~ \KWexit \gexit \KWdo B ~\KWend$ \\
\textbf{iff}:
\begin{itemize}
\item $(\idx=\idxinitial \land \initcond{L}) \Rightarrow \phi$.
      That is, $\phi$ holds after executing the initialization;
\item $\vDash_{par} \{\idxinitial \leq \idx \leq \idxfinal \wedge \neg \gexit \wedge\phi \} \texttt{ B; i=i+1 } \{ \phi \}$ holds.
      That is, $\phi$ remains true after each execution of $B$ followed by and index increment,
      provided that $b^{ex}$ does not hold.
\end{itemize}
\end{definition}

The intuition behind this invariant definition lays on the following translation.
The loop $\KWloop  \idx \KWin \idxinitial ..\idxfinal ~ \KWexit \gexit ~ \KWdo B ~\KWend$
can be translated into a sequence of commands: the initialization of the loop index,
followed by a classical while loop iterating as long as the index remains within bounds
and that the exit condition does not hold:
{\small
\begin{lstlisting}[mathescape]
   $i=\idxinitial$; while ($i \leq \idxfinal \wedge \neg \gexit$) $\KWdo$ B; i=i+1 $~\KWend$
\end{lstlisting}
}
Thus, to show that $\Phi$ is an invariant, it suffices to show that it holds after
the initialization, and then, that $\Phi$ is indeed an invariant of the while loop above,
which corresponds to the second condition of definition.
We are interested in establishing  the most precise loop invariant \inv for a given loop pattern in \prog.

\begin{definition} \emph {(Most precise invariant under initialization conditions)}\\
A formula $\phi$ is the \textit{most precise invariant under initialization conditions},
or shortly, \textit{under conditions} \initcond{L} for a loop $L$, noted $\phi = M_I(L, \initcond{L})$,
if $\phi$ is an invariant under \initcond{L} for $L$, and if, for any other invariant $\psi$ of $L$
under the same conditions, then $\phi \Rightarrow \psi$.
\end{definition}

%==================================================================================
\subsection{Body loop patterns}

We are interested in identifying  loop patterns that comeout  fequently.
Actually, we define our loop patterns as particular body patterns,
for which we exhibit the most precise invariant in a sens precised later.

\begin{definition} \emph{(Body pattern)}\\
A \textit{loop body pattern} or \textit{pattern} $B_P \in \SB$ is a collection of group-assigns.
Let $L$ be a loop with loop body $B_L = G_{l_1}, \ldots G_{l_m}$.
A statement $B_P \in \SB$ is a \textit{body pattern} for loop $L$, or shortly,
a pattern for loop $L$, if all group assigns in $B_P$ occur in $B_L$.
\end{definition}

\begin{definition} \emph{(Loop reduced to a pattern $B_p$)}\\
Let $B_P$ be a loop body pattern. We define the \textit{loop reduced to the pattern} $B_P$,
as the loop  iterating \idx from $\idxinitial$ throug $\idxfinal$ and executing a body equals to $B_P$.
We note it by $L_R(B_P, i, \idxinitial,\idxfinal)$ or shortly by $L_R(B_P)$. (What about exit condition?)
\end{definition}


\begin{definition} 4 \emph {(Pattern capture)}\\
A formula $\phi$ captures a body pattern $B_P$, under conditions $H$,
noted $\mathrm{Capture}^H(\phi, B_p)$ \textbf{iff}
\begin{itemize}
\item[i.]  $\phi = M_I(L_R(B_P),H)$: meaning that $\phi$ is the most precise invariant
           under conditions $H$ of the loop reduced to $B_P$, $L_R(B_P)$,
\item[ii.] $\phi$ is an inductive invariant under conditions $H$ of any well-formed loop $L^*$
           including $B_P$ in its body.
\end{itemize}
\end{definition}

%==================================================================================
\subsection{Stating invariant maximality and pattern capture}

The following theorem states sufficient conditions on an invariant for
a loop in $L$ to be the most precise invariant under a particular
initialization hypothesis.

\begin{theorem}[Sufficient conditions for invariant maximality]
\label{lem:precise-inv}
Let $L$ be the loop \textnormal{$\KWloop  \idx \KWin \idxinitial ..\idxfinal ~
\KWexit g_{exit}~ \KWdo B ~\KWend$} with $B$ a body loop not writing the index \idx.
Let $\psi$ be an inductive invariant for $L$ under \initcond{L}.
And let $\phi$ be such that :
\begin{itemize}
\item[(a)] $\initcond{L} \Rightarrow \phi(\idxinitial)$
\item[(b)] $\spost{B}{\initcond{L} \land \neg g_{exit} \land \phi(\idxinitial)}
             \Leftrightarrow
            \framecond{L} \land \preservecond{L}{\idxinitial+1} \land  \phi(\idxinitial+1)$
\item[(c)] $\spost{B}{\idxinitial < \idx \leq \idxfinal \land  \framecond{L} \land \preservecond{L}{\idx} \land \neg g_{exit} \land \phi(\idx)}
             \Leftrightarrow \\
            \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx+1} \land \phi(\idx+1)$
\end{itemize}
\noindent Then, $\phi$ is the most precise inductive invariant for $L$ under \initcond{L},
that is:
\begin{align*}
(\idx = \idxinitial \land \initcond{L} \land \phi(\idx)) \Rightarrow  \psi(\idx)\\
(\forall \idx) ((\idxinitial < \idx \leq \idxfinal+1 \land \framecond{L} \land \preservecond{L}{\idx} \land \phi(i))
\Rightarrow \psi(i))  & \quad \quad [\maxinv]
\end{align*}
\end{theorem}

\begin{proof}
  \subproof{\textbf{Init case}}
  By definition, as $\psi$ is an inductive invariant under \initcond{L}, the following holds:
  $$(\idx= \idxinitial \land \initcond{L}) \Rightarrow \psi(\idx)$$
  Obviously we have thus :
  $$(\idx= \idxinitial \land \initcond{L} \land \phi(\idx)) \Rightarrow  \psi(\idx)$$

  \subproof{\textbf{Preservation case}}
  Here the proof proceeds by induction on the loop index \idx.\\
\\
  First, as $\psi$ is an inductive invariant, the Hoare triple below holds.
  $$
    \{\idxinitial \leq \idx \leq \idxfinal \land \neg g_{exit} \land \psi(\idx) \}
    \texttt{B;\idx:=i+1}
    \{\psi(\idx) \}
  $$
  %
  By the hypothesis that the body loop $B$ does not writing the index \idx, we get the following Hoare triple
  $$
    \{\idxinitial \leq i \leq \idxfinal \land \neg g_{exit} \land \psi(i) \}
    \texttt{B}
    \{\psi(i+1) \}
  $$
  %
  By \spstrong we get that
  \begin{align*}
    \spost{\texttt{B}}{\idxinitial \leq i \leq \idxfinal \land \neg g_{exit} \land \psi(i) }
    \Rightarrow \psi(i+1) \quad \quad \mathsf{(1)}
  \end{align*}

  \subsubproof{\textbf{Base case}}
  $$\initcond{L} \land \idx= \idxinitial \land \phi(\idx) \Rightarrow  \psi(\idx)$$
  %
  By adding $g_{exit}$ to both side of the formula we get that
  \begin{align*}
    \initcond{L} \land \neg g_{exit} \land \phi(\idxinitial)
    \Rightarrow
    \neg g_{exit} \land \idx= \idxinitial \land \psi(\idx)
  \end{align*}
  %
  By applying \spmonoton we get that
  \begin{align*}
    \spost{\texttt{B}}{ \initcond{L} \land \neg g_{exit} \land \phi(\idxinitial)}
    \Rightarrow
    \spost{\texttt{B}}{\neg g_{exit} \land \idx= \idxinitial \land \psi(\idx)}
  \end{align*}
  %
  By theorem hypothesis $(b)$ we have
  \begin{align*}
    \spost{\texttt{B}}{\initcond{L} \land \neg g_{exit} \land \phi(\idxinitial)}
    \Leftrightarrow
    \framecond{L} \land \preservecond{L}{\idxinitial+1} \land \phi(\idxinitial+1)
  \end{align*}
  %
  So
  \begin{align*}
     \framecond{L} \land \preservecond{L}{\idxinitial+1} \land  \phi(\idxinitial+1)
    \Rightarrow
    \spost{\texttt{B}}{\neg g_{exit} \land \idx= \idxinitial \land \psi(\idx)} \quad \quad \mathsf{(2)}
  \end{align*}
  %
  For $\idx = \idxinitial \land \idxfinal \geq \idxinitial$ (notice that the case $\idxfinal < \idxinitial$ is vacuosly true) we get that
  $$\neg g_{exit} \land \idx= \idxinitial \land \psi(\idx) \Rightarrow \idxinitial \leq i \leq \idxfinal \land \neg g_{exit} \land \psi(i)$$
  By applying \spmonoton we get that
  \begin{align*}
    \spost{\texttt{B}}{\neg g_{exit} \land \idx= \idxinitial \land \psi(\idx)}
    \Rightarrow
    \spost{\texttt{B}}{\idxinitial \leq i \leq \idxfinal \land \neg g_{exit} \land \psi(i)}
  \end{align*}
  and by $\mathsf{(1)}$ and by transition we get that
  \begin{align*}
    \spost{\texttt{B}}{\neg g_{exit} \land \idx= \idxinitial \land \psi(\idx)}
    \Rightarrow
    \psi(\idxinitial+1) \quad \quad \mathsf{(3)}
  \end{align*}
  With $\mathsf{(3)}$ and $\mathsf{(2)}$ for $\idx = \idxinitial \land \idxfinal \geq \idxinitial$

  \begin{align*}
    \framecond{L} \land \preservecond{L}{\idxinitial+1} \land  \phi(\idxinitial+1)
    \Rightarrow \psi(\idxinitial+1)
  \end{align*}

  \subsubproof{\textbf{Inductive step}}
  Following is the inductive hypothesis
  $$
  \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx} \land \phi(\idx)
  \Rightarrow
  \psi(i)
  $$
  %
  which can be rewritten
  $$
  \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx} \land \phi(\idx)
  \Rightarrow
  \idxinitial < \idx \leq \idxfinal \land \psi(i)
  $$
  %
  By adding $g_{exit}$ to both side of the formula we get that
  \begin{align*}
  \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx} \land \neg g_{exit} \land \phi(i)
  \Rightarrow \\
  \idxinitial < \idx \leq \idxfinal \land \neg g_{exit} \land \psi(i)
  \end{align*}
  %
  By applying \spmonoton, we get that
  \begin{align*}
    \spost{\texttt{B}}{\idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx} \land \neg g_{exit} \land \phi(i)}
    \Rightarrow\\
    \spost{\texttt{B}}{\idxinitial < \idx \leq \idxfinal \land \neg g_{exit} \land \psi(\idx)}
  \end{align*}
  %
  By the theorem hypothesis $(c)$ we get the following
  \begin{align*}
    \spost{B}{\idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx} \land \neg g_{exit} \land \phi(\idx)}
             \Leftrightarrow  \\
    \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx+1} \land \phi(\idx+1)
  \end{align*}
  %
  So
  \begin{align*}
   \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx+1} \land \phi(\idx+1)
   \Rightarrow\\
   \spost{\texttt{B}}{\idxinitial < \idx \leq \idxfinal \land \neg g_{exit} \land \psi(\idx)} \quad \mathsf{(4)}
  \end{align*}
  %
  By $\mathsf{(4)}$ and $\mathsf{(1)}$ we get that
  \begin{align*}
    \idxinitial < \idx \leq \idxfinal \land \framecond{L} \land \preservecond{L}{\idx+1} \land \phi(\idx+1)
    \Rightarrow \psi(\idx+1)
  \end{align*}
  Finally
  $$(\forall \idx) ((\idxinitial < \idx \leq \idxfinal+1 \land \framecond{L} \land \preservecond{L}{\idx} \land \phi(i))
  \Rightarrow \psi(i))$$
\end{proof}


According to the previous theorem \ref{lem:precise-inv} prove that an invariant $\phi$
is a most precise invariant of the loop $L$ consists first to prove that $\phi$ preserves
a loop initialization and second to compute the stronguest postcondition over the loop body
$B_L = G_{l_1}, \ldots G_{l_m}$ at each iteration under the guard \gexit to exit the loop.

\vspace{0.5 cm}
Following is the definition of stronguest loop invariant in our parallel loop semantic model.
We have two definitions (\sppar):
\begin{enumerate}
 \item the first definition concerns to the loop intermediate form
where the loop body (groups of guarded assignments) is empty;
 \item the second concerns to the general definition when we know
all the value of expression used in the groups of guarded assignments.
\end{enumerate}

\patternnote

\begin{lemma}
\label{lem:pattern-captures}
  \emph{(Pattern Captures)} Prove that a formula $\phi(i)$, given by an invariant \inv
  in  our \loopform, captures the pattern \pat becomes to prouve that $\phi(i)$ is the
  most precise invariant to loop reduced to pattern \pat.
\end{lemma}

\begin{proof}
 TODO
\end{proof}


%==================================================================================
%==================================================================================
\section{Identified loop patterns}
\label{sec:list-loop-patterns}

\newcommand{\pattern}[3]{%
\refstepcounter{pc}
\patterndef #1
%
\begin{equation}
  \begin{array}{cccc} #2 \end{array} \tag{\curpattern}
\end{equation}
%
\loopinvariant
%
\begin{equation}
  \Inv{\idx} \symdef \begin{array}{cccc} #3 \end{array} \tag{\curinv}
\end{equation}
}

%==================================================================================
%==================================================================================
\subsection{Search Pattern}

\pattern{
  The group assignments is empty and the control boolean expression \gexit to exit the
  loop is a value-preserving expression.
}{
  \gexit = g^\at{\idx}
}{
  (\forall j)\left(\begin{array}{cc}
                  \seen{j}{\idx} \impl \neg g_0^\at{\idx}
             \end{array}\right)
}

\patternnote Notice that this particular pattern allows to control the execution of loop body.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N~ \KWexit A[\idx] = 0~ \KWdo:\\
    &&~~~\textit{invariant}:(\forall j)\left(\begin{array}{cc}
                                      (1\leq j < i) \impl A[j] \neq 0
                            \end{array}\right)\\
    &&~~~\varepsilon \\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\label{theo:capture-search-pattern}
\end{theorem}

\begin{proof}
  \subproof{Proof of loop invariant initalization}
  When $\idx = \idxinitial$, $\nexists j$ such that $\idxinitial \leq j < \idx$, i.e $\seen{j}{\idx}=\mathit{false}$\\
  then $$\Inv{\idx} = (\forall j) (\seen{j}{\idx} \impl \neg g_0^\at{\idx}) = \mathit{true}$$
  therefore
  $$(\idx = \idxinitial) \Leftrightarrow (\Inv{\idx} \land (\idx = \idxinitial))$$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  The proof proceeds by induction on the number of iterations \idx.

  \subsubproof{Base case}
  By \vpp we have $\gexit = g^\at{\idxinitial} = g_0^\at{\idxinitial}$, therefore:
  \begin{eqnarray*}
    \spost{\KWskip}{\idx \leq \idxfinal \land \neg g_0^\at{\idxinitial}}
    &=& \idx \leq \idxfinal \land \neg g_0^\at{\idxinitial}\\
    &\Leftrightarrow& (\forall j) (\idxinitial \leq j < \idxinitial+1 \impl \neg g_0^\at{j})\\
    &\Leftrightarrow& (\forall j) (\seen{j}{\idxinitial+1} \impl \neg g_0^\at{j})\\
    &\Leftrightarrow& \Inv{\idxinitial+1}
  \end{eqnarray*}

  \subsubproof{Inductive step}
  Now assume \Inv{\idx} at loop iteration \idx, and let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx} through
  the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variable,
  only initial values of variables and current value of the loop index.
  \begin{eqnarray*}
    &\spost{\KWskip}{\neg \gexit \land \Inv{\idx}}&\\
    &=&\\
    &\spost{\KWskip}{\neg g_0^\at{\idx} \land \Inv{\idx}}&\\
    &=&\\
    &\neg g_0^\at{\idx} \land \Inv{\idx}&\\
  \end{eqnarray*}
  %
  Unfolding \Inv{\idx}
  \begin{eqnarray*}
    &\neg g_0^\at{\idx} \land (\forall j)(\seen{j}{\idx} \impl \neg g_{0}^\at{j})&\\
    &\Leftrightarrow&\\
    &(\forall j)(\seen{j}{\idx+1} \impl \neg g_{0}^\at{j})&\\
    &\Leftrightarrow&\\
    &\Inv{\idx+1}
  \end{eqnarray*}

  This proves that \Inv{\idx} is the strongest loop invariant on the
  loop reduced to the pattern.
  By deduction through the lemme \ref{lem:pattern-captures}, \Inv{\idx}
  remains a loop invariant of any loop where \curpattern occurs. Therefore,
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{proof}

%==================================================================================
%==================================================================================
\subsection{Update Patterns}

\subsubsection*{Certain Single Update Pattern}

\pattern{
  A scalar variable $a$ is modified in exactly a single assignment, whose
  guard is \textit{true}, and it receives a value-preserving expression.
}{
  \mathit{true} \rightarrow a := e^\at{\idx}
}{
  (\idx = \idxinitial \impl a = a_0) \land (\idx \neq \idxinitial \impl a = e_0^\at{\idx - 1})
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\idx = 1 \impl a = \mathit{false}) \land (\idx \neq 1 \impl a = \mathit{true})\\
         \end{array}\right)\\
    &&~~~true \rightarrow a := true\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
  The proof proceeds by induction on the number of iterations \idx.

  \subproof{Proof of loop invariant initalization:}
  In a loop reduced only to this pattern, no variable is modified, excepted
  $a$ and current value of the loop index, $\initcond{L} \equiv (a = a_0)$.
  $$(i = \idxinitial \land a = a_0) \impl \Inv{\idx}$$
  and since $\idx$ is exactly equal to $\idxinitial$ then
  $$\initcond{L} \land \idx = \idxinitial) \Leftrightarrow (\Inv{\idx} \land \idx = \idxinitial)$$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.
  \begin{eqnarray*}
    &\spost{\mathit{true} \rightarrow a := e^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &\spost{\mathit{true} \rightarrow a := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=& \\
    &(\exists a') (a = e_0^\at{\idx} \land \Inv{\idx}[a\leftarrow a'])&\\
    &\Leftrightarrow&\\
    &(a = e_0^\at{\idx}) \land (\exists a') (\Inv{\idx}[a\leftarrow a'])&\\
    &\Leftrightarrow&\\
    &(a = e_0^\at{\idx}) \land \mathit{true}&\\
    &\Leftrightarrow&\\
    &\Inv{\idx+1}&
  \end{eqnarray*}

  This proves that \Inv{\idx} is the strongest loop invariant on the
  loop reduced to the current pattern \curpattern.
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Known Single Update Pattern}

\pattern{
  A scalar variable is only modified in a single assignment, whose guard is
  a value-preserving expression, and it receives a value-preserving expression.
}{
  g^\at{\idx} \rightarrow a := e^\at{\idx}
}{
  &(a = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})\\
  &\lor \\
  &(\exists j)
  \left(\begin{array}{ll}
    &\seen{j}{\idx} \land g_0^\at{j} \land a = e_0^\at{j} \\
    \land &(\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k}))
  \end{array}\right)
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1\leq j < i \impl A(j)-B(j)\neq0)\\
           &\lor\\
           &(\exists j)(1\leq j < i \land A(j)-B(j)= 0 \land m = B(j) \land \\
           &(\forall k)(j < k < i \impl A(k)-B(k)\neq0))\\
         \end{array}\right)\\
    &&~~~A(i)-B(i)=0 \rightarrow m := B(i)\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
  The proof proceeds by induction on the number of iterations \idx.

  \subproof{Proof of loop invariant initalization:}
  In a loop reduced only to this pattern, no variable is modified, excepted
  $a$ and current value of the loop index, $\initcond{L} \equiv (a = a_0)$.
  $$(\idx = \idxinitial \land a = a_0) \impl \Inv{\idx}$$
  When $\idx = \idxinitial$, $\nexists j$ such that $\idxinitial \leq j < \idx$ i.e $(\seen{j}{\idx})=\mathit{false}$\\
  So
  $$(\Inv{\idx} \land \idx = \idxinitial)\equiv (a = a_0)$$
  Therefore
  $$(\initcond{L} \land \idx = \idxinitial) \Leftrightarrow (\Inv{\idx} \land \idx = \idxinitial)$$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.
  \begin{eqnarray*}
    &\spost{g^\at{\idx} \rightarrow a := e^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &\spost{g_0^\at{\idx} \rightarrow a := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &(\exists a')\left(\begin{array}{ll}
                       & \Inv{\idx}[a\leftarrow a'] \\
                       \land & g_0^\at{\idx}[a\leftarrow a'] \impl a = e_0^\at{\idx}\\
                       \land & \neg g_0^\at{\idx}[a\leftarrow a'] \impl a = a'
                   \end{array}\right)&\\
  \end{eqnarray*}
  %
  Since $g_0^\at{\idx}$ and $\neg g_0^\at{\idx}$ are a partition
  we can write the formula in disjunctive normal form (DNF) :
  \begin{eqnarray*}
   &(\exists a')\left(\begin{array}{cc}
                      & \Inv{\idx}[a\leftarrow a'] \\
                      &\land\\
                      & (g_0^\at{\idx} \land a = e_0^\at{\idx})
                        \lor  (\neg g_0^\at{\idx} \land a = a')
                \end{array}\right)&\\
  \end{eqnarray*}
  %
  By developping we have the following equivalence
  \begin{eqnarray*}
   &(\exists a') \left(\begin{array}{cc}
          &(\Inv{\idx}[a\leftarrow a'] \land g_0^\at{\idx} \land a = e_0^\at{\idx})\\
          &\lor\\
          &(\Inv{\idx}[a\leftarrow a'] \land \neg g_0^\at{\idx} \land a = a')\\
    \end{array}\right)&\\
  \end{eqnarray*}

  Let :
  \begin{eqnarray*}
    &&A=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land g_0^\at{\idx} \land a = e_0^\at{\idx})\\
    &&B=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land \neg g_0^\at{\idx} \land a = a')\\
  \end{eqnarray*}
  %
  - Simplify $A$
  \begin{eqnarray*}
    A &\Leftrightarrow& (\exists a')(\Inv{\idx}[a\leftarrow a']) \land g_0^\at{\idx} \land a = e_0^\at{\idx}\\
    A &\Leftrightarrow& g_0^\at{\idx} \land (a = e_0^\at{\idx})\\
  \end{eqnarray*}
  %
  - Simplify $B$ by Unfolding of $\Inv{\idx}[a\leftarrow a']$ :
  \begin{eqnarray*}
    &(\exists a')(\Inv{\idx}[a\leftarrow a'] \land \neg g_0^\at{\idx} \land a = a')&\\
    &\Leftrightarrow&\\
    &(\exists a')
      \left(\begin{array}{cc}
      \begin{array}{cc}
         &\left(\begin{array}{cc}
                 (a' = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})\\
                 \lor\\
                 (\exists j)(\seen{j}{\idx} \land g_0^\at{j} \land a' = e_0^\at{j} \land \\
                 ~~~~~~~~(\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k}))\\
               \end{array}\right)\\
         &\land\\
         &(\neg g^\at{\idx} \land a = a')
     \end{array}
     \end{array}\right)&\\
    &\Leftrightarrow& \\
    &(B_1 \lor B_2)&
  \end{eqnarray*}
  %
  With :
  \begin{eqnarray*}
    B_1 &=& (\exists a')
         \left(\begin{array}{cc}
            &(a' = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})\\
            &\land\\
            &(\neg g^\at{\idx} \land a = a')\\
          \end{array}\right)\\
    B_2 &=& (\exists a')
         \left(\begin{array}{cc}
               &(\exists j)(\seen{j}{\idx} \land g_0^\at{j} \land a' = e_0^\at{j}) \\
               &\land (\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k}))\\
               \land &(\neg g^\at{\idx} \land a = a')\\
           \end{array}\right)\\
  \end{eqnarray*}
  %
  - Simplify $B_1$ by eliminating existential
  \begin{eqnarray*}
    B_1 &\Leftrightarrow& (a = a_0) \land (\forall j)(\seen{j}{\idx+1} \impl \neg g_0^\at{j})\\
  \end{eqnarray*}
  %
  - Simplify $B_2$
  \begin{eqnarray*}
    B_2 &=& (\exists a')
         \left(\begin{array}{cc}
               &(\exists j)(\seen{j}{\idx} \land g_0^\at{j} \land a' = e_0^\at{j}) \\
               &\land (\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k}))\\
               \land &(\neg g^\at{\idx} \land a = a')\\
           \end{array}\right)\\
  \end{eqnarray*}
  %
  $a' = a$ for the last $j = i$, where $a$ is modified. Then $B_2$ is equivalent to:
  \begin{eqnarray*}
    B_2 &\Leftrightarrow&
         \left(\begin{array}{cc}
              &(\exists j)(\seen{j}{\idx} \land g_0^\at{j} \land a = e_0^\at{j} \\
              &\land (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k}))\\
         \end{array}\right)\\
  \end{eqnarray*}
  %
  - Computation of $B_2 \lor A$
  \begin{eqnarray*}
    B_2 \lor A &\Leftrightarrow&
                \left(\begin{array}{cc}
                     &(\exists j)(\seen{j}{\idx} \land g_0^\at{j} \land a = e_0^\at{j} \\
                     &\land (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k}))\\
                     &\lor\\
                     &g_0^\at{\idx} \land (a = e_0^\at{\idx})\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  By developping we have :
  \begin{eqnarray*}
    B_2 \lor A &\Leftrightarrow&
                \left(\begin{array}{cc}
                     &(\exists j)(\seen{j}{\idx+1} \land g_0^\at{j} \land a = e_0^\at{j} \\
                     &\land (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k}))\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  - Computation of $B_1 \lor B_2 \lor A$
  \begin{eqnarray*}
    B_1 \lor B_2 \lor A &\Leftrightarrow&
               \left(\begin{array}{cc}
                    &(a = a_0) \land (\forall j)(\seen{j}{\idx+1} \impl \neg g_0^\at{j})\\
                    &\lor\\
                    &(\exists j)(\seen{j}{\idx+1} \land g_0^\at{j} \land a = e_0^\at{j} \\
                    &~~~~~~~~\land (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k}))\\
               \end{array}\right) \\
    &\Leftrightarrow& \Inv{\idx+1}
  \end{eqnarray*}

  This proves that \Inv{\idx} is the strongest loop invariant on the
  loop reduced to the current pattern \curpattern.
\end{proof}

%==================================================================================
%==================================================================================

\subsubsection*{Known Multiple Update Pattern}

\pattern{
  A scalar variable is modified in more than one assignment, all of
  whose guards are value-preserved, and it receives in each a value-preserving expression.
}{
  &g_1^\at{\idx} \rightarrow a := e_1^\at{\idx}\\
  &...\\
  &g_n^\at{\idx} \rightarrow a := e_n^\at{\idx}\\
}{
  &(a = a_0) \land (\forall j)(\forall r)(\seen{j}{\idx} \impl \neg g_{r0}^\at{j})\\
  \lor
  & (\exists j)
   \left(\begin{array}{cl}
  &(\exists r)(\seen{j}{\idx} \land g_{r0}^\at{j} \land a = e_{r0}^\at{j})\\
   \land&  (\forall k)(\forall r) (\betweens{j}{k}{\idx} \impl \neg g_{r0}^\at{k})
   \end{array}\right)
}

\patternnote The existential and universal quantifiers on $r$
concern the implicit range $1 \leq r \leq n$.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1 \leq j < i \impl A(j)-B(j)=0)\\
           &\lor\\
           &(\exists j)(1 \leq j < i \land ((A(j)-B(j) < 0 \land m = B(j))\\
           &~~~~~~~~~~~~~~~~~~~~~~~~  \lor (A(j)-B(j) > 0 \land m = A(j))) \\
           &(\forall k)(j < k < i \impl A(k)-B(k) = 0))\\
         \end{array}\right)\\
    &&~~~A(i)-B(i) < 0 \rightarrow m := B(i)\\
    &&~~~A(i)-B(i) > 0 \rightarrow m := A(i)\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
  This is the generation of the proof of previous theorem with the following restrictions:
  for $n$ assignments to scalar variable $a$, whose guards are $g_1$, .., $g_n$
  then only one of the guards $g_r$ can be satisfied, the others is unsatisfiable.
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Single Update Pattern}

\pattern{
  A scalar variable $a$ is modified at most in a single assignment, whose
  guard is unknown, and it receives a value-preserving expression.
}{
  g^? \rightarrow a := e^\at{\idx}
}{
  (a = a_0) \lor (\exists j)(\seen{j}{\idx} \land a = e_0^\at{j})\\
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \lor (\exists j)(1\leq j < i \land m = B_0(j))\\
         \end{array}\right)\\
    &&~~~A(m)-B(m)=0 \rightarrow m := B(i)\\
    &&\KWend
  \end{eqnarray*}


\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
  The proof proceeds by induction on the number of iterations \idx.\\

  \subproof{Proof of loop invariant initalization:}
  In a loop reduced only to this pattern, no variable is modified, excepted
  $a$ and current value of the loop index, $\initcond{L} \equiv (a = a_0)$.
  $$(i = \idxinitial \land a = a_0) \impl \Inv{\idx}$$
  and
  $$(\Inv{\idx} \land \idx = \idxinitial) \Leftrightarrow (i = \idxinitial \land a = a_0)$$
  because $i = \idxinitial$, $\nexists j$ such that $\idxinitial \leq j <i$, i.e $(\seen{j}{\idx})=\mathit{false}$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.\\
  Let $\varrho$, such that $\varrho=g^?$
  \begin{eqnarray*}
    &\spost{g^? \rightarrow a := e^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &\spost{\varrho \rightarrow a := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &(\exists a')\left(\begin{array}{ll}
                       & \Inv{\idx}[a\leftarrow a'] \\
                       \land & \varrho[a\leftarrow a'] \impl a = e_0^\at{\idx}\\
                       \land & \neg \varrho[a\leftarrow a'] \impl a = a'
                   \end{array}\right)&\\
  \end{eqnarray*}
  %
  Since $\varrho[a\leftarrow a']$ and $\neg \varrho[a\leftarrow a']$ are a partition
  we can write the formula in disjunctive normal form (DNF) :
  \begin{eqnarray*}
   &(\exists a')\left(\begin{array}{cc}
                      & \Inv{\idx}[a\leftarrow a'] \\
                      &\land\\
                      & (\varrho[a\leftarrow a'] \land a = e_0^\at{\idx})
                        \lor  (\neg \varrho[a\leftarrow a'] \land a = a')
                \end{array}\right)&\\
  \end{eqnarray*}
  %
  As we don't know the value of $\varrho[a\leftarrow a']$ the above formula
  is equivalent (degraded notion?) to
  By developping we have the following equivalence
  \begin{eqnarray*}
   &\left(\begin{array}{cc}
          &(\exists a')(\Inv{\idx}[a\leftarrow a'] \land a = e_0^\at{\idx})\\
          &\lor\\
          &(\exists a')(\Inv{\idx}[a\leftarrow a']  \land a = a')\\
    \end{array}\right)&\\
  \end{eqnarray*}

  Let :
  \begin{eqnarray*}
    &&A=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land a = e_0^\at{\idx})\\
    &&B=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land a = a')\\
  \end{eqnarray*}
  %
  - Simplify $A$
  \begin{eqnarray*}
    A &\Leftrightarrow& (\exists a')(\Inv{\idx}[a\leftarrow a']) \land a = e_0^\at{\idx}\\
    A &\Leftrightarrow& (a = e_0^\at{\idx})\\
  \end{eqnarray*}
  %
  - Simplify $B$ by Unfolding of $\Inv{\idx}[a\leftarrow a']$ :
  \begin{eqnarray*}
    &(\exists a')(\Inv{\idx}[a\leftarrow a'] \land a = a')&\\
    &\Leftrightarrow&\\
    &(\exists a')
      \left(\begin{array}{cc}
      \begin{array}{cc}
         &(a = a_0) \lor (\exists j)(\seen{j}{\idx} \land a = e_0^\at{j})\\
         \land &(a = a')
     \end{array}
     \end{array}\right)&\\
    &\Leftrightarrow& \\
    &(\exists a')
      \left(\begin{array}{cc}
      \begin{array}{cc}
         &(a = a_0 \land a = a')\\
         &\lor\\
         &(\exists j)(\seen{j}{\idx} \land a = e_0^\at{j}) \land (a = a')
     \end{array}
     \end{array}\right)&\\
    &\Leftrightarrow& \\
    &\left(\begin{array}{cc}
      \begin{array}{cc}
         &(a = a_0)\\
         &\lor\\
         &(\exists j)(\seen{j}{\idx} \land a = e_0^\at{j})
     \end{array}
     \end{array}\right)&\\
  \end{eqnarray*}
  %
  - Computation of $A \lor B$
  \begin{eqnarray*}
    A \lor B&\Leftrightarrow&
               \left(\begin{array}{cc}
                    &(a = a_0) \lor (\forall j)(\seen{j}{\idx+1} \impl a = e_0^\at{j})\\
               \end{array}\right) \\
    &\Leftrightarrow& \Inv{\idx+1}
  \end{eqnarray*}

  This proves that \Inv{\idx} is the strongest loop invariant on the
  loop reduced to the current pattern \curpattern.
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Single Min/Max Pattern}

\pattern{
  A scalar variable $a$ is only modified in a single assignment, whose
  guard is a comparison between the variable and a value-preserving expression, and
  it receives the same value-preserving expression.
}{
  (a \bullet e^\at{\idx}) \rightarrow a := e^\at{\idx}  \qquad \bullet \in \{<, \leq, >, \geq \}
}{
  & (a \circ a_0) \land (\forall k)(\seen{k}{\idx} \impl a \circ e_0^\at{k})\\
  \land & ((a = a_0) \lor (\exists j)(\seen{j}{\idx} \land a = e_0^\at{j}))
}
%
where $\circ$ can be deduced from $\bullet$ as follows:
$\begin{array}{l|llll}
\bullet & <    & \leq & >    & \geq \\ \hline
\circ   & \geq & \geq & \leq & \leq
\end{array}$

\vspace{0.5cm}
\patternnote Above invariant is equivalent to its complex form:
\begin{eqnarray*}
&(a = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg (a_0 \bullet e_0^\at{j}))\\
\lor
& ((\exists j)(\seen{j}{\idx} \land a = e_0^\at{j} \land (\forall k)(\betweens{j}{k}{i} \impl
  \neg (a_0 \bullet e_0^\at{k}))) \land \\
&(\forall k)(\seen{k}{\idx} \impl a \circ e_0^\at{k}))\\
\end{eqnarray*}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1\leq j < i \impl \neg (m_0 < A[j]))\\
           &\lor\\
           &((\exists j)(1\leq j < i \land m = A[j]) \land \\
           &(\forall k)(1\leq k < i \impl m \geq A[k]))\\
         \end{array}\right)\\
    &&~~~m < A(i) \rightarrow m := A(i)\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
\ifdefined\longversion
  The proof proceeds by induction on the number of iterations \idx.

  \subproof{Proof of loop invariant initalization:}
  In a loop reduced only to this pattern, no variable is modified, excepted
  $a$ and current value of the loop index. At the beginning of the loop, $i = \idxinitial$,
  $(a = a_0)$.
  $$(i = \idxinitial \land a = a_0) \impl \Inv{\idx}$$
  and
  $$(\Inv{\idx} \land \idx = \idxinitial) \Leftrightarrow (i = \idxinitial \land a = a_0)$$
  because $i = \idxinitial$, $\nexists j$ such that $\idxinitial \leq j <i$, i.e $(\seen{j}{\idx})=\mathit{false}$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.\\

  \subsubproof{First step of induction:}
  The most significant information we know about this pattern before
  the execution of loop body at first iteration is that $(a = a_0)$.
  Thus we start from precondition $(a = a_0)$
  %
  By \vpp we have:
  \begin{eqnarray*}
    &\spost{(a \bullet e^\at{\idxinitial}) \rightarrow a := e^\at{\idxinitial}}{a = a_0}&\\
    &=&\\
    &\spost{(a \bullet e_0^\at{\idxinitial}) \rightarrow a := e_0^\at{\idxinitial}}{a = a_0}&\\
    &=&\\
    &(\exists a')\left(\begin{array}{ll}
                         & (a' = a_0) \\
                         \land & (a' \bullet e_0^\at{\idxinitial}) \impl a = e_0^\at{\idxinitial} \\
                         \land & \neg (a' \bullet e_0^\at{\idxinitial}) \impl a = a'
                   \end{array}\right)&\\
  \end{eqnarray*}
  %
  Simplifying the existential:
  \begin{eqnarray*}
    &&\Leftrightarrow \left(\begin{array}{ll}
                         & (a_0 \bullet e_0^\at{\idxinitial}) \impl a = e_0^\at{\idxinitial} \\
                         \land & \neg (a_0 \bullet e_0^\at{\idxinitial}) \impl a = a_0
                      \end{array}\right) \\
  \end{eqnarray*}
  %
  The two guards form the partition, so we can write the formula in disjunctive normal form (DNF) :
  %
  \begin{eqnarray*}
    &&\Leftrightarrow \left(\begin{array}{ll}
                    & (a_0 \bullet e_0^\at{\idxinitial}) \land a = e_0^\at{\idxinitial} \\
                    \lor & \neg (a_0 \bullet e_0^\at{\idxinitial}) \land a = a_0
                   \end{array}\right) \\
  \end{eqnarray*}
  %
  Let us note :
  %
  \begin{eqnarray*}
    &&A=\neg (a_0 \bullet e_0^\at{\idxinitial}) \land (a = a_0)\\
    &&B=(a_0 \bullet e_0^\at{\idxinitial}) \land a = e_0^\at{\idxinitial}\\
  \end{eqnarray*}

  \subsubproof{Case $\bullet \in \{<, >\}$}
  %
  Notice that in this case $\neg (a_0 \bullet e_0^\at{\idxinitial}) = (a_0 \circ e_0^\at{\idxinitial})$.\\
  \begin{eqnarray*}
    &&A = (a_0 \circ e_0^\at{\idxinitial}) \land (a = a_0)\\
    &&A \Leftrightarrow (a \circ e_0^\at{\idxinitial}) \land (a = a_0)\\
    &&A \Leftrightarrow (a \circ e_0^\at{\idxinitial}) \land (a = a_0) \land (a = a_0 \impl a \circ a_0)\\
    &&A \Leftrightarrow (a \circ e_0^\at{\idxinitial}) \land (a = a_0) \land (a \circ a_0)\\
  \end{eqnarray*}
  %
  Formatting:
  %
  \begin{eqnarray*}
    &&A\Leftrightarrow \left(\begin{array}{cc}
                        &(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
                        \land& (a = a_0)\\
                     \end{array}\right) \\
  \end{eqnarray*}
  %
  Let us denote by
  \begin{eqnarray*}
    &&A_1=(a \geq a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
    &&A_2=(a = a_0)\\
  \end{eqnarray*}
  %
  Compute now $B$
  \begin{eqnarray*}
    &&B=(a_0 \bullet e_0^\at{\idxinitial}) \land (a = e_0^\at{\idxinitial})\\
    &&B=(a_0 \bullet a) \land (a = e_0^\at{\idxinitial})\\
    &&B=(a_0 \bullet a) \land (a = e_0^\at{\idxinitial}) \land (a = e_0^\at{\idxinitial} \impl (a \circ e_0^\at{\idxinitial}))\\
    &&B=(a_0 \bullet a) \land (a = e_0^\at{\idxinitial}) \land (a \circ e_0^\at{\idxinitial})\\
    &&B=(a \circ a_0 \land a \neq a_0) \land (a = e_0^\at{\idxinitial}) \land (a \circ e_0^\at{\idxinitial})\\
  \end{eqnarray*}
  %
  Formatting:
  \begin{eqnarray*}
    &&B\Leftrightarrow \left(\begin{array}{cc}
                        &(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
                        \land& (a \neq a_0) \land (a = e_0^\at{\idxinitial})\\
                     \end{array}\right) \\
  \end{eqnarray*}
  %
  Let us denote by
  \begin{eqnarray*}
    &&B_1=(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
    &&B_2=(a \neq a_0) \land (a = e_0^\at{\idxinitial})\\
  \end{eqnarray*}
  %
  $B_1 = A_1$ then :
  \begin{eqnarray*}
    &&A \lor B \Leftrightarrow (A_1 \land A_2) \lor (B_1 \land B_2)\\
    &&A \lor B \Leftrightarrow A_1 \land (A_2 \lor  B_2)\\
    &&A \lor B \Leftrightarrow
                         \left(\begin{array}{cc}
                             &(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
                             &\land\\
                             & (a = a_0) \lor ((a \neq a_0) \land (a = e_0^\at{\idxinitial}))
                         \end{array}\right) \\
  \end{eqnarray*}

 \subsubproof{Case $\bullet \in \{\leq, \geq\}$}
  %
  \begin{eqnarray*}
    &&A = \neg (a_0 \bullet e_0^\at{\idxinitial}) \land (a = a_0)\\
    &&A \Leftrightarrow \neg(a \bullet e_0^\at{\idxinitial}) \land (a = a_0)\\
    &&A \Leftrightarrow (a \circ e_0^\at{\idxinitial} \land a \neq e_0^\at{\idxinitial}) \land (a = a_0) \land (a = a_0 \impl a \circ a_0)\\
    &&A \Leftrightarrow (a \circ e_0^\at{\idxinitial} \land a \neq e_0^\at{\idxinitial}) \land (a = a_0) \land (a \circ a_0)\\
  \end{eqnarray*}
  %
  Formatting:
  %
  \begin{eqnarray*}
    &&A\Leftrightarrow \left(\begin{array}{cc}
                        &(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
                        \land& (a = a_0) \land (a \neq e_0^\at{\idxinitial})\\
                     \end{array}\right) \\
  \end{eqnarray*}
  %
  Let us denote by
  \begin{eqnarray*}
    &&A_1=(a \geq a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
    &&A_2=(a = a_0) \land (a \neq e_0^\at{\idxinitial})\\
  \end{eqnarray*}
  %
  Compute now $B$
  \begin{eqnarray*}
    &&B=(a_0 \bullet e_0^\at{\idxinitial}) \land (a = e_0^\at{\idxinitial})\\
    &&B=(a_0 \bullet a) \land (a = e_0^\at{\idxinitial})\\
    &&B=(a \circ a_0) \land (a = e_0^\at{\idxinitial}) \land (a = e_0^\at{\idxinitial} \impl (a \circ e_0^\at{\idxinitial}))\\
    &&B=(a \circ a_0) \land (a = e_0^\at{\idxinitial}) \land (a \circ e_0^\at{\idxinitial})\\
  \end{eqnarray*}
  %
  Formatting:
  \begin{eqnarray*}
    &&B\Leftrightarrow \left(\begin{array}{cc}
                        &(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
                        \land& (a = e_0^\at{\idxinitial})\\
                     \end{array}\right) \\
  \end{eqnarray*}
  %
  Let us denote by
  \begin{eqnarray*}
    &&B_1=(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
    &&B_2=(a = e_0^\at{\idxinitial})\\
  \end{eqnarray*}
  %
  $B_1 = A_1$ then :
  \begin{eqnarray*}
    &&A \lor B \Leftrightarrow  = (A_1 \land A_2) \lor (B_1 \land B_2)\\
    &&A \lor B \Leftrightarrow A_1 \land (A_2 \lor  B_2)\\
    &&A \lor B \Leftrightarrow
                         \left(\begin{array}{cc}
                             &(a \circ a_0) \land (\forall k)(\seen{k}{\idxinitial+1} \impl a \circ e_0^\at{k})\\
                             &\land\\
                             & ((a = a_0) \land (a \neq e_0^\at{\idxinitial})) \lor (a = e_0^\at{\idxinitial})
                         \end{array}\right) \\
  \end{eqnarray*}

  \subsubproof{Induction:}
  \begin{eqnarray*}
    &\spost{(a \bullet e^\at{\idx}) \rightarrow a := e^\at{\idxinitial}}{\Inv{\idx}}&\\
    &=&\\
    &\spost{(a \bullet e_0^\at{\idx}) \rightarrow a := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &(\exists a')\left(\begin{array}{cc}
                         & \Inv{\idx}[a \leftarrow a'] \\
                         \land & (a' \bullet e_0^\at{\idx}) \impl a = e_0^\at{\idx} \\
                         \land & \neg (a' \bullet e_0^\at{\idx}) \impl (a = a')
                   \end{array}\right)&\\
    &=& \\
    &(\exists a')\left(\begin{array}{cc}
                         & \Inv{\idx}[a \leftarrow a']\\
                         &\land\\
                         &\left(\begin{array}{ll}
                               & (a' \bullet e_0^\at{\idx}) \impl a = e_0^\at{\idx} \\
                               \land
                               & \neg (a' \bullet e_0^\at{\idx}) \impl (a = a')
                         \end{array}\right)\\
                   \end{array}\right)&\\
  \end{eqnarray*}
  %
  The two guards form the partition, so we can write the formula in disjunctive normal form (DNF) :
  \begin{eqnarray*}
    &&\Leftrightarrow (\exists a')\left(\begin{array}{cc}
                    & \Inv{\idx}[a \leftarrow a'] \land (a' \bullet e_0^\at{\idx}) \land (a = e_0^\at{\idx}) \\
                    &\lor\\
                    &\Inv{\idx}[a \leftarrow a'] \land \neg (a' \bullet e_0^\at{\idx}) \land (a = a')
                   \end{array}\right) \\
  \end{eqnarray*}
  %
  Let us note :
  %
  \begin{eqnarray*}
    &&A=(\exists a')(\Inv{\idx}[a \leftarrow a'] \land \neg (a' \bullet e_0^\at{\idx}) \land (a = a'))\\
    &&B=(\exists a')(\Inv{\idx}[a \leftarrow a'] \land (a' \bullet e_0^\at{\idx}) \land (a = e_0^\at{\idx})) \\
  \end{eqnarray*}

  \subsubproof{Case $\bullet \in \{<, >\}$}
  Notice that in this case $\neg (a' \bullet e_0^\at{\idx}) = a' \circ e_0^\at{\idx}$,\\
  %
  Unfolding $\Inv{\idx}$ in $A$
  \begin{eqnarray*}
    &&A=(\exists a')(\Inv{\idx}[a \leftarrow a'] \land \neg (a' \bullet e_0^\at{\idx}) \land (a = a'))\\
    &&A\Leftrightarrow (\exists a') \left(\begin{array}{cc}
                 &\left(\begin{array}{cc}
                    & (a' = a_0) \land (a' \circ a_0) \land (\forall k)(\seen{k}{\idx} \impl a' \circ e_0^\at{k})\\
                    &\lor\\
                    & (\exists j)(\seen{j}{\idx} \land a' = e_0^\at{j}) \land (a' \circ a_0) \land \\
                    &(\forall k)(\seen{k}{\idx} \impl a' \circ e_0^\at{k})\\
                  \end{array}\right)\\
                 &\land\\
                 &(a' \circ e_0^\at{\idx}) \land (a = a')\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  By distributing $(a \circ e_0^\at{\idx}) \land (a = a')$, $A = A_1 \lor A_2$,  with
  \begin{eqnarray*}
    &&A_1 = (\exists a') \left(\begin{array}{cc}
                 &(a' = a_0) \land (a' \circ a_0) \land (\forall k)(\seen{k}{\idx} \impl a' \circ e_0^\at{k})\\
                 &\land (a' \circ e_0^\at{\idx}) \land (a = a')\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  By eliminating existential $(a = a')$ we have:
  \begin{eqnarray*}
    &&A_1 = \left(\begin{array}{cc}
                 &(a = a_0) \land (a \circ a_0) \land (\forall k)(\seen{k}{\idx} \impl a \circ e_0^\at{k})
                 \land (a \circ e_0^\at{\idx})\\
                \end{array}\right)\\
    &&A_1 \Leftrightarrow \left(\begin{array}{cc}
                 &(a = a_0) \land (a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  \begin{eqnarray*}
    &&A_2 = (\exists a') \left(\begin{array}{cc}
                  & (\exists j)(\seen{j}{\idx} \land a' = e_0^\at{j}) \land (a' \circ a_0) \land \\
                  &(\forall k)(\seen{k}{\idx} \impl a' \circ e_0^\at{k}) \land (a' \circ e_0^\at{\idx}) \land (a = a')\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  Approaching existential close as possible
  \begin{eqnarray*}
    &&A_2 = \left(\begin{array}{cc}
                 & (\exists a') ((\exists j)(\seen{j}{\idx} \land a' = e_0^\at{j}) \land (a = a'))\\
                 &\land\\
                 &(a \circ a_0) \land (\forall k)(\seen{k}{\idx} \impl a \circ e_0^\at{k}) \land (a \circ e_0^\at{\idx})\\
                \end{array}\right)\\
    &&A_2 = \left(\begin{array}{cc}
                 & (\exists a') ((\exists j)(\seen{j}{\idx} \land a' = e_0^\at{j}) \land (a = a'))\\
                 &\land\\
                 &(a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                \end{array}\right)\\
  \end{eqnarray*}
  %
  $A_1 \lor A_2$ equivalent
  \begin{eqnarray*}
    &&A_2 = \left(\begin{array}{cc}
                 & (\exists j)(\seen{j}{\idx} \land a = e_0^\at{j}))\\
                 &\land\\
                 &(a = a_0) \land (a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                \end{array}\right)\\
  \end{eqnarray*}

  Compute now $B$ by unfolding $\Inv{\idx}$
  \begin{eqnarray*}
    B &=& (\exists a')(\Inv{\idx}[a \leftarrow a'] \land (a' \bullet e_0^\at{\idx}) \land (a = e_0^\at{\idx})) \\
    &=& (\exists a')(\Inv{\idx}[a \leftarrow a'] \land (a' \bullet e_0^\at{\idx}) \land (a = e_0^\at{\idx})) \\
    &\Leftrightarrow& (a = e_0^\at{\idx})
  \end{eqnarray*}
  %
  Because
  \begin{eqnarray*}
    &&B\Leftrightarrow (\exists a')\left(\begin{array}{cc}
                 &\left(\begin{array}{cc}
                    & (a' \circ a_0) \land  (a' = a_0) \land (\forall k)(\seen{k}{\idx} \impl a' \circ e_0^\at{k})\\
                    &\lor\\
                    & (a' \circ a_0) \land (\exists j)(\seen{j}{\idx} \land a' = e_0^\at{j}) \land \\
                    &(\forall k)(\seen{k}{\idx} \impl a' \circ e_0^\at{k})\\
                  \end{array}\right)\\
                 &\land\\
                 &(a' \bullet e_0^\at{\idx})
                \end{array}\right) = true
  \end{eqnarray*}
  %
  Compute $A_2\lor B$
  \begin{eqnarray*}
    &&A_2\lor B\Leftrightarrow \left(\begin{array}{cc}
                 &\left(\begin{array}{cc}
                 &(a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                 &\land\\
                 & (\exists a') ((\exists j)(\seen{j}{\idx} \land a' = e_0^\at{j}) \land (a = a'))\\
                  \end{array}\right)\\
                 &\lor\\
                 &(a = e_0^\at{\idx})
                \end{array}\right)\\
    &&A_2\lor B\Leftrightarrow \left(\begin{array}{cc}
                 &(a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                 &\land\\
                 & (\exists j)(\seen{j}{\idx+1} \land a = e_0^\at{j})\\
                  \end{array}\right)\\
  \end{eqnarray*}

  \begin{eqnarray*}
    &&A_1 \lor A_2 \lor B \Leftrightarrow \left(\begin{array}{cc}
                 &(a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                 &\land (\exists j)(\seen{j}{\idx+1} \land a = e_0^\at{j})\\
                 &\lor\\
                 &(a = a_0) \land (a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                  \end{array}\right)\\
    &&A_1 \lor A_2 \lor B \Leftrightarrow \left(\begin{array}{cc}
                              & (a \circ a_0) \land (\forall k)(\seen{k}{\idx+1} \impl a \circ e_0^\at{k})\\
                              \land & ((a = a_0) \lor (\exists j)(\seen{j}{\idx+1} \land a = e_0^\at{j}))
                  \end{array}\right)\\
  \end{eqnarray*}

 \subsubproof{Case $\bullet \in \{\leq, \geq\}$} TODO

\fi
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Single Min/Max Index Pattern}

\pattern{
  A scalar variable $a$ is only modified in a single assignment, whose
  guard is a comparison between a value-preserving expression and the same expression
  where the loop index is replaced by the variable, and it receives the value of
  the loop index.
}{
  (e^\at{a} \bullet e^\at{\idx}) \rightarrow a := \idx  \qquad \bullet \in \{<, \leq, >, \geq \}
}{
  &(a = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg (e_0^\at{a_0} \bullet e_0^\at{j})) \\
  \lor
  & ((\exists j)(\seen{j}{\idx} \land a = j) \land (\forall k)(\seen{k}{\idx} \impl e_0^\at{a} \circ e_0^\at{k}))
}
%
where $\circ$ can be deduced from $\bullet$ as follows:
$\begin{array}{l|llll}
\bullet & <    & \leq & >    & \geq \\ \hline
\circ   & \geq & \geq & \leq & \leq
\end{array}$

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1\leq j < i \impl \neg (A(m_0) < A[j]))\\
           &\lor\\
           &((\exists j)(1\leq j < i \land m = j) \land \\
           &(\forall k)(1\leq k < i \impl A(m) \geq A[k]))\\
         \end{array}\right)\\
    &&~~~A(m) < A(i) \rightarrow m := i\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 Same proof as above.
\end{proof}

%==================================================================================
%==================================================================================
\subsection{Integrate Patterns}

\subsubsection*{Certain Single Add-Up Pattern}

\pattern{
  A scalar variable $a$ is modified at most in a single assignment, whose
  guard is \textit{true}, and it receives its own previous value plus a constant.
}{
  \mathit{true} \rightarrow a := a + K
}{
  a = a_0 + K * (i-1)
}
%
\patternnote The change of $a$ follows a arithmetic serie because by reason of $K$
             and the first term $a_0$\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &m = m_0 + (i-1)\\
         \end{array}\right)\\
    &&~~~true \rightarrow m := m+1\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
\ifdefined\longversion
  The proof proceeds by induction on the number of iterations \idx.\\

  \subproof{Proof of loop invariant initalization:}
  In a loop reduced only to this pattern, no variable is modified, excepted
  $a$ and current value of the loop index. At the beginning of the loop, $i = \idxinitial$,
  $(a = a_0)$.
  $$(i = \idxinitial \land a = a_0) \impl \Inv{\idx}$$
  and
  $$(\Inv{\idx} \land \idx = \idxinitial) \Leftrightarrow (i = \idxinitial \land a = a_0)$$
  because $\idx \neq \idxinitial$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.
  \begin{eqnarray*}
    \spost{\mathit{true} \rightarrow a := a + K}{\Inv{\idx}}
    &=& (\exists a')( \Inv{\idx}[a \leftarrow a'] \land (a = a'+K))\\
    &\Leftrightarrow& (\exists a')(a' = a_0 + K * (i-1) \land (a = a' + K))\\
    &\Leftrightarrow& a = a_0 + K * (i-1) + K\\
    &\Leftrightarrow& a = a_0 + K * (i)\\
    &\Leftrightarrow& \Inv{\idx+1}
  \end{eqnarray*}
  This proves that \Inv{\idx} is the strongest loop invariant on the
  loop reduced to the current pattern \curpattern.
\fi
\end{proof}


%==================================================================================
%==================================================================================
\subsubsection*{Known Single Add-Up Pattern}

\pattern{
  A scalar variable $a$ is modified at most in a single assignment, whose
  guard is a value-preserving expression, and it receives its own previous value plus a constant $k$.
}{
  g^\at{\idx} \rightarrow a := a + K
}{
  &(a = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})) \\
  &\lor\\
  & (\exists j)
  \left(\begin{array}{cl}
        &\seen{j}{\idx} \land g_0^\at{j}\\
        \land& (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 + K * k) \\
        \land& (\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k})
  \end{array}\right)
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1\leq j < i \impl A(j)-B(j)\neq0)\\
           &\lor\\
           &(\exists j)(\seen{j}{\idx} \land A(j)-B(j)= 0\\
           &\land (\exists k)(1 \leq k \leq j \land m = m_0 + k)\\
           &\land (\forall k)(j < k < i \impl A(k)-B(k)\neq0))\\
         \end{array}\right)\\
    &&~~~A(i)-B(i)=0 \rightarrow m := m+1\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
\ifdefined\longversion
  The proof proceeds by induction on the number of iterations \idx.\\

  \noindent
  We start from precondition $(a = a_0)$ before the loop, because
  initially, the variable $a$ takes its initial value $a_0$.\\

  \noindent
  By \vpp we have :
  \begin{eqnarray*}
    \spost{g^\at{\idxinitial} \rightarrow a := a + K}{a = a_0}
    &=&\spost{g_0^\at{\idxinitial} \rightarrow a := a + K}{a = a_0}\\
    &=& (\exists a')\left(\begin{array}{ll}
                         & (a' = a_0) \\
                         \land & g_0^\at{\idxinitial} \impl (a = a_0 + K) \\
                         \land & \neg g_0^\at{\idxinitial} \impl (a = a')
                   \end{array}\right)\\
  \end{eqnarray*}
  %
  We simplify the existential :
  \begin{eqnarray*}
    \spost{g^\at{\idxinitial} \rightarrow a := a + K}{a = a_0}
    &\Leftrightarrow& \left(\begin{array}{ll}
                           & g_0^\at{\idxinitial} \impl (a = a_0 + K) \\
                           \land & \neg g_0^\at{\idxinitial} \impl (a = a_0)
                      \end{array}\right) \\
  \end{eqnarray*}
  %
  Since $g_0^\at{\idx}$ and $\neg g_0^\at{\idx}$ are a partition
  we can write the formula in disjunctive normal form (DNF) :
  %
  \begin{eqnarray*}
    \spost{g^\at{\idxinitial} \rightarrow a := a + K}{a = a_0}
    &\Leftrightarrow& \left(\begin{array}{ll}
                           & g_0^\at{\idxinitial} \land (a = a_0 + K)  \\
                           \lor & \neg g_0^\at{\idxinitial} \land (a = a_0)
                   \end{array}\right) \\
  \end{eqnarray*}
  %
  We format the above formula to have $\Inv{\idxinitial+1}$ as following :
  %
  \begin{eqnarray*}
    &\left(\begin{array}{ll}
                    & g_0^\at{\idxinitial} \land (a = a_0 + K)  \\
                    \lor & \neg g_0^\at{\idxinitial} \land (a = a_0)
    \end{array}\right)& \\
    &\Leftrightarrow&  \\
    &\left(\begin{array}{cc}
            &(a = a_0) \land (\forall j)(\seen{j}{\idxinitial+1} \impl \neg g_0^\at{j})\\
            &\lor\\
            &(\exists j)(\seen{j}{\idxinitial+1} \land g_0^\at{j} \land\\
            &(\exists k)(1 \leq k \leq \tocount{j} \land (a =  a_0 + K*k) \land  \\
            &(\forall k)(\betweens{j}{k}{\idxinitial+1} \impl \neg g_0^\at{k})))
      \end{array}\right)&\\
    &\Leftrightarrow& \\
    &\Inv{\idxinitial+1}&
  \end{eqnarray*}
  %
  Then :
  \begin{eqnarray*}
    \spost{g^\at{\idxinitial} \rightarrow a := a + K}{a = a_0} &\Leftrightarrow& \Inv{\idxinitial+1}
  \end{eqnarray*}

  Now assume \Inv{\idx} at loop iteration \idx. Notice that \Inv{\idx}
  does not mention any variables modified in the loop excepted $a$,
  initial values of others variables and current value of the loop index.
  %
  Let us prove that \Inv{\idx+1} at loop iteration $\idx+1$ is the strongest
  postcondition of \Inv{\idx} through the loop body at iteration \idx.
  %
  %
  \begin{eqnarray*}
    \spost{g^\at{\idx} \rightarrow a := a + K}{\Inv{\idx}}
    &=& \spost{g_0^\at{\idx} \rightarrow a := a + K}{\Inv{\idx}}\\
    &=& (\exists a')\left(\begin{array}{ll}
                     & \Inv{\idx}[a\leftarrow a'] \\
                    \land & g_0^\at{\idx}[a\leftarrow a'] \impl a = a + K\\
                    \land & \neg g_0^\at{\idx}[a\leftarrow a'] \impl a = a'
                   \end{array}\right)\\
    &\Leftrightarrow& (\exists a')\left(\begin{array}{cc}
                     & \Inv{\idx}[a\leftarrow a'] \\
                     &\land\\
                     &\left(\begin{array}{ll}
                           & g_0^\at{\idx} \land a = a + K \\
                          \lor & \neg g_0^\at{\idx} \land a = a'
                     \end{array}\right)\\
                   \end{array}\right)\\
    &\Leftrightarrow& A \lor B
  \end{eqnarray*}
  %
  With :
  \begin{eqnarray*}
    &&A=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land g_0^\at{\idx} \land a = a + K)\\
    &&B=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land \neg g_0^\at{\idx} \land a = a')
  \end{eqnarray*}
  %
  \subproof{Simplification of $A$ :}
  \begin{eqnarray*}
    A &=& (\exists a')(\Inv{\idx}[a\leftarrow a']) \land g_0^\at{\idx} \land a = a + K\\
      &\Leftrightarrow& g_0^\at{\idx} \land a = a + K
  \end{eqnarray*}
  %
  \subproof{Simplification of $B$}
  %
  \begin{eqnarray*}
    B=(\exists a')(\Inv{\idx}[a\leftarrow a'] \land (a = a') \land \neg g_0^\at{\idx})\\
  \end{eqnarray*}
  %
  Unfolding of $\Inv{\idx}[a\leftarrow a']$ :
  \begin{eqnarray*}
    B &=& (\exists a')
         \left(\begin{array}{cc}
              &(a' = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})) \lor\\
              & (\exists j)
              \left(\begin{array}{cl}
              &\seen{j}{\idx} \land g_0^\at{j}\\
              \land& (\exists k)(1 \leq k \leq \tocount{j} \land a' = a_0 + K * k) \\
              \land& (\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k})
              \end{array}\right)\\
              &\land\\
              &(a = a') \land \neg g_0^\at{\idx}
          \end{array}\right)\\
    &\Leftrightarrow& B_1 \land B_2
  \end{eqnarray*}
  %
  With :
  \subsubproof{Simplification of $B_1$ :}
  \begin{eqnarray*}
    B_1 &\Leftrightarrow& (\exists a')
         \left(\begin{array}{cc}
              &(a' = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})) \\
              &\land\\
              &(a = a') \land \neg g_0^\at{\idx}
           \end{array}\right) \\
         &\Leftrightarrow&
         \left(\begin{array}{cc}
              &(a = a_0) \land (\forall j)(\seen{j}{\idx+1} \impl \neg g_0^\at{j})) \\
           \end{array}\right)\\
  \end{eqnarray*}

  \subsubproof{Simplification of $B_2$ :}
  \begin{eqnarray*}
    B_2 &\Leftrightarrow& (\exists a')
         \left(\begin{array}{cc}
              & (\exists j)
              \left(\begin{array}{cl}
              &\seen{j}{\idx} \land g_0^\at{j}\\
              \land& (\exists k)(1 \leq k \leq \tocount{j} \land a' = a_0 + K * k) \\
              \land& (\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k})
              \end{array}\right)\\
              &\land\\
              &(a = a') \land  \neg g_0^\at{\idx}
           \end{array}\right)\\
  \end{eqnarray*}
  %
  $B_2$ is equivalent to :
  \begin{eqnarray*}
    B_2 &\Leftrightarrow &
        (\exists j)
        \left(\begin{array}{cl}
           &\seen{j}{\idx} \land g_0^\at{j}\\
           \land& (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 + K * k) \\
           \land& (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k})
        \end{array}\right)\\
  \end{eqnarray*}

  \subsubproof{Computation of $A \lor B_2$ :}
  \begin{eqnarray*}
   A \lor B_2
   &\Leftrightarrow&
          \begin{array}{cc}
              &(\exists j)
              \left(\begin{array}{cl}
                   &\seen{j}{\idx} \land g_0^\at{j}\\
                   \land& (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 + K * k) \\
                   \land& (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k})
              \end{array}\right)\\
              \lor &g_0^\at{\idx} \land a = a + K
          \end{array}
  \end{eqnarray*}

  By developping we have
  \begin{eqnarray*}
   A \lor B_2
    &\Leftrightarrow&
              (\exists j)
              \left(\begin{array}{cl}
                   &\seen{j}{\idx+1} \land g_0^\at{j}\\
                   \land& (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 + K * k) \\
                   \land& (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k})
              \end{array}\right)\\
  \end{eqnarray*}

  \subsubproof{Computation of $B_1 \lor A \lor B_2$ :}
  \begin{eqnarray*}
    B_1 \lor A \lor B_2
    &\Leftrightarrow&
        \begin{array}{cc}
          &(a = a_0) \land (\forall j)(\seen{j}{\idx+1} \impl \neg g_0^\at{j})) \\
          &\lor \\
          & (\exists j)
            \left(\begin{array}{cl}
              &\seen{j}{\idx+1} \land g_0^\at{j}\\
              \land& (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 + K * k) \\
              \land& (\forall k)(\betweens{j}{k}{\idx+1} \impl \neg g_0^\at{k})
           \end{array}\right)
        \end{array}\\
    &\Leftrightarrow&
    \Inv{\idx+1}
  \end{eqnarray*}
  %
  This proves that \Inv{\idx} is the strongest loop invariant on the
  loop reduced to the current pattern \curpattern.
\fi
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Known Multiple Add-Up Pattern}

\pattern{
  A scalar variable is modified in more than one assignment, all of
  whose guards are value-preserved, and it receives in each its own previous value
  plus a constant.
}{
  &g_1^\at{\idx} \rightarrow a := a + K_1\\
  &...\\
  &g_n^\at{\idx} \rightarrow a := a + K_n\\
}{
  &(a = a_0) \land (\forall j)(\forall r)( \seen{j}{\idx} \impl \neg g_{r0}^\at{j})) \\
  &\lor\\
  & (\exists j)
  \left(\begin{array}{cl}
  &(\exists r)(\seen{j}{\idx} \land g_{r0}^\at{j}) \\
  \land& (\exists k)(1 \leq k \leq \tocount{j} \\
  &\land a_0 + \mathit{min}(K_r) * k \leq a \leq a_0 + \mathit{max}(K_r) * k) \\
  \land& (\forall k)(\forall r)(\betweens{j}{k}{\idx} \impl \neg g_{r0}^\at{k})
  \end{array}\right)
}

\patternnote The existential and universal quantifiers on $r$
concern the implicit range $1 \leq r \leq n$.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1\leq j < i \impl A(j)-B(j) = 0)\\
           &\lor\\
           &(\exists j)(\seen{j}{\idx} \land (A(j)-B(j) < 0 \lor A(j)-B(j) > 0)\\
           &\land (\exists k)(1 \leq k \leq j \land m_0-k \leq m \leq m_0 +k) \\
           &\land (\forall k)(j < k < i \impl A(j)-B(j) = 0))\\
         \end{array}\right)\\
    &&~~~A(i)-B(i) < 0 \rightarrow m := m+1\\
    &&~~~A(i)-B(i) > 0 \rightarrow m := m-1\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Single Add-Up Pattern}

\pattern{
  A scalar variable $a$ is modified at most in a single assignment, whose
  guard is unknown, and it receives its own previous value plus a constant.
}{
  g^? \rightarrow a := a + K
}{
  &(a = a_0) \\
  &\lor \\
  & (\exists j)(\seen{j}{\idx} \land (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 + K * k))\\
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &m = (m = m_0) \lor \\
           &(\exists j)(1 \leq j < i \land (\exists k)(1 \leq k \leq j \land m = m_0+10*k))\\
         \end{array}\right)\\
    &&~~~F(m)=0 \rightarrow m := m+10\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Multiple Add-Up Pattern}

\pattern{
  A scalar variable is modified in more than one assignment, all of
  whose guards are unknown, and it receives in each its own previous value
  plus a constant.
}{
  &g^? \rightarrow a := a + K_1\\
  &...\\
  &g^? \rightarrow a := a + K_n\\
}{
  &(a = a_0) \\
  &\lor \\
  &(\exists j)(\seen{j}{\idx} \land (\exists k)(1 \leq k \leq \tocount{j} \land a_0 + \mathit{min}(K_r)*k \leq a \leq a_0 + \mathit{max}(K_r)*k))\\
}

\patternnote The existential and universal quantifiers on $r$
concern the implicit range $1 \leq r \leq n$.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \lor \\
           &(\exists j)(1 \leq j < i \land (\exists k)(1 \leq k \leq j \land m_0+10*k \leq m \leq m_0 +20*k))\\
         \end{array}\right)\\
    &&~~~F(m)=0 \rightarrow m := m+10\\
    &&~~~G(m)=0 \rightarrow m := m+20\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Certain Single Mult-Up Pattern}

\pattern{
  A scalar variable is only modified in a single assignment, whose
  guard is \textit{true}, and it receives its own previous value times
  (resp. divided by) a constant.
}{
  &\mathit{true} \rightarrow a := a \bullet K \qquad \bullet \in \{*, / \}
}{
  &a = a_0 \bullet K^{i-1}
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &m = m_0 * 2^{i-1}\\
         \end{array}\right)\\
    &&~~~true \rightarrow m := m*2\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Known Single Mult-Up Pattern}

\pattern{
  A scalar variable is only modified in a single assignment, whose
  guard is a value-preserving expression, and it receives its own previous value times
  (resp. divided by) a constant.
}{
  &g^\at{\idx} \rightarrow a := a \bullet K  \qquad \bullet \in \{*, / \}
}{
  &(a = a_0) \land (\forall j)(\seen{j}{\idx} \impl \neg g_0^\at{j})) \\
  \lor
  & (\exists j)\left(\begin{array}{cl}
  & \seen{j}{\idx} \land g_0^\at{j} \\
  \land& (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 \bullet K^k)\\
  \land& (\forall k)(\betweens{j}{k}{\idx} \impl \neg g_0^\at{k})
  \end{array}\right)
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \land (\forall j)(1 \leq j < i \impl A(j)-B(j)\neq0)\\
           &\lor (\exists j)(\seen{j}{\idx} \land (A(j)-B(j)= 0 \land \\
           &(\exists k)(1 \leq k \leq j \land m = m_0 * 2^k) \land\\
           &(\forall k)(j < k < i \impl A(k)-B(k)\neq0))\\
         \end{array}\right)\\
    &&~~~A(i)-B(i)=0 \rightarrow m := m*2\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Single Mult-Up Pattern}

\pattern{
  A scalar variable $a$ is modified at most in a single assignment, whose
  guard is unknown, and it receives its own previous value times
  (resp. divided by) a constant.
}{
  &g^? \rightarrow a := a \bullet K  \qquad \bullet \in \{*, / \}
}{
  &(a = a_0) \lor (\exists j)(\seen{j}{\idx} \land (\exists k)(1 \leq k \leq \tocount{j} \land a = a_0 \bullet K^k))\\
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(m = m_0) \lor (\exists j)(1 \leq j < i \land (\exists k)(1 \leq k \leq j \land m = m_0+10^k))\\
         \end{array}\right)\\
    &&~~~F(m)=0 \rightarrow m := m*10\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsection{Map Patterns}

\subsubsection*{Certain Single Map Pattern}

\pattern{
  An array variable is modified at index \idx, in at most single assignment, whose
  guard is \textit{true} and it receives a value-preserving expression.
}{
  &\mathit{true} \rightarrow A[\idx] := e^\at{\idx}
}{
  &(\forall j)(\seen{j}{\idx} \impl A[j] = e_0^\at{j}) \\
  \land& (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])
}

\patternnote This pattern corresponds in particular to an array copy.

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(1\leq j< i \impl A[j] = B[j]) \land\\
           &(\forall j)(1 > j \land j \geq i \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
         \end{array}\right)\\
    &&~~~true \rightarrow A[i] := B[i]\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
  \subproof{\textbf{Init Case}}
  $$\initcond{L} \equiv (\forall j)(\inbounds{A}{j} \impl A[j] = A_0[j])$$\\
  When $i = \idxinitial$, $\nexists j$ such that $\idxinitial \leq j <i$, i.e $\seen{j}{\idx}=\mathit{false}$\\
  and $\neg \seen{j}{\idx} \land \inbounds{A}{j} \equiv \inbounds{A}{j}$.\\
  so
  $$(\Inv{\idx} \land \idx = \idxinitial) = (\forall j)(\inbounds{A}{j} \impl A[j] = A_0[j])$$\\
  then
  $$\initcond{L} \Leftrightarrow (\Inv{\idx} \land \idx = \idxinitial)$$

  \subproof{\textbf{Preservation case}}
  The proof proceeds by induction on the number of iterations \idx.


  \subproof{\textbf{Base case}}
  \begin{eqnarray*}
    &&\spost{\true \rightarrow A[\idxinitial] := e^\at{\idxinitial}}{\initcond{L}  \land \Inv{\idxinitial}}\\
    &&\spost{\true \rightarrow A[\idxinitial] := e_0^\at{\idxinitial}}{\initcond{L} \land \Inv{\idxinitial}}\\
    &&=(\exists A')\left(\begin{array}{ll}
                         & (\forall j)(\inbounds{A'}{j} \impl A'[j] = A_0[j])\\
                         \land & A[\idxinitial] = e_0^\at{\idxinitial} \\
                         \land & (\forall j)( \inbounds{A}{j} \land j \neq \idxinitial) \Rightarrow (A[j] = A'[j]))
                   \end{array}\right)\\
  \end{eqnarray*}
  %
  $(\forall j)(\inbounds{A}{j} \land j \neq \idxinitial) \Rightarrow (A'[j] = A_0[j])$
  \begin{eqnarray*}
    &&=(\exists A')\left(\begin{array}{ll}
                         & (\forall j)(\inbounds{A'}{j} \impl A'[j] = A_0[j])\\
                         \land & A[\idxinitial] = e_0^\at{\idxinitial} \\
                         \land & (\forall j)( \inbounds{A}{j} \land j \neq \idxinitial) \Rightarrow (A[j] = A_0[j]))
                   \end{array}\right)\\
  \end{eqnarray*}

  \begin{eqnarray*}
    &&=\left(\begin{array}{ll}
            & A[\idxinitial] = e_0^\at{\idxinitial} \\
            \land & (\forall j)( \inbounds{A}{j} \land j \neq \idxinitial) \Rightarrow (A[j] = A_0[j]))
        \end{array}\right)\\
  \end{eqnarray*}
  %
  Formating :
  \begin{eqnarray*}
    &&\Leftrightarrow \left(\begin{array}{ll}
                           \land & (\forall j)(\seen{j}{\idxinitial+1}\impl A[j] = e_0^\at{j}) \\
                           \land & (\forall j)(\neg \seen{j}{initial} \land \inbounds{A}{j}) \Rightarrow (A[j] = A_0[j]))
                      \end{array}\right) \\
    &&\Leftrightarrow \Inv{\idxinitial+1}
  \end{eqnarray*}

  \subproof{\textbf{Inductive Step}}
  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.
  \begin{eqnarray*}
    &\spost{\true \rightarrow A[\idx] := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &(\exists A')\left(\begin{array}{cc}
                         & \Inv{\idx}[A\leftarrow A'] \\
                         \land & (A[\idx] = e_0^\at{\idx}) \\
                         \land & (\forall j)( \inbounds{A}{j} \land \neg (j= \idx) \Rightarrow (A[j] = A'[j])
                   \end{array}\right)&
  \end{eqnarray*}
  %
  By unfolding  $\Inv{\idx}[A\leftarrow A']$ we have :
  \begin{eqnarray*}
    (\exists A')\left(\begin{array}{cc}
         &(\forall j)(\seen{j}{\idx} \impl A'[j] = e_0^\at{j}) \\
         \land &(\forall j)(\neg \seen{j}{\idx} \land \inbounds{A'}{j} \impl A'[j] = A_0[j])\\
         \land & (A[\idx] = e_0^\at{\idx}) \\
         \land & (\forall j)((\inbounds{A}{j} \land j \neq \idx) \Rightarrow (A[j] = A'[j]))
      \end{array}\right)&
  \end{eqnarray*}
  %
  Let
  \begin{eqnarray*}
    F_1 &&= \left(\begin{array}{ll}
          &(\forall j)(\seen{j}{\idx} \land g_0^\at{j} \impl A'[j] = e_0^\at{j}) \\
          \land & g_0^\at{\idx} \Rightarrow (A[\idx] = e_0^\at{\idx}) \\
    \end{array}\right)\\
      &&\Leftrightarrow (\forall j)(\seen{j}{\idx+1} \land g_0^\at{j} \impl A[j] = e_0^\at{j})
  \end{eqnarray*}
  and
  \begin{eqnarray*}
    F_2 &&= \left(\begin{array}{ll}
          & (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A'}{j} \impl A'[j] = A_0[j])\\
         \land & (\forall j) ((\inbounds{A}{j} \land j \neq \idx) \Rightarrow (A[j] = A'[j])
    \end{array}\right)\\
      &&\Leftrightarrow (\forall j)(\neg \seen{j}{\idx+1} \land \inbounds{A}{j} \impl A[j] = A_0[j])
  \end{eqnarray*}
  so
  \begin{eqnarray*}
    &\spost{\true \rightarrow A[\idx] := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &\left(\begin{array}{cc}
           &(\forall j)(\seen{j}{\idx+1} \impl A[j] = e_0^\at{j}) \\
           \land& (\forall j)(\neg \seen{j}{\idx+1} \land \inbounds{A}{j} \impl A[j] = A_0[j])
      \end{array}\right)&
  \end{eqnarray*}

%\fi
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Certain Shifted Single Map Pattern}

\pattern{
  An array variable is modified at index \idx plus a constant $k$, in at most single assignment,
  whose guard is \textit{true}, and it receives a value-preserving expression.
}{
  &\mathit{true} \rightarrow A[\idx + K] := e^\at{\idx}
}{
  &(\forall j)(\seen{j}{\idx} \impl A[j + K] = e_0^\at{j}) \\
  \land& (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j + K} \impl A[j + K] = A_0[j + K])
}

\patternnote All map patterns can be shifted like the above.

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(1 \leq j < i \impl A[j+1] = B[j]) \land\\
           &(\forall j)(1 > j \land j \geq i \land \inbounds{A}{j+1} \impl A[j+1] = A_0[j+1])\\
         \end{array}\right)\\
    &&~~~true \rightarrow A[i+1] := B[i]\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Known Single Map Pattern}

\pattern{
  An array variable is modified at index \idx in at most single assignment, whose
  guard is a value-preserving expression, and it receives a value-preserving expression.
}{
  &g^\at{\idx} \rightarrow A[\idx] := e^\at{\idx}
}{
  &(\forall j)(\seen{j}{\idx} \land g_0^\at{j} \impl A[j] = e_0^\at{j}) \\
  \land&(\forall j)(\seen{j}{\idx} \land \neg g_0^\at{j} \impl A[j] = A_0[j]) \\
  \land&
  (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(1 \leq j < i \land A_0[j] \neq 0 \impl A[j] = 0)\\
           \land &(\forall j)(1 \leq j < i \land A_0[j] = 0 \impl A[j] = A_0[j])\\
           \land &(\forall j)(1 > j \land j \geq i \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
         \end{array}\right)\\
    &&~~~A[i] \neq 0 \rightarrow A[i] := 0\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
%\ifdefined\longversion
  The proof proceeds by induction on the number of iterations \idx.\\

  \subproof{Proof of loop invariant initalization:}
  In a loop reduced only to this pattern, no variable is modified, excepted
  $A$ and current value of the loop index.\\
  At the beginning of the loop
  $$\initcond{L} \equiv (\forall j)(\idxinitial \leq j \leq \idxfinal \impl A[j] = A_0[j])$$\\
  When $i = \idxinitial$, $\nexists j$ such that $\idxinitial \leq j <i$, i.e $\seen{j}{\idx}=\mathit{false}$\\
  and $\neg \seen{j}{\idx} \land \inbounds{A}{j} \equiv \idxinitial \leq j \leq \idxfinal$.\\
  so
  $$(\Inv{\idx} \land \idx = \idxinitial) = (\forall j)(\idxinitial \leq j \leq \idxfinal \impl A[j] = A_0[j])$$\\
  then
  $$(\initcond{L} \land i = \idxinitial) \Leftrightarrow (\Inv{\idx} \land \idx = \idxinitial)$$

  \subproof{Proof of loop invariant preservation in a loop reduced to \curpattern:}
  Now assume \Inv{\idx} at loop iteration \idx. Let us prove that \Inv{\idx+1}
  at loop iteration $\idx+1$ is the strongest postcondition of \Inv{\idx}
  through the loop body at iteration \idx.
  %
  Notice that \Inv{\idx} does not mention any variables modified in the loop
  excepted $a$ and current value of the loop index.
  \begin{eqnarray*}
    &\spost{g_0^\at{\idx} \rightarrow A[\idx] := e_0^\at{\idx}}{\Inv{\idx}}&\\
    &=&\\
    &(\exists A')\left(\begin{array}{cc}
                         & \Inv{\idx}[A\leftarrow A'] \\
                         \land & g_0^\at{\idx} \Rightarrow (A[\idx] = e_0^\at{\idx}) \\
                         \land & (\forall j)( \inbounds{A}{j} \land \neg (g_0^\at{j} \land j= \idx) \Rightarrow (A[j] = A'[j])
                   \end{array}\right)&
  \end{eqnarray*}
  %
  By unfolding  $\Inv{\idx}[A\leftarrow A']$ we have :
  \begin{eqnarray*}
    &&\Leftrightarrow (\exists A') \left(\begin{array}{ll}
         &(\forall j)(\seen{j}{\idx} \land g_0^\at{j} \impl A'[j] = e_0^\at{j}) \\
         \land&(\forall j)(\seen{j}{\idx} \land \neg g_0^\at{j} \impl A'[j] = A_0[j]) \\
         \land&
         (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A'}{j} \impl A'[j] = A_0[j])\\
         \land & g_0^\at{\idx} \Rightarrow (A[\idx] = e_0^\at{\idx}) \\
         \land & (\forall j) (\inbounds{A}{j} \land \neg g_0^\at{\idx}) \Rightarrow (A[j] = A'[j])) \\
         \land & (\forall j) ((\inbounds{A}{j} \land j \neq \idx) \Rightarrow (A[j] = A'[j])
    \end{array}\right)\\
  \end{eqnarray*}
  %
  regroup them :
  \begin{eqnarray*}
    &&\Leftrightarrow (\exists A') \left(\begin{array}{ll}
        &\left(\begin{array}{ll}
             &(\forall j)(\seen{j}{\idx} \land g_0^\at{j} \impl A'[j] = e_0^\at{j}) \\
             \land & g_0^\at{\idx} \Rightarrow (A[\idx] = e_0^\at{\idx}) \\
        \end{array}\right)\\
        \land&
        \left(\begin{array}{ll}
             & (\forall j)(\seen{j}{\idx} \land \neg g_0^\at{j} \impl A'[j] = A_0[j]) \\
            \land & (\forall j) (\inbounds{A}{j} \land \neg g_0^\at{\idx}) \Rightarrow (A[j] = A'[j])) \\
        \end{array}\right)\\
        \land&
        \left(\begin{array}{ll}
             & (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A'}{j} \impl A'[j] = A_0[j])\\
             \land & (\forall j) ((\inbounds{A}{j} \land j \neq \idx) \Rightarrow (A[j] = A'[j])
        \end{array}\right)\\
    \end{array}\right)\\
  \end{eqnarray*}
%\fi
\end{proof}


%==================================================================================
%==================================================================================
\subsubsection*{Known Multiple Map Pattern}

\pattern{
  An array variable is modified in more than one assignment, all
  of whose guards are value-preserving expressions, at index \idx, and it receives in each a
  value-preserving expression.
}{
  &g_1^\at{\idx} \rightarrow A[\idx] := e_1^\at{\idx}\\
  &...\\
  &g_n^\at{\idx} \rightarrow A[\idx] := e_n^\at{\idx}\\
}{
  &(\forall j)(\forall r)(\seen{j}{\idx} \land g_{r0}^\at{j} \impl A[j] = e_{r0}^\at{j}) \\
  \land&(\forall j)(\seen{j}{\idx} \land (\forall r) (\neg g_{r0}^\at{j})) \impl A[j] = A_0[j]) \\
  \land&
  (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
}

\patternnote The existential and universal quantifiers on $r$
concern the implicit range $1 \leq r \leq n$.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(1 \leq j < i \land (A_0[j] < 0 \impl A[j] = -1 \lor A_0[j] > 0 \impl A[j] = +1)\\
           &\land (\forall j)(1 \leq j < i \land A_0[j] = 0 \impl A[j] = A_0[j])\\
           &\land (\forall j)(1 > j \land j \geq i \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
         \end{array}\right)\\
    &&~~~A[i] < 0 \rightarrow A[i] := -1\\
    &&~~~A[i] > 0 \rightarrow A[i] := +1\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Single Map Pattern}

\pattern{
  An array variable is only modified in a single assignment, whose
  guard is unknown, at index \idx, and it receives a value-preserving expression.
}{
  &g^? \rightarrow A[\idx] := e^\at{\idx}
}{
  &(\forall j)(\seen{j}{\idx} \impl A[j] = e_0^\at{j} \lor A[j] = A_0[j]) \\
  \land&
  (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(1 \leq j < i \impl A[j] = 0 \lor A[j]=A_0[j])\\
           &\land (\forall j)(1 > j \land j \geq i \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
         \end{array}\right)\\
    &&~~~A[i/2] \rightarrow A[i] := 0\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Multiple Map Pattern}

\pattern{
  An array variable is modified in more than one assignment, all
  of whose guards are unknown, at index \idx, and it receives in each a
  value-preserving expression.
}{
  &g^? \rightarrow A[\idx] := e_1^\at{\idx}\\
  &...\\
  &g^? \rightarrow A[\idx] := e_n^\at{\idx}\\
}{
  &(\forall j)(\seen{j}{\idx} \impl (\exists r)(A[j] = e_{r0}^\at{j}) \lor A[j] = A_0[j]) \\
  \land&
  (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
}

\patternnote The existential and universal quantifiers on $r$
concern the implicit range $1 \leq r \leq n$.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\begin{array}{cc}
           &(\forall j)(1 \leq j < i \impl (A[j] = -1 \lor A[j] = +1 \lor A[j] = A_0[j])\\
           &\land (\forall j)(1 > j \land j \geq i \land \inbounds{A}{j}\impl A[j] = A_0[j])\\
         \end{array}\\
    &&~~~A[i-1] < A[i-2] \rightarrow A[i] := -1\\
    &&~~~A[i-1] > A[i-2] \rightarrow A[i] := +1\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Filter Pattern}

\pattern{
  An array variable is only modified in a single assignment, whose
  guard is a value-preserving expression, at index $v$, and it receives in each a
  value-preserving expression. Scalar variable $v$ is incremented in a single assignment,
  whose guard is the same as the one above.
}{
  &g^\at{\idx} &\rightarrow& A[v] := e^\at{\idx}\\
  &g^\at{\idx} &\rightarrow& v := v + 1\\
}{
  &(\forall j)(\seen{j}{\idx} \land g_0^\at{j} \impl (\exists k)(v_0 \leq k < v \land A[k] = e_0^\at{j}))  \\
  \land&
  (\forall k)(v_0 \leq k < v \impl (\exists j)(\seen{j}{\idx} \land g_0^\at{j} \land A[k] = e_0^\at{j}))  \\
  \land &
  (\forall k_1, k_2)((\exists j_1,j_2) (k_1 \leq k_2 \impl
  \left(\begin{array}{cc}
       &\betweens{\idxinitial}{j_1}{j_2}\\
       \land &\betweens{j_1}{j_2}{i}\\
       \land &A[k_1] = e_0[j_1]\\
       \land &A[k_2] = e_0[j_2]\\
  \end{array}\right)))\\
  \land&
  (\forall k)(k \geq v \land \inbounds{A}{k} \impl A[k] = A_0[k])\\
}
%
\patternnote This pattern corresponds in particular to an array filter, in
which elements satisfying a certain condition are copied to the front of the
array.

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\begin{array}{ll}
           &(\forall j)(1 \leq j < i \land A_0[j] > 0 \impl (\exists k)(\upsilon_0 \leq k < \upsilon \land B[k] = A_0[j]))\\
           \land &(\forall k)(\upsilon_0 \leq k < \upsilon \impl (\exists j)(1 \leq j < i \land  A_0[j] > 0 \land B[k] = A_0[j]))\\
           \land &(\forall k_1, k_2)((\exists j_1,j_2) (k_1 \leq k_2 \impl
                 \left(\begin{array}{cc}
                      &\betweens{j_1}{j_2}{i}\\
                      \land &\betweens{\idxinitial}{j_1}{j_2}\\
                      \land &B[k_1] = A_0[j_1]\\
                      \land &B[k_2] = A_0[j_2]\\
                 \end{array}\right)))\\
           \land &(\forall k)(k \geq \upsilon \land \inbounds{A}{k} \impl B[k] = B_0[k])\\
         \end{array}\\
    &&~~~A[i] > 0 \rightarrow B[\upsilon] := A[i]\\
    &&~~~A[i] > 0 \rightarrow \upsilon := \upsilon + 1\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsection{Exchange Patterns}

\subsubsection*{Known Exchange Pattern}

\pattern{
  An array variable is only modified in a single assignment,
  whose guard is a value-preserving expression, at some unkown index,
  and it receives a value-preserving expression.
}{
  &g^\at{\idx} \rightarrow A[e^?] := e^\at{\idx}\\
}{
  &(\forall j)\left(\begin{array}{cc}
                    &\inbounds{A}{j} \impl (A[j] = A_0[j]) \\
                    \lor &(\exists k)(\seen{k}{\idx} \land g_0^\at{k} \land A[j] = e_0^\at{k})\\
                    \end{array}\right)
}
%
\patternnote This pattern includes the case where the index of A is value-preserving but different from \idx.

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(\inbounds{A}{j} \impl A[j] = A_0[j] \lor \\
           &(\exists k)(1 \leq k < i \land B[k] > 0 \land A[j] = B[k]))
         \end{array}\right)\\
    &&~~~B[i] > 0 \rightarrow A[B[i]] := B[i]\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Exchange Pattern}

\pattern{
  An array variable is only modified in a single assignment,
  whose guard is unknown, at some unkown index, and it receives a value-preserving expression.
}{
  &g^? \rightarrow A[e^?] := e^\at{\idx}
}{
  &(\forall j)(\inbounds{A}{j} \impl A[j] = A_0[j] \lor (\exists k)(\seen{k}{\idx} \land A[j] = e_0^\at{k}))
}

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           &(\forall j)(\inbounds{A}{j} \impl A[j] = A_0[j] \lor \\
           &(\exists k)(1 \leq k < i \land A[j] = B_0[k]))
         \end{array}\right)\\
    &&~~~B[i/2] > 0 \rightarrow A[i/2] := B[i]\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Known Interchange Pattern}

\pattern{
  An array variable is modified in possibly more than one assignment,
  all of whose guards are unknown, at index \idx, and it receives in each
  its own value at some unknown index.
}{
  &g^? \rightarrow A[\idx] := A[e^?]\\
  &...\\
  &g^? \rightarrow A[\idx] := A[e^?]\\
}{
  &(\forall j)(\seen{j}{\idx} \impl (\exists k)(\inbounds{A}{k} \land A[j] = A_0[k])) \\
  \land&
  (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])
}

\patternnote Also for guard value-preserving.\\

\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant}:\left(\begin{array}{cc}
           (\forall j)(1 \leq j < i \impl (\exists k)(\inbounds{A}{k} \land A[j] = A_0[k]))\\
           \land (\forall j)(1 > j \land j \geq i \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
         \end{array}\right)\\
    &&~~~B[i] > 0 \rightarrow A[i] := A[i/2]\\
    &&~~~B[i] < 0 \rightarrow A[i] := A[i/2+1]\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\subsubsection*{Unknown Interchange Pattern}

\pattern{
  An array variable is modified in possibly more than one assignment,
  all of whose guards are unknown, at some unkown index, and it receives in each
  its own value at some unknown index.
}{
  &g^? \rightarrow A[e^?] := A[e^?]\\
  &...\\
  &g^? \rightarrow A[e^?] := A[e^?]\\
}{
  &(\forall j)(\inbounds{A}{j} \impl (\exists k)(\inbounds{A}{k} \land A[j] = A_0[k]))\\
}

\patternnote Also for guard value-preserving and index in right-hand-side value-preserving.\\

\noindent
\patternexample
  \begin{eqnarray*}
    &&\KWloop \KWover i \KWin 1~..~N \\
    &&~~~\textit{invariant} :~ (\forall j)(\inbounds{A}{k} \impl (\exists k)(\inbounds{A}{k} \land A[j] = A_0[k]))\\
    &&~~~B[i] > 0 \rightarrow A[i\%3] := A[A[i]]\\
    &&~~~B[i] < 0 \rightarrow A[i\%3] := A[-A[y]]\\
    &&\KWend
  \end{eqnarray*}

\begin{theorem}
  \Inv{\idx} given by \curinv captures pattern \curpattern.
\end{theorem}

\begin{proof}
 TODO
\end{proof}

%==================================================================================
%==================================================================================
\ifdefined\longversion
\section{Pre-Transformation Tactic}
When our code fall into the above patterns nothing to do, just apply the corresponding invariant patterns.
Contrariwise, in some cases we will need a pre-processing them to bring into our patterns.
This pre-processing mainly to reorganize our code in order to transform the expression
which used others variables updates in the loop to a \textit{value-preserving expression}
define in section~\ref{sec:naming-conventions}. For example in the following code

$$\begin{array}{l}
  \KWloop \KWover i \KWin 1 .. N \\
  ~~~~ True \rightarrow A[i] := B[Index]\\
  ~~~~ True \rightarrow Index := Index + 1\\
  \KWend
\end{array}$$

The last statement is Certain Single Add-Up Pattern but the first statement is not Certain Single Map Pattern
because $B[Index]$ use a update variable $Index$ (therefore it's not value-preserving expression).
If we transform it as below we have Certain Single Map Pattern and Certain Single Add-Up Pattern.
Thus, the full invariant is the conjonction of the two corresponding invariants.

$$\begin{array}{l}
  \KWloop \KWover i \KWin 1 .. N \\
  ~~~~ True \rightarrow A[i]   := B[Index0 + I-1]\\
  ~~~~ True \rightarrow Index := Index + 1\\
  \KWend
\end{array}$$
%
\loopinvariant
%
\begin{eqnarray*}
&(\forall j)(\seen{j}{\idx} \impl A[j] = B_0[Index0 + j-1]) \\
\land& (\forall j)(\neg \seen{j}{\idx} \land \inbounds{A}{j} \impl A[j] = A_0[j])\\
&\land& \\
&Index = Index_0 + 1 * (i-1)&
\end{eqnarray*}

%==================================================================================
%==================================================================================

\subsubsection*{Example}
From a sequential program (return the string corresponding to hexadecimal format)
extracted in SPARK project ~\cite{sparkskein:url}
\begin{lstlisting}
subtype String_6_Index is Positive range 1 .. 6;
subtype String_6 is String (String_6_Index);
\end{lstlisting}

\begin{lstlisting}
function T0_Image (T0 : in U64) return String_6
is
   Result : String_6 := "000000";
   C : String(1 .. 20); --enough for"16#aabbccddeeffgghh#"
   LSB_Index : Positive := 19;
begin
   U64_IO.Put (C, T0, 16);
   for I in reverse String_6_Index loop
      Result (I) := C (LSB_Index);
      LSB_Index := LSB_Index - 1;
      exit when C (LSB_Index) = '#';
   end loop;
   return Result;
end T0_Image;
\end{lstlisting}

we extract the loop and translate \footnote{The translation from sequential loop to our
loop form will be futur works} it to our loop form which must respects the different
restrictions imposed.
$$\begin{array}{l}
  \KWloop \KWover \idx \KWin 1 .. 6 ~ \KWexit ~ \neg (C (19-(\idx-1) = '\#') ~ \KWdo \\
  ~~~~ < \textrm{\Inv{\idx} of the patterns identified here} >\\
  ~~~~ \mathit{true} \rightarrow Result (\idx) := C (19-(\idx-1))\\
  ~~~~ \mathit{true} \rightarrow LSB\_Index := 19 - (\idx-1)\\
  \KWend
\end{array}$$
\fi

\bibliographystyle{abbrv}
\bibliography{loop_patterns}
\end{document}