Commit 149444e4 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

aplas: fix typos from atva

parent b3066f8e
......@@ -107,7 +107,9 @@ to obtain in polynomial time an equi-satisfiable {\qfpa} abstraction for a symbo
We introduce some notations first.
%
Given a formula $\varphi\equiv \Pi : \Sigma$,
$\atoms(\varphi)$ denotes the set of spatial atoms in $\Sigma$, and $\patoms(\varphi)$ denotes the set of predicate atoms in $\Sigma$.
$\atoms(\varphi)$ denotes the set of spatial atoms in $\Sigma$, and
$\patoms(\varphi)$ denotes the set of predicate atoms in $\Sigma$.
We also denote $\overline{\patoms}(\varphi)$ for $\atoms(\varphi)\setminus\patoms(\varphi)$.
\begin{definition}{(Presburger abstraction of \slah\ formula)}
Let $\varphi\equiv \Pi : \Sigma$ be a \slah\ formula.
......@@ -139,13 +141,13 @@ where
\quad (\atomtail(a_j) \le \atomhead(a_i)\lor \atomtail(a_i) \le \atomhead(a_j))
\end{array}
\\
\phi_2 & \triangleq & \bigwedge\limits_{a_i \in \patoms, a_j \not \in \patoms}
\phi_2 & \triangleq & \bigwedge\limits_{a_i \in \patoms(\varphi), a_j \in \overline{\patoms}(\varphi)}
\begin{array}[t]{l}
(\isnonemp_{a_i}) \limp \\
\quad (\atomtail(a_j) \le \atomhead(a_i) \lor \atomtail(a_i) \le \atomhead(a_j))
\end{array}
\\
\phi_3 & \triangleq & \bigwedge\limits_{a_i, a_j \not \in \patoms(\varphi), i < j}
\phi_3 & \triangleq & \bigwedge\limits_{a_i, a_j \in \overline{\patoms}(\varphi), i < j}
\atomtail(a_j) \le \atomhead(a_i) \lor \atomtail(a_i) \le \atomhead(a_j)
\end{eqnarray}
}
......
......@@ -61,7 +61,7 @@ The general case is dealt with in Section~\ref{ssec:ent-all};
%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,
%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,
%the the entailment $\varphi \models \psi$ does not hold.
In the sequel, we assume that $\abs(\varphi)$ is satisfiable and $\abs(\varphi) \models \abs(\psi)$. Otherwise, the entailment is trivially unsatisfiable.
In the sequel, we assume that $\abs(\varphi)$ is satisfiable and $\abs(\varphi) \models \abs(\psi)$. Otherwise, the entailment is trivially invalid.
\subsection{Decomposition into ordered entailments}
\label{ssec:order}
......
......@@ -139,7 +139,7 @@ $s,h \models \exists\vec{z}\cdot\Pi:\Sigma$ iff $\exists \vec{n}\in\NN^{|\vec{z
\end{definition}
%\vspace{-2mm}
We write $A \models B$ for $A$ and $B$ (sub-)formula in \slah\ for
We write $A \models B$ where $A$ and $B$ are (sub-)formula in \slah\ for
$A$ entails $B$, i.e.,
that for any model $(s,h)$ such that $s,h\models A$ then $s,h\models B$.
......
......@@ -177,7 +177,7 @@ when the heap it denotes is not empty
is
$(v=2 \land \exists k\cdot k > 0 \land 2k = y - x) \lor (2 < v \land 2 < y-x)$,
i.e., either all chunks have size 2 and the heap-list has an even size or
$v$ and the size of the heap-list are strictly greater than 2.
both $v$ and the size of the heap-list are strictly greater than 2.
For the empty case, the summary is trivially $x=y$.
%For $v=\infty$, the summary is $2 < y-x$.
The other spatial atoms $a$ (e.g., $x \pto v$ and $\blk(x,y)$)
......
......@@ -101,7 +101,7 @@
\newcommand \patoms {{\tt PAtoms}}
\newcommand \atoms {{\tt Atoms}}
\newcommand \atomhead {{\tt head}}
\newcommand \atomtail {{\tt tail}}
\newcommand \atomtail {{\tt next}}
\newcommand \vars {{\tt Vars}}
\newcommand{\addr}{\mathcal{A}}
......
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