Using the Verification Properties panel

Using the Verification Properties Panel

The Verification Properties Panel acts as an interface to define specific properties our contract must meet for it to be considered valid.

Four types of properties can be checked:

1. Action 1 cannot happen after Action 2
2. Action 1 can only happen after Action 2
3. If Action 1 happens, Action 2 can only happen after Action 3 happens
4. Action 1 will eventually happen after Action 2 happens

The actions are defined to be the transitions in the model editor.

To use this panel, add the properties by putting in the actions in their respective spots and clicking ADD. When the button is pressed, the properties are added into the Existing Properties category and more can be added afterward.

Note to add multiple actions into one sentence, the | operator can be used for “or” clauses.

Once these are all defined, the VerifyContract plugin can be used to verify the properties listed under Existing Properties

An empty verification properties panel looks like this:

Basing the examples of verifications below on this auction model:

Adding a Type 1 property:

Adding a Type 2 property that has an "or" example: