Database operators

table-written

(table-written t)

(table-written t)

• takes t: a
• produces bool
• where a is of type table or string

Whether a table is written in the function under analysis

Supported in properties only.

table-read

(table-read t)

(table-read t)

• takes t: a
• produces bool
• where a is of type table or string

Whether a table is read in the function under analysis

Supported in properties only.

cell-delta

(cell-delta t c r)

(cell-delta t c r)

• takes t: a
• takes c: b
• takes r: string
• produces c
• where a is of type table or string
• where b is of type column or string
• where c is of type integer or decimal

The difference in a cell's value before and after the transaction

Supported in properties only.

column-delta

(column-delta t c)

(column-delta t c)

• takes t: a
• takes c: b
• produces c
• where a is of type table or string
• where b is of type column or string
• where c is of type integer or decimal

The difference in a column's total summed value before and after the transaction

Supported in properties only.

column-written

(column-written t c)

(column-written t c)

• takes t: a
• takes c: b
• produces bool
• where a is of type table or string
• where b is of type column or string

Whether a column is written to in a transaction

Supported in properties only.

column-read

(column-read t c)

(column-read t c)

• takes t: a
• takes c: b
• produces bool
• where a is of type table or string
• where b is of type column or string

Whether a column is read from in a transaction

Supported in properties only.

row-read

(row-read t r)

(row-read t r)

• takes t: a
• takes r: string
• produces bool
• where a is of type table or string

Whether a row is read in the function under analysis

Supported in properties only.

row-written

(row-written t r)

(row-written t r)

• takes t: a
• takes r: string
• produces bool
• where a is of type table or string

Whether a row is written in the function under analysis

Supported in properties only.

row-read-count

(row-read-count t r)

(row-read-count t r)

• takes t: a
• takes r: string
• produces integer
• where a is of type table or string

The number of times a row is read during a transaction

Supported in properties only.

row-write-count

(row-write-count t r)

(row-write-count t r)

• takes t: a
• takes r: string
• produces integer
• where a is of type table or string

The number of times a row is written during a transaction

Supported in properties only.

row-exists

(row-exists t r time)

(row-exists t r time)

• takes t: a
• takes r: string
• takes time: one of after
• produces bool
• where a is of type table or string

Whether a row exists before or after a transaction

Supported in properties only.

read

(read t r)

(read t r)

• takes t: a
• takes r: string
• takes time: one of after
• produces object
• where a is of type table or string

The value of a read before or after a transaction

Supported in properties only.