MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit fe631126 authored by Jean-Marie Madiot's avatar Jean-Marie Madiot
Browse files

renamed central invariant to I

parent 6607b5e3
......@@ -256,8 +256,8 @@ into its right-hand side.%
\footnote{%
$P \supd Q$ is defined as
$\forall\store.\;
P \star S\;\store \fupd Q \star S\;\store$,
where $S\;\store$ is the state interpretation invariant
P \star \centralinvariant\;\store \fupd Q \star \centralinvariant\;\store$,
where $\centralinvariant\;\store$ is the state interpretation invariant
(Definition~\ref{def:invariant}).
}
% LATER say more? explain that this update can be used only if the
......
......@@ -44,6 +44,8 @@
\newcommand{\rcvfpointedby}[1]{\mathrel{\mapsfrom}_{#1}}
\newcommand{\nmaster}{m}
\newcommand{\nv}{n}
% Central invariant
\newcommand{\centralinvariant}{I}
% Fonts.
\newcommand{\kw}[1]{\mathsf{#1}}
......
......@@ -285,7 +285,7 @@ The central invariant of \DIAMS,
or \emph{state interpretation invariant} \cite[\S7.3]{iris},
is the following Iris assertion:
\[
S\;\store \triangleq
\centralinvariant\;\store \triangleq
\exists\logicalstore. \left\{
\def\arraystretch{1.2}
\begin{array}{l@{\quad\star\quad}l@{\quad}l}
......@@ -335,12 +335,12 @@ S\;\store \triangleq
Let us try and explain the most important aspects of these definitions.
In Iris, the state interpretation invariant~$S\;\store$ is an assertion that
In Iris, the state interpretation invariant~$\centralinvariant\;\store$ is an assertion that
holds of the \emph{physical store}~$\store$ in between every two steps of
computation. It is used by Iris in the definition of Hoare triples; we inherit
this definition from Iris.
Our definition of $S\;\store$ begins with an existential quantification over
Our definition of $\centralinvariant\;\store$ begins with an existential quantification over
a \emph{\logical store}~$\logicalstore$.
%
The invariant records the fact that both stores are closed
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment