  We address the problem of reasoning on graph transformations featuring
actions such as \emph{addition} and \emph{deletion} of nodes and edges, node
\emph{merging} and \emph{cloning}, node or edge \emph{labelling} and edge
\emph{redirection}. First, we introduce the considered graph rewrite systems
which are parameterized by a given logic $\mathcal{L}$. Formulas of
$\mathcal{L}$ are used to label graph nodes and edges. In a second step, we
tackle the problem of formal verification of the considered rewrite systems by
using a Hoare-like weakest precondition calculus. It acts on triples of the
form $\{\texttt{Pre}\}(\texttt{R},\texttt{strategy}) \{\texttt{Post}\}$ where
\texttt{Pre} and \texttt{Post} are conditions specified in the given logic
$\mathcal{L}$, \texttt{R} is a graph rewrite system and \texttt{strategy} is an
expression stating how rules in \texttt{R} are to be performed. We prove that
the calculus we introduce is sound. Moreover, we show how the proposed
framework can be instantiated successfully with different logics. We
investigate first-order logic and several of its decidable fragments with a
particular focus on different dialects of description logic (DL). We also show,
by using bisimulation relations, that some DL fragments cannot be used due to
their lack of expressive power.
