certain nodes).

[${\rhd}$]{} We show that abstract rewriting with annotations is sound and, with additional assumptions, complete. Finally, we even derive strongest post-conditions for the case of graph rewriting with annotations.

*Related work:* The idea of shape graphs together with shape constraints was pioneered in [@srw:shape-analysis-3vl] where the constraints are specified in a three-valued logic. A similar approach was proposed in [@sww:abstract-gts], using first-order formulas as constraints. In partner abstraction [@b:partner-abstraction-thesis; @bw:partner-abstraction], cluster abstraction [@b:cluster-abstraction-thesis; @br:cluster-abstraction], and neighbourhood abstraction [@rz:neighbourhood-abstraction-groove] nodes are clustered according to local criteria, such as their neighbourhood and the resulting graph structures are enriched with counting constraints, similar to our constraints. The idea of counting multiplicities of nodes and edges is also found in canonical graph shapes [@r:canonical-graph-shapes]. The uniform treatment of monoid annotations was introduced in previous work [@k:ver-mobile; @ckn:graph-languages-type-graphs; @ckn:graph-languages-type-graphs-journal], in the context of type systems and with the aim of studying decidability and closure properties, but not for abstract rewriting.

Preliminaries {#sec:preliminaries}
=============

This paper presupposes familiarity with category theory and the topos structure of graphs. Some concepts (in particular elementary topoi, subobject and partial map classifiers, and slice categories) are defined in [App. \[apx:topos\]]{}. Furthermore all proofs can be found in [App. 