Grammar clarifications, particularly \in and \subset

arrayslice.c

@@ -0,0 +1,13 @@
+//@ type seq = integer[];
+
+//@ logic seq init = { [ .. ] = 0 };
+
+//@ logic seq ident = { init \with [0 .. 10] = \lambda integer i; i };
+
+//@ lemma init_def: \forall integer i; init[i] == 0;
+
+//@ lemma ident_def1: \forall integer i; i < 0 ==> ident[i] == 0;
+
+//@ lemma ident_def2: \forall integer i; 0 <= i <= 10 ==> ident[i] == i;
+
+//@ lemma ident_def3: \forall integer i; i > 10 ==> ident[i] == 0;

higherorder.tex

@@ -1,7 +1,8 @@
 \begin{syntax}
 term ::= "\lambda" binders ";" term ; abstraction
-| ext-quantifier "(" term "," term "," term ")"
+| ext-quantifier "(" term "," term "," term ")";
+| { "{" term "\with" "[" range "]" "=" term "}" }; array slice update
 \
 ext-quantifier ::= "\max" | "\min" | "\sum";
                       | "\product" | "\numof"
-\end{syntax}
+\end{syntax}

loc.tex

@@ -1,11 +1,14 @@
 \begin{syntax}
+  range ::= term? ".." term? ;
+       \
   tset ::= "\empty" ; empty set
        | tset "->" id ;
        | tset "." id ;
        | "*" tset ;
        | "&" tset ;
        | tset "[" tset "]" ;
-       | term? ".." term? ; range
+       | tset "[" range "]" ;
+       | "(" range ")" ; a range as a set of integers
        | "\union" "(" tset ("," tset)* ")" ; union of locations
        | "\inter" "(" tset ("," tset)* ")" ; intersection
        | tset "+" tset ;

logic.tex

@@ -4,7 +4,7 @@
   logic-def ::= logic-const-def ;
           | logic-function-def ;
           | logic-predicate-def ;
-          | lemma-decl ;
+          | lemma-def ;
   \
   type-var ::= id
   \
@@ -35,6 +35,6 @@
   \
   parameter ::= type-expr id
   \
-  lemma-decl ::= "lemma" poly-id ":";
+  lemma-def ::= "lemma" poly-id ":";
                    pred ";"
 \end{syntax}

logicdecl.tex

@@ -8,7 +8,7 @@
   | logic-const-decl ;
   | logic-predicate-decl ;
   | logic-function-decl ;
-  | axiom-decl 
+  | axiom-def 
   \
   logic-type-decl ::= "type" logic-type ";" ;
   \
@@ -25,5 +25,5 @@
   "predicate";
   poly-id parameters? ";"
   \
-  axiom-decl ::= "axiom" poly-id ":" pred ";" 
-\end{syntax}
+  axiom-def ::= "axiom" poly-id ":" pred ";" 
+\end{syntax}

logiclabels.tex

@@ -1,5 +1,5 @@
 \begin{syntax}
   ident ::= id label-binders ; normal identifier with labels
   \
-  label-binders ::= "{" label-id (, label-id)* "}"
+  label-binders ::= "{" label-id (, label-id)* "}" ; label-id defined in Fig. \ref{fig:gram:at}
 \end{syntax}

logictypedecl.tex

@@ -16,7 +16,9 @@
     "(" type-expr;
     ("," type-expr)* ")" ; non-constant constructor
   \
-  type-expr ::= {"(" type-expr};
+  type-expr ::= product-type ; 
+  \
+  product-type ::= {"(" type-expr};
                 {("," type-expr)+ ")"} ; product type
   \
   term ::= {term "." id} ; record field access
@@ -39,4 +41,4 @@
     | "{" ("."id "=" pat)* "}" ; record pattern
     | "(" pat ( "," pat )* ")" ; tuple pattern
     | pat "as" id ; pattern binding
-\end{syntax}
+\end{syntax}

speclang_modern.tex

@@ -242,6 +242,7 @@ \subsection{Operators precedence}
 \label{fig:precedence}
 \end{figure}
 
+\paragraph{Conditional expressions and labels}
 There is a remaining ambiguity between the connective
 \lstinline|$\cdots$?$\cdots$:$\cdots$| and the labelling operator
 \lstinline|:|. Consider for instance the
@@ -251,6 +252,16 @@ \subsection{Operators precedence}
 Such a case must be considered as a syntax error, and should be fixed
 by explicitly adding parentheses.
 
+\paragraph{Labels and parsing}
+Note also that the use of labels can subtlely change the parsing of an
+expression, because labeled expressions have the least binding precedence.
+That is, once a label is seen, the parser finds the longest valid term or
+predicate following the label to consider as the labeled expression.
+For example, \lstinline|a && b ==> c && d| parses as 
+\lstinline|(a && b) ==> (c && d)|, but
+\lstinline|a && nm: b ==> c && d| parses as
+\lstinline|a && (nm: ( b ==> (c && d)))|.
+
 \subsection{Semantics}
 \label{sec:twovaluedlogic}
 
@@ -1264,6 +1275,18 @@ \subsection{Memory locations and sets of terms}
 \label{fig:gram:locations}
 \end{figure}
 
+\paragraph{Ranges}
+The \lstinline|..| syntax for ranges of integers has the appearance of a
+binary operator but is not a binary operator with conventional precedence,
+because either or both operand is optional.  
+A missing operand designates an
+open range, that is the range includes all integers in the negative (if the left operand is missing) or positive direction (if the right operand is missing).
+This range syntax is used only within parentheses to designate a set of 
+integers (cf. Fig. \ref{fig:gram:locations} later) or within square brackets to designate a 
+range of array indices, as shown in Figs.  \ref{fig:gram:term} and 
+\ref{fig:gram:locations}.
+
+\paragraph{Tsets}
 The grammar for tsets is given in
 Figure~\ref{fig:gram:locations}. The semantics is given below,
 where $s$ denotes any \textsl{tset}.
@@ -1303,6 +1326,7 @@ \subsection{Memory locations and sets of terms}
   satisfying predicate \lstinline|P|
   (binders \lstinline|b| are bound in both \lstinline|s| and \lstinline|P|).
 \item \lstinline|x \in s| holds if and only if \lstinline|x| is an element of \lstinline|s|.
+  The operator has the same precedence as relational predicates (e.g., \lstinline|<|).
 \item \lstinline|\subset(s$_1$,s$_2$)| holds if and only if each element
   of \lstinline|s$_1$| is also an element of \lstinline|s$_2$|
   (that is, \lstinline|s$_1$| is a subset of \lstinline|s$_2$|).
@@ -1647,11 +1671,11 @@ \subsubsection*{Default logic labels}\label{sec:default-logic-labels}
   all contracts, where it refers to the pre-state for the
   \lstinline|requires|, \lstinline|assumes|, \lstinline|assigns|,
   \lstinline|frees|,
-  \lstinline|variant|,
+  \lstinline|decreases|,
   \lstinline|terminates|
-  clauses and the post-state for other clauses
-  (\lstinline|ensures|, \lstinline|allocates|, and abrupt termination
-  clauses).
+  clauses and the post-state for 
+  \lstinline|ensures|, \lstinline|allocates|, and abrupt termination
+  clauses.
 It is also visible in data invariants, presented in Section~\ref{sec:invariants}.
 \item The label \lstinline|Old| is visible in \lstinline|assigns| and
   \lstinline|ensures| clauses of all contracts (both for functions and for
@@ -2218,6 +2242,33 @@ \subsection{Higher-order logic constructions}
   If \lstinline|i>j| then \lstinline|\sum| and \lstinline|\numof| above are 0,
   \lstinline|\product| is 1, and \lstinline|\max| and \lstinline|\min| are
   unspecified (see Section~\ref{sec:twovaluedlogic}).
+\item[Array slice update]
+  A term of the form
+  \lstinline|{ $a$ \with [ $low$ .. $up$ ] = $f$}| allows updating a slice of
+  an array. $a$ must be an array of $\tau$ and $f$
+  a unary function taking as argument
+  an \lstinline|integer| and returning a value of type $\tau$. Such a term
+  denotes an array $a'$ such that:
+  \[
+    a'[i] = \left\{\begin{array}{lr}
+                    a[i] & \mathrm{if~} i < low \\
+                    f(i) & \mathrm{if~} low \leq i \leq up \\
+                    a[i] & \mathrm{if~} i > up
+                    \end{array}\right.
+  \]
+If $low$ (resp. $up$) is missing, then all the lower (resp. upper) part of
+the array gets modified in $a'$. If both bounds are omitted, all elements of
+$a'$ are computed using $f$.
+
+As a special case, a term of the form
+\lstinline|{ $a$ \with [ $low$ .. $up$ ] = $v$}| where $v$ is a term of type
+$\tau$ is equivalent to
+\lstinline|{ $a$ \with [ $low$ .. $up$ ] = \lambda $\mathbb{Z}$. $v$ }|, i.e.
+it evaluates to an array where the relevant cells all contain the same
+value $v$.
+
+Finally, ranges can also be used in designated initializers
+(see section \ref{sec:aggregate}), with the same semantics as above.
 \end{description}
 
 
@@ -2227,6 +2278,12 @@ \subsection{Higher-order logic constructions}
   \listinginput{1}{sum.c}
 \end{example}
 
+\begin{example}
+  \label{ex:arraysliceupdate}
+  Properties of arrays initialized as a whole slice
+  \listinginput{1}{arrayslice.c}
+\end{example}
+
 \subsection{Concrete logic types}\label{sec:concrete-logic-types}
 \index{type!concrete}
 \experimental