Failure

A postcondition says something about the effect of an entrypoint when the entrypoint does not fail. It is possible to specify situations when the entrypoint fails.

The goal is to generate one failure specification for every case the entrypoint fails.

Basics#

For example, the entrypoint set fails when the parameter value v is greater than 10, and fails with the pair v and the message "v must be below 10":

specification entry set(v : nat)
fails {
f1 with (x : nat * string):
(* specify failure object *)
x = (v, "v must be below 10") and
(* specify failure condition *)
v >= 10
}
}

Keyword fails introduces the section to declare specification of fail situations. In the example above the fail statment, is identified with id f1.

As illustrated above, the failure statement is the conjunction of:

  1. a statement to describe the object the entrypoint fails with
  2. a statement to specify the conditions that makes the entrypoint fail

The object the entrypoint fails with is usually a string message, but it can be more complex like for example a pair with the string message and a computed value used in the failure decision.

Archetype builtins#

note

This section describes specification features available from version 1.2.4 of Archetype.

The Archetype language provides several high-level syntaxes and builtins that may fail. This section presents how to specify their failure behavior.

Execution conditions#

called by <ADDRESS>
require {
r1 : <CONDITION>
}
failif {
f1 : <CONDITION>
}

Not found#

In the following, c is an asset collection, k is a key value and i is a nat.

c[k]
c.remove(k)
c.update(k, ...)

Out of bound#

c.nth(i)

Key exists#

c.add({ <ID> = k; ... })

Arithmetic#

a / b
a div b
a % b
n -= v