mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
3323 lines
134 KiB
TeX
3323 lines
134 KiB
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}
|