2.0.3 Specification logic

The properties of the inputs of the code analysed are given in a logic which is a restriction of the CSL logic defined in [Bouajjani and al. CONCUR-09]. This logic is a multi-sorted first order logic with reachability predicates. More precisely, in this logic one can use the following terms: it can express the following properties:

l[n]

the length of the heap segment stating from node n, i.e., the number of edges of the segment.

d[n]

the data stored in the node n.

S(n)

the sum of the data stored in the heap segment starting from node n except n itself is constrained by expr. We denote by S[n]=S(n)+d[n].

M[n]

the multiset of data stored in the heap segment starting from node n.

The atomic constraints of the logic are the following:

x(n)

variable x is labeling a node of a heap called n.

expr op 0 where op in \=,!=,<=,>=,!=,<,>\

linear constraints on terms

acyclic(x)

variable x labels a node from which starts a segment which is acyclic.

reach(x,y)

variable x labels a node from which starts a segment which reaches another node labeled by y.