SID Syntax

Attestor supports a limited fragment of symbolic heap separation logic with inductive predicate definitions to provide systems of inductive predicate definitions (SID), which are compiled into graph grammars.

The syntax of SIDs is given by the following grammar:

 SID ::= PREDICATE(PARAMETERS) <= FORMULA (<= FORMULA)* ;
 PARAMETERS ::= VAR{TYPE} | !VAR{TYPE} | PARAMTERS, PARAMTERS
 FORMULA ::= (EXISTENTIAL '|')? HEAP
 EXISTENTIAL ::= VAR{TYPE} | EXISTENTIAL, EXISTENTIAL
 HEAP ::= VAR.FIELD -> VAR | PREDICATE(VAR (, VAR)*) | HEAP * HEAP  

Here, PREDICATE refers to the name of a predicate symbol, which is a non-empty string of digits and letters. Similarly, VAR, TYPE, and FIELD refer to the name and type and selector of a variable. Free variables (left of <=) may additionally be declared as corresponding to reduction tentacles by adding a prefix !.