Temporal Specifications

Temporal specifications allow users to specify properties over arbitrary amounts of time. They are extremely useful for checking protocol behaviors amid unknown user interaction. A temporal specification is made up of several sections discussed below.

Variables

The variables section is an optional section that declares specification variables. They can be declared using the following syntax:

vars: type1 name1, type2 name2, ...

For more details, please see the page about specification variables.

Fairness

The fairness section is an optional section that defines a fairness property. Unlike a specification that checks if a particular temporal property holds, a fairness property requires that a temporal property holds. As such it is used to constrain the allowable behavior of the system and to enforce that specific behaviors occur. A fairness property can be declared as follows, where tprop is a temporal property:

fair: tprop

Specification

The specification section is a required section that defines the temporal property to check. It can be declared as follows, where tprop is a temporal property:

spec: tprop

Examples

Example 1

Whenever some user deposits X funds they can eventually withdraw Y funds where Y <= X

vars: address u, uint X
spec: [](finished(wallet.deposit, sender = u && value = X) ==>
      <> finished(wallet.withdraw(amt), sender = u && amt <= X))

Example 2

Note that the above specification has a trivial counterexample where the user does not ever attempt to perform a withdraw. We therefore need a fairness property that specifies that the user will always attempt to withdraw funds.

vars: address u, uint X
fair: []<> started(wallet.withdraw(amt), sender = u && amt <= X)
spec: [](finished(wallet.deposit, sender = u && value = X) ==>
      <> finished(wallet.withdraw(amt), sender = u && amt <= X))