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

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
  }
}

Entrypoint

archetype simple

variable value : nat = 0

entry set(v : nat) {
  if v < 10 then
    value := v
  else
    fail (v, "v must be below 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

Code

f1 with InvalidCaller(msg : string) :
  msg = "InvalidCaller" and
  caller <> <ADDRESS>

Specification

called by <ADDRESS>

Code

f1 with InvalidCondition(x : string * string) :
  x   = ("InvalidCondition", "r1") and
  not <CONDITION>

Specification

require {
  r1 : <CONDITION>
}

Code

f1 with InvalidCondition(x : string * string) :
  x = ("InvalidCondition", "f1") and
  <CONDITION>

Specification

failif {
  f1 : <CONDITION>
}

Not found

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

Code

f with NotFound(msg : string) :
  msg = "NotFound" and
  not c.contains(k)

Specification

c[k]

c.remove(k)

c.update(k, ...)

Out of bound

Code

f with OutOfBound(x : string * nat) :
  x   = ("OutOfBound", i) and
  c.count() < i

Specification

c.nth(i)

Key exists

Code

f with KeyExists(msg : string) :
  msg = "KeyExists" and
  c.contains(k)

Specification

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

Arithmetic

Code

f with DivByZero(msg : string) :
  msg = "DivByZero" and
  b = 0

Specification

a / b

a div b

a % b

Code

f with NatAssign(msg : string) :
  msg = "NatAssign" and
  n < v

Specification

n -= v