Index Syntax

In indexed mode, nonterminal edges can additionally be labelled with an index, which is composed of index symbols. Edges of heap configurations can either be labelled with a concrete or abstract index, while nonterminals on the left-hand side and nonterminal edges on the right-hand side of grammar rules can be labelled either with a concrete or instantiable index.

Indices are specified as a JSON-Array of Strings representing individual index symbols.

Types of Indices

Note on examples

The meaning of the index symbols depends entirely on the grammar manipulating them. In the examples of this section we are merely suggesting possible uses of indices.

Concrete Indices

A concrete index models a specific information for the nonterminal. It has the form

CONCRETE* BOTTOM

see CONCRETE and BOTTOM on how to specify the respective symbols in your input.

Examples

The information modeled by indices is typically a length information for a list, or a depth information for a tree. Assume s is a concrete symbol and Z a bottom symbol. Then List[ssZ] could model a list of length 2. Or Tree[Z] could modell a tree of depth 0, i.e. a leaf.

Here is how you would specify these indices in the input format:

"index":["s","s","Z"]

and

"index":["Z"]

Abstract Indices

An abstract index models relative information on the nonterminals. They have the form

CONCRETE* ABSTRACT

see CONCRETE and ABSTRACT on how to specify the respective symbols in your input.

Examples

Abstract indices are primarily used to store information on the relative length or depth of several lists or trees respectively. For this example let s be a concrete index symbol and X an abstract one. Then, List[ssX] and List[X] could model two lists where the first is exactly two elements longer then the other one.

Abstract indices can also be used to store information about the minimal size of an object. With the symbols from above Tree[ssX] could model a tree with depth at least 2.

Here is how you would specify these indices in the input format:

"index":["s","s","_X"]

and

"index":["_X"]

Instantiable Indices

An instantiable index can match several concrete or abstract indices with the same prefix. It has the form

CONCRETE* VARIABLE

see CONCRETE and VARIABLE on how to specify the respective symbols in your input.

Examples

Let s be a concrete index symbol, X an abstract one and () an index variable. The left hand side Tree[ss()] then matches for example Tree[ssZ], Tree[ssssssZ] or Tree[ssX]. However, it does not matches neither Tree[sZ] nor Tree[aaZ] nor List[ssZ]. It can also match Tree[X] if there is a suitable materialisation for X.

Here is how you would specify this index in the input format:

"index":["s","s","()"]

Index Symbols

Concrete Symbol

To tell ATTESTOR that a certain symbol in your input is meant to be a concrete (non-bottom) symbol, it has to start with a lower case letter.

Examples

The following are recognised as concrete symbols:

• s
• succ
• concreteSymbol

However, the next examples are not recognised as concrete symbols (in brackets what they would be taken for):

• S (bottom symbol)
• Succ (bottom symbol)
• _succ (abstract symbol)
• 1 (not accepted at all)

Bottom Symbol

Bottom symbols are indicated by starting with an upper case letter.

Examples

The following are recognised as bottom symbols:

• Z
• C
• Bottom

However, the next examples are not recognised as bottom symbols (in brackets what they would be taken for):

• z (concrete symbol)
• boTTom (concrete symbol)
• _Z (abstract symbol)
• 0 (not accepted at all)

Abstract Symbol

Abstract symbols are indicated by starting with an underscore. Note, that this underscore is omitted in output for readability.

Examples

The following are recognised as abstract symbols:

• _X
• _A
• _Abstract

However, the next examples are not recognised as bottom symbols (in brackets what they would be taken for):

• a (concrete symbol)
• Abstract (bottom symbol)
• X (bottom symbol)
• ? (not accepted at all)

Index Variable

The index variable is denoted by ().