2.3 Specification logic

The initial constraint on the program analysed is 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:

len[n]

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

data[n]

the data stored in the first element of the heap segment starting in the node n.

sum[n]

the sum of the data stored in the heap segment starting from node n except n itself.

mstl[n]

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

mshd[n]

is the term used to represent data[n] in the multiset constraints.

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 =,!=,<=,>=,!=,<,> is a 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.

disjoint(x,y)

variable x labels a node from which starts a segment which is disjoint from (does not share nodes with) the list segment which starting node is labeled by y.