Database Operators

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.

previous:
Transactional Operators next:
Authorization Operators

Pact