Commit b71b8f52 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

logic: slight changes

parent af3ca9c5
...@@ -20,7 +20,7 @@ and symbolic heaps $\varphi$ is given by the following grammar: ...@@ -20,7 +20,7 @@ and symbolic heaps $\varphi$ is given by the following grammar:
\begin{array}{l l l r} \begin{array}{l l l r}
t & ::= x \mid n \mid t+t &\ \ \ & \mbox{terms} t & ::= x \mid n \mid t+t &\ \ \ & \mbox{terms}
\\ \\
\Pi & ::= t=t \mid t \ne t \mid t \leq t \mid t < t \mid \Pi \land \Pi &\ \ \ & \mbox{pure formulas} \Pi & ::= \top \mid \bot \mid t=t \mid t \ne t \mid t \leq t \mid t < t \mid \Pi \land \Pi &\ \ \ & \mbox{pure formulas}
\\ \\
\Sigma & ::= \emp \mid t \pto t \mid \blk(t, t) \mid \hls{}(t, t; t^\infty) \mid \Sigma \sepc \Sigma &\ \ \ & \mbox{spatial formulas} \Sigma & ::= \emp \mid t \pto t \mid \blk(t, t) \mid \hls{}(t, t; t^\infty) \mid \Sigma \sepc \Sigma &\ \ \ & \mbox{spatial formulas}
\\ \\
...@@ -42,7 +42,7 @@ the rules in Equations~(\ref{eq:hlsv-emp}) and (\ref{eq:hlsv-rec}), ...@@ -42,7 +42,7 @@ the rules in Equations~(\ref{eq:hlsv-emp}) and (\ref{eq:hlsv-rec}),
where $v$ is a variable interpreted over $\NN\cup\{\infty\}$. where $v$ is a variable interpreted over $\NN\cup\{\infty\}$.
%Here we assume that $c \ge 2$ since $x \pto x'-x \sepc \blk(x+1,x')$ occurs in the body of Rule~(\ref{eq:hlsv-rec}). %Here we assume that $c \ge 2$ since $x \pto x'-x \sepc \blk(x+1,x')$ occurs in the body of Rule~(\ref{eq:hlsv-rec}).
An atom $\hls{}(x,y;\infty)$ is also written $\hls{}(x,y)$; An atom $\hls{}(x,y;\infty)$ is also written $\hls{}(x,y)$;
$\top$ and $\bot$ are shorthands for $x=x$ and $x\ne x$ atoms.. %$\top$ and $\bot$ are shorthands for $x=x$ and $x\ne x$ atoms..
Whenever one of $\Pi$ or $\Sigma$ is empty, we omit the colon. Whenever one of $\Pi$ or $\Sigma$ is empty, we omit the colon.
We write $\fv(\varphi)$ for the set of free variables occurring in $\varphi$. We write $\fv(\varphi)$ for the set of free variables occurring in $\varphi$.
If $\varphi = \exists\vec{z}\cdot\Pi:\Sigma$, If $\varphi = \exists\vec{z}\cdot\Pi:\Sigma$,
...@@ -92,6 +92,7 @@ The satisfaction relation $s,h\models \varphi$, ...@@ -92,6 +92,7 @@ The satisfaction relation $s,h\models \varphi$,
where $s$ is a stack, $h$ a heap, and $\varphi$ a \slah\ formula, where $s$ is a stack, $h$ a heap, and $\varphi$ a \slah\ formula,
is defined by: % structural induction on $\varphi$ as follows: is defined by: % structural induction on $\varphi$ as follows:
\begin{itemize} \begin{itemize}
\item $s,h \models \top$ always and never $s,h \models \bot$,
\item $s,h \models t_1 \sim t_2$ iff \item $s,h \models t_1 \sim t_2$ iff
$s(t_1) \sim s(t_2)$, where $\sim\in\{=,\ne,\le,<\}$, $s(t_1) \sim s(t_2)$, where $\sim\in\{=,\ne,\le,<\}$,
% %
...@@ -138,7 +139,7 @@ $s,h \models \exists\vec{z}\cdot\Pi:\Sigma$ iff $\exists \vec{n}\in\NN^{|\vec{z ...@@ -138,7 +139,7 @@ $s,h \models \exists\vec{z}\cdot\Pi:\Sigma$ iff $\exists \vec{n}\in\NN^{|\vec{z
\end{definition} \end{definition}
%\vspace{-2mm} %\vspace{-2mm}
We write $A \models B$ for $A$ and $B$ sub-formula in \slah\ to mean We write $A \models B$ for $A$ and $B$ (sub-)formula in \slah\ to mean
that $A$ entails $B$, i.e., that for any model $(s,h)$ such that $s,h\models A$ that $A$ entails $B$, i.e., that for any model $(s,h)$ such that $s,h\models A$
then $s,h\models B$. then $s,h\models B$.
......
...@@ -186,7 +186,7 @@ By conjoining the pure part of $\texttt{path}_{\texttt{4-9}}$ with ...@@ -186,7 +186,7 @@ By conjoining the pure part of $\texttt{path}_{\texttt{4-9}}$ with
formulas $\texttt{pb}^\Sigma_{\texttt{4-9}}$ and formulas $\texttt{pb}^\Sigma_{\texttt{4-9}}$ and
$\texttt{pb}^\sepc_{\texttt{4-9}}$, $\texttt{pb}^\sepc_{\texttt{4-9}}$,
we obtain an equi-satisfiable existentially quantified {\PbA} formula we obtain an equi-satisfiable existentially quantified {\PbA} formula
whose satisfiability is NP-complete. whose satisfiability is a NP-complete problem.
\smallskip \smallskip
\noindent \noindent
......
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