Commit 18ed5364 authored by ehilin02's avatar ehilin02
Browse files

section 5

parent 85467b42
......@@ -86,10 +86,10 @@ Let $\varphi \equiv x < y: \hls{}(x, y; 3)$ and $s$ be a store such that $s(x)=
The following lemma (proved in the appendix) states that
the effective upper bounds of chunks in heap lists atoms of $\varphi$
with respect to stacks %\mihaela{r3: not clear}
can be captured by an {\EPbA} formula.
can be captured by a {\qfpa} formula.
\begin{lemma}\label{lem-eub}
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
\end{lemma}
The following lemma (proof in the appendix) provides the correct test used
......@@ -101,10 +101,11 @@ Then $\varphi \models_\preceq \psi$ iff
%$C_\preceq \wedge \abs(\varphi) \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$.
$C_\preceq \wedge \abs(\varphi) \models \forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$.
\end{lemma}
From Lemma~\ref{lem-hls-hls}, it follows that the entailment of
From Lemma~\ref{lem-hls-hls}, it follows that $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3) \models_\preceq \hls{}(t_1, t_2; t_3)$ is invalid iff $C_\preceq \wedge \abs(\varphi) \wedge \exists z.\ \xi_{eub, \varphi}(z) \wedge \neg z \le t_3$ is satisfiable, which is an {\EPbA} formula. Therefore, this special case of the ordered entailment problem is in coNP.
\medskip
%\vspace{-4mm}
\subsubsection{At least two atoms in the antecedent:} Recall that
\noindent {\bf At least two atoms in the antecedent:} Recall that
$\varphi\equiv C_\preceq \wedge \Pi: a_1 \sepc \cdots \sepc a_m$;
a case analysis on the form of the first atom of the antecedent, $a_1$, follows.
......
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