The Ivy language
Ivy’s language is designed to let you to specify and implement systems in a way that is both convenient and conducive to automated verification. Technically, this means that important verification problems like invariant checking and bounded model checking fall within a decidable fragment of firstorder logic.
For this reason, the Ivy language has certain unusual features. Ivy divides the world into three categories of things:
 Data values,
 Function values and
 Procedures.
Data values are the kinds of things that can be printed out, stored in files, transmitted over the internet and so on. These are sometimes refered to as POD types for “plain old data”. Function values are pure mathematical functions. They can be evaluated on arguments to produce deterministic results, and they have no side effects. In other words, evaluating a function does not modify the value of any variable. On the other hand, a procedure, when called, has an effect. In addition to returning values, it may also modify the values of variables.
Data values and function values can be stored in variables and passed as arguments. That is, data and functions are “first class” values. On the other hand, procedures cannot be stored in variables or passed as arguments.
A particularly unusual aspect of the Ivy language is that there are
no references. Two distinct variables are never “aliases” for the
same underlying “object”. Modifying variable a
never has an effect
on the value of variable b
. Ivy’s philosophy is that references are a
lowlevel optimization that should be used by compilers to avoid
copying, but should never appear in highlevel programs. The absense
of aliases enormously simplifies the analysis, testing and
verification of programs.
Another unusual aspect of the Ivy language is that it is synchronous. This means that:
 All actions occur in reaction to input from the environment, and
 all actions are isolated, that is, they appear to occur instantaneously, with no interruption.
This aspect of Ivy’s semantics greatly simplifies reasoning about concurrent and distributed systems.
We will now consider the basic elements of an Ivy program.
The language specifier
Every Ivy file begins with a line like the following:
#lang ivy1.7
This tells Ivy what version of the language we are using. This is important because in successive version of the language, certain features may be changed or deprecated. Providing the language version allows old programs to keep working. They current version of the Ivy language is 1.7. Changes between versions of the language are listed at the end of this document.
State and actions
An Ivy program describes objects that have state and provide actions that operate on state. State variables may hold either plain old data or mathematical relations and functions (much as in the Alloy language, but with important differences that we will discuss later).
Types and declarations
Suppose we have a network consisting of nodes, with pairwise links
between the nodes. We can model the structure of the network with a
relation link
like this:
type node
relation link(X:node,Y:node)
This says that node
is a POD type, but tells us nothing yet about
how values of type node
are represented. At this point, we say that
node
is an uninterpreted type. Further, we declared
that link
is a set of pairs (X,Y) where X and Y
are nodes.
In Ivy, as in Prolog, identifiers beginning with capital letters
are logical variables, or placeholders. These are not to be confused
with program variables, which hold the program state. The colons
introduce type annotations. In the above declaration, the variables
X and Y are just taking up space, telling us what sort of relation
link
is (that is, for every X and Y of type node
, link(X,Y)
is a Boolean value.
We could equivalently have written the relation declaration as:
function link(X:node,Y:node) : bool
Either way, we create a variable link
that holds a function value, in particular
a function from pairs of node
to bool
.
As another example, here is a declaration of a function that gives an ID to each node:
type id
function node_id(X:node) : id
A variable that holds just a node value can be declared like this:
individual root:node
Enumerated types
The type node
declared above is an uninterpreted type. This means
it can be any set with at least one element. Often it is useful to
define a type in extension, that is, by enumerating its elements
explicitly. An example of an enumerated type in Ivy would be:
type color = {red,green,blue}
This declares a type with exactly three distinct values, and also declares
individuals red
, green
and blue
as its elements.
Actions
An action is Ivy’s notion of a procedure that mutates the values of state variables. For example, here is a declaration of an action that adds a link between two nodes:
action connect(x:node, y:node) = {
link(x,y) := true
}
The action connect
is defined in terms of one of Ivy’s primitive
actions: an assignment. An assignment modifies the value of a
variable. In this case, the single pair (x,y) is added to the
relation link
(or put another way, the value of the expression
link(x,y)
is set to true, without otherwise modifying
link
). Because there is no aliasing in Ivy, the values of all other
variables remain unchanged by the assignment.
We can use placeholders to make larger modifications to a relation. For example, here is an action that removes all links from a given node x:
action clear(x:node) = {
link(x,Y) := false
}
The effect of the assignment with variable Y is to simultaneously
assign link(x,Y)
for all nodes Y. We don’t have to give a type
annotation for Y because it can be inferred from context.
We can be a little more selective by giving a Boolean expression in
the assignment. For example, this action removes links from x to all
nodes in the set failed
:
action clear_failed(x:node) = {
link(x,Y) := link(x,Y) & ~failed(Y)
}
If there are no parameters, we don’t use parentheses. For example:
action flip = {
bit := ~bit
}
In fact, you will never see a pair of empty parentheses in IVY. An action can also have return parameters. For example:
action swap(a:t,b:t) returns (c:t,d:t) = {
c := b;
d := a
}
Control
Sequential execution
We can execute two actions sequentially by separating them with semicolon. For example, this action removes all links from x, then links x to y:
action connect_unique(x:node, y:node) = {
link(x,Y) := false;
link(x,y) := true
}
The semicolon is a sequential composition operator in Ivy, not a
statement terminator. However, an extra semicolon is allowed before an
ending brace }
to make editing sequences of statements easier. In
this case, we could have written the sequence of two assignments
equivalently as:
link(x,Y) := Y = y
Calling actions
We could also have written connect_unique
by calling clear
and connect
:
action connect_unique(a:node, b:node) = {
call clear(a);
call connect(a,b)
}
Ivy uses the
callbyvalue convention. That is, when we call clear(a)
a
local variable x is created during the execution of clear
and
assigned the value a. This means that, as in the C programming
language, modifying the value of x in clear
would not result
in modifying the value of a in connect_unique
.
The return values of an action can be obtained like this:
call x,y := swap(x,y)
An action with a single return value can be called within an expression.
For example, if sqrt
is an action, then:
x := y + sqrt(z)
is equivalent to
call temp := sqrt(z)
x := y + temp
If there is more than one call within an expression, the calls are executed in lefttoright order. Calls inside conditional operators occur whether or not the condition is true. For example, the statement:
x := sqrt(y) if c else z
is equivalent to:
call temp := sqrt(y);
x := temp if c else z
Parentheses are not used when calling an action with no parameters. For example, if we have:
action next returns (val:t) = {
current := current + 1;
val := current
}
then we would write:
x := y + next
The lack of parentheses introduces no ambiguity, since the action
next
is not a value and cannot itself be passed as an argument to
the function +
. An advantage of this convention is that we don’t have
to remember whether next
is an action or a variable, and we can
easily replace a variable by an action without modifying all references
to the variable.
Conditionals
Conditionals in Ivy are much as in any procedural programming language. For example, the following code clears the incoming links to node y if y is in the failed set:
if failed(y) {
link(X,y) := false
}
The curly brackets around the assignment are required. No parentheses are need around the condition. A conditional can have an associated else clause, for example:
if failed(y) {
link(X,y) := false
} else {
link(y,z) := true
}
Because brackets are required, there is no ambiguity as to which ‘if’ an ‘else’ belongs to.
The following syntax can be used to find a element of a type that satisfies some condition:
if some x:t. f(x) = y {
z := x + y
}
else {
z := y
}
Here, if there is any value x
of type t
such that f(x) = y
, then
such a value is assigned to x
and the assignment z := x + y
is
executed. If there is more than one such value, the choice is
nondeterministic. If there is no such value, the else
clause is
executed. The symbol x
is only in scope in the if
clause. It acts
like a local variable and is distinct from any x
declared in an
outer scope.
It is also possible to choose a value of x
minimizing some function
of x
. For example, we can find an element of a set s
with the least key like this:
if some x:t. s(x) minimizing key(x) {
...
}
This is logically equivalent to the following:
if some x:t. s(x) & ~exists Y. s(Y) & key(Y) < key(x) {
...
}
Besides being more concise, the minimizing
syntax can be more
efficiently compiled and is easier for Ivy to reason about (see the
decidability discussion). The keyword
maximizing
produces the same result with the direction of <
reversed.
Loops
Loops are discouraged in Ivy. Often, the effect of a loop can be
described using an assignment or an if some
conditional.
For example, instead of something like this:
for y in type {
link(x,y) := false
}
we can write this:
link(x,Y) := false
When a loop is needed, it can be written like this:
sum := 0;
i := x;
while i > 0
{
sum := sum + f(i);
i := i  1
}
This loop computes the sum of f(i)
for i
in the range (0,x]
.
A loop can be decorated with a invariants, like this:
while i > 0
invariant sum >= 0
{
sum := sum + f(i);
i := i  1
}
The invariant sum >= 0
is a special assertion that is applied
on each loop iteration, before the evaluation of the condition.
Invariants are helpful in proving properties of programs with loops.
In some situations we need to guarantee that a loop always terminates. We can do this
with ranking function that is supplied by the keyword decreases
, like this:
while i > 0
invariant sum >= 0
decreases i
{
sum := sum + f(i);
i := i  1
}
The argument of decreases
is an expression whose value must decrease
with every loop iteration and such that the loop is never entered when
the expression is less than 0
.
Nondeterministic choice
The asterisk “*” can be used to represent nondeterministic choice in Ivy in two situations. First, on the righthand side of an assignment:
x := *
This cause x to be assigned nondeterministically to any value of its type. We can use variables in nondeterministic assignments, so for example:
link(x,Y) := *
causes x to be linked to an arbitrary set of nodes.
Further, we can use an asterisk in a conditional to create a nondeterministic branch:
if * {
link(x,y) := true
} else {
link(x,z) := true
}
Nondeterministic choice also occurs when we create a local variable (see below). On entry to an action the values of return parameters are nondeterministically chosen.
Expressions
Expressions in Ivy are terms or formulas in firstorder logic
with equality. Ivy provides the following builtin operators: ~
(not), &
(and), 
(or), >
(implies), <>
(iff) =
(equality). There is also a builtin conditional operator X if C else
Y
that returns X
if the Boolean condition C
is true and Y
otherwise. The if/else operator binds most strongly, followed by
equality, not, and, or. The weakest binding operators are <>
and
>
, which have equal precedence.
The binary and ternary operators are leftassociating (i.e., they bind
more strongly on the left). For example, x if p else y if q else z
is equivalent to (x if p else y) if q else z
and p > q > r
is
equivalent to (p > q) > r
. Warning: in the case of if/else and
>
, this is nonstandard and is due to an error in the parser. This
will change in a future version of the language. In the interim it is
best to always parenthesize expressions with multiple uses if if/else
and >
.
Expressions may also use logical quantifiers. For example, this formula says that there exists a node X such that for every node Y, X is linked to Y:
exists X. forall Y. link(X,Y)
In this case, the variables do not need type annotations, since we can infer that both X and Y are nodes. However, in some cases, annotations are needed. For example, this is a statement of the transitivity of equality:
forall X,Y,Z. X=Y & Y=Z > X=Y
We can determine from this expression that X, Y and Z must all be of the same type, but not what that type is. This means we have to annotate at least one variable, like this:
forall X:node,Y,Z. X=Y & Y=Z > X=Y
Assume, require and ensure
The primitive actions require
and ensure
allow us to write
specifications. These actions fail if the associated condition
is false. For example, suppose we wish the connect
action to handle
only the case where the node y is not in the failed set. We could
write
action connect(x:node, y:node) = {
require ~failed(y);
link(x,y) := true
}
If the condition ~failed(y)
is true, control passes through the
require
and this action behaves in the same way as the original. If
the condition ~failed(y)
is false, however, the require
action
fails. This means that whenever we use connect
we must prove that
the y argument is not in the failed set.
The ensure
action is similar, except it is the responsibility of the action
itself to ensure the truth of the formula. For example:
action increment(x:node) returns (y:node) = {
y := x + 1;
ensure y > x
}
The semantics of require
and ensure
are the same, except for the
assignment of blame when they fail. With require
, the onus of
guaranteeing the truth of the formula falls on the action’s caller,
while with ensure
it falls on the action itself. We will refer to
require
and ensure
actions collectively as assertions.
On the other hand, the assume
action does not allow control to pass
through if the associated condition is false. A typical application of
assume
is to make a temporary modeling assumption that we wish later
to remove. For example, this action nondeterministically chooses a
nonfailed node and connects x to it:
action connect_non_failed(x:node) = {
y := *;
assume ~failed(y);
link(x,y) := true
}
Of course, if all the nodes are failed, this action cannot
terminate. There is some degree of risk in using assumptions when
modeling, since assumptions can eliminate behaviors in unexpected
ways. Ideally, a finished program will not contain any occurrence of
assume
.
In require
, ensure
and assume
actions, any free variables are treated
as universally quantified. For example, if we want to connect x to a
node that is not currently linked to any node, we could change the
assumption above to
assume ~link(y,Z)
Initialization
Normally, we expect a system to start in some welldefined state, or
at least for some specified conditions to hold initially. In Ivy, we use an
after init
declaration for this purpose. For example:
after init {
link(X,Y) := false
}
This provides an action that executes at initialization, before the
environment calls any other actions. Multiple after init
actions are
executed in the order in which they are declared in the program.
Local variables
The above example of a guarded command action assumes that y is a
declared program variable of type node
. We can also declare y locally
within the action, like this:
action connect_non_failed(x:node) = {
var y:node;
assume ~failed(y);
link(x,y) := true
}
This creates a fresh y that is in scope only within the action (or generally to the end of the most tightly enclosing pair of brackets). We don’t need a nondeterministic assignment to y since the value of y is already nondeterministic at the point where it is declared. We can create a local variable and assign it in the same statement, like this:
var y:node := x
or, if the type of y
can be inferred, just this:
var y := x
Modelling interleaving concurrency in Ivy
Actions in an Ivy program execute only in response to calls from the program’s environment. Ivy makes the synchronous hypothesis: when the environment calls an action, it waits for the action to complete before issuing another call. Put another way, Ivy actions appear to execute in zero time. At first blush, it might seem that this eliminates the possibility of concurrency. In fact, the synchronous hypothesis is intended to make the implementation of concurrent and distributed systems simpler. The key idea is that only the appearance of synchronicity is required. In practice actions can execute concurrently, provided that to an outside observer they appear to have executed sequentially.
For now, we will leave aside the question of how to enforce the synchronous hypothesis in practice. Instead, we will consider how to use the synchronous IVY language to model a distributed protocol at an abstract level using interleaving concurrency. In an interleaving model, processes take turns executing actions in isolation (that is, in apparently zero time) in a nondeterministic order.
An Ivy program exports a set of actions to its environment. Each of these actions can be used to model a single isolated step of a process. Since the environment is allowed to call these actions in an arbitrary order, the Ivy program can be used to model arbitrary interleaving of process actions.
An abstract interface model
The following is a very abstract model of an interface that establishes connections between clients and servers. Each server has a semaphore that is used to guarantee that at any time at most one client can be connected to the server.
#lang ivy1.5
type client
type server
relation link(X:client, Y:server)
relation semaphore(X:server)
after init {
semaphore(W) := true;
link(X,Y) := false
}
action connect(x:client,y:server) = {
require semaphore(y);
link(x,y) := true;
semaphore(y) := false
}
action disconnect(x:client,y:server) = {
require link(x,y);
link(x,y) := false;
semaphore(y) := true
}
export connect
export disconnect
This program declares two types client
and server
. The state of
the protocol model consists of two relations. The relation link
tells us which clients are connected to which servers, while
semaphore
tells us which servers have their semaphore “up”. The
link
and semaphore
components aren’t “real”. They are abstractions
that represent the interface user’s view of the system.
The program exports two actions to the environment: connect
and
disconnect
. The connect
actions creates a link from client x
to
server y
, putting the server’s semaphore down. Notice that connect
requires that server’s semaphore be up on entry. The disconnect
action removes a link and puts the semaphore up. The two export
declarations at the end tell us that the environment may call
connect
and disconnect
in arbitrary sequence, though it must obey
the stated requirements.
Safety and invariants
A program is safe if it cannot fail, so long as in the past all requirements of the environment have been satisfied (that is, it is safe if any failure of the program can be blamed on the environment).
There are various ways to use assertions to specify desired safety properties of a program. A simple one is to add a test action that asserts some property of the program state. In the client/server example above, we might specify that no two distinct clients can be connected to a single server using the following test action:
action test = {
ensure ~(X ~= Z & link(X,Y) & link(Z,Y))
}
export test
The assertion is implicitly universally quantified over (distinct)
clients X
and Z
and server Y
. To help Ivy to prove that this
assertion always holds, we can suggest facts that might be useful in
constructing an inductive invariant. For example:
invariant X = Z  ~link(X,Y)  ~link(Z,Y)
invariant link(X,Y) > ~semaphore(Y)
Here, we state that no two clients are connected to the same server (which is just the property we want to prove) and additionally that when a client is connected to a server, its semaphore is down. These facts are inductive in the sense that they are initially true, and each of our three actions preserves them. Moreover, they are sufficient to guarantee that our test assertion is true. Thus, Ivy can use these invariants to prove safety of the program.
An invariant is asserted to hold at all times after initialization
when an exported action is not executing. In particular, the
invariant is not guaranteed to hold when the program calls back to the
environment (see import
below) or when it calls one of its own
actions.
Axioms and background theories
The builtin types and operators provided by Ivy are fairly
impoverished. We have only uninterpreted types, the Boolean type
bool
, enumerated types and the basic operators of firstorder
logic. This is by design. By introducing richer data types, or
theories, we would quickly make our verification problems
undecidable, meaning we would sacrifice reliability of automated
verification. In practice, before introducing, say, the integers into
a model, we should make sure that the power of the integers is really
needed. It may be, for example, that all we require is a totally
ordered set.
Ivy allows us to introduce background theories in the form of logical axioms. This in turn allows us to avoid using unnecessarily powerful theories. As an example, consider defining an ordering relation over our node ID’s:
relation (I:id < J:id)
This is an example of an infix symbol. The symbol <
is no
different than other relational symbols, except that Ivy predefines
it as having infix syntax.
We can ensure that <
is a total order by writing axioms:
axiom X:id < Y & Y < Z > X < Z
axiom ~(X:id < X)
axiom X:id < Y  X = Y  Y < X
These axioms say, respectively, that <
is
transitive,
antisymmetric
and total. As in other
cases, the free variables are universally quantified.
Of course, axioms are assumptions and assumptions are dangerous. We want to make sure that our axioms are consistent, that is, that they have at least one model. The Ivy tool can be helpful in determining this.
Overloaded operators.
In Ivy the equality operator is overloaded in the sense that it
applies to any pair of arguments so long as they are of the same
type. One way to think of this is that there is really a distinct
equality operator predeclared for each type, but that we use =
as a
shorthand for all of them. It is useful to be able to declare other
such overloaded operators to avoid, for example, having to invent a
new “less than” symbol for every ordered type, or adding type
annotations to operators.
Ivy provides for this in a limited way. Certain symbols, such as <
,
+
and 0
are always overloaded. This allows use the same symbol
with different type signatures disambiguate these uses based on type
inference.
To make type inference stronger, the overloaded operators also come
with type constraints. In functional language terms, <
has type
alpha * alpha > bool
and +
has type alpha * alpha > alpha
.
Numerals
Numerals are a special case of overloaded symbols. A numeral is any
symbol beginning with a digit, for example 0
, or 0xdeadbeef
. The
types of numerals are inferred from context. For example, if x
has
type foo
, then in the expression x+1
, the numeral 1
is inferred
to have type foo
.
Numerals are special symbols in the sense that they do not have to be
explicitly declared. However, Ivy gives them no special
interpretation. Ivy does not even assume that distinct numerals have
distinct values. This means that 0 = 2
is not necessarily false. In
fact, this equation might be true in a type representing the integers
mod 2.
Section [Interpretations] describes how to give concrete
interpretations to Ivy types, so that symbols like +
and 0
have
specific meanings.
Quoted symbols
A quoted symbol is a possiblyempty sequence of characters enclosed in
double quote characters (and not containing a double quote character).
An example would be "ab$c"
. Quoted symbols are similar to numerals:
their type is inferred from context.
Modules
A module in Ivy is a group of declarations that can be instantiated. In this way it is similar to a template class in an objectoriented programming language. Besides defining classes of objects, modules can be used to capture a reusable theory, or structure a modular proof.
Here is a simple example of a module representing an up/down counter with a test for zero:
module counter(t) = {
individual val : t
after init {
val := 0
}
action up = {
val := val + 1
}
action down = {
val := val  1
}
action is_zero returns(z : bool) = {
z := (val = 0)
}
}
This module takes a single parameter t
which is the type of the
counter value val
. We can create an instance of the module like this:
type foo
instance c : counter(foo)
This creates an object c
with members c.val
, c.up
, c.down
and c.is_zero
.
Any Ivy declaration can be contained in a module. This includes axioms, invariants, instances and modules. As an example, here is a module representing a theory of partial orders:
module po(t,lt) = {
axiom lt(X:t,Y) & lt(Y,Z) > lt(X,Z)
axiom ~(lt(X:t,Y) & lt(Y,X))
}
This module takes a type t
and a relation lt
over t
. It provides
axioms stating that lt
is transitive and antisymmetric. We might instantiate it
like this:
type foo
instantiate po(foo,<)
Since we didn’t give an object name, the members of po
are created
within the current object (which in this case is the global
object). Notice that we passed the overloaded infix symbol <
as a
parameter. Any symbol representing a type, function, relation, action
or object can be passed as a module parameter.
Like a class in an objectoriented programming language, a module can contain references to symbols declared outside the module. However, a declaration inside the module takes precedence. For example, consider this code:
relation r,s
module m = {
relation r
axiom s > r
}
instance c : m
The axiom in c
is equivalent to:
axiom s > c.r
That is, the local declaration of r
shadows the global one.
Singleton objects
We can create a module with just one instance like this:
object foo = {
relation bit
after init {
bit := false
}
action flip = {
bit := ~bit
}
}
This creates a single object foo
with members foo.bit
and
foo.flip
, exactly as if we had created a module and instantiated it
once.
This
The special symbol this
refers to the innermost surrounding object
or module. For example:
object foo = {
relation bit
after init {
this.bit := false
}
}
Here this.bit
refers to foo.bit
. In the outermost scope this
refers to the root object, which contains the entire program.
Type objects
A type may have the same name as an object. This makes it possible to define types with traits. For example:
object num = {
type this
function next(N:this) : this
function plus(X:this,Y:this) : this
}
This declares a type num
and also a function num.next
from type
num
to type num
and am function plus
that takes two arguments of type num
and returns a num
. The function num.next
can be applied using
a special syntax. That is, if x
is of type num
, then the expression
x.next
is a shorthand for num.next(x)
. Similarly, x.plus(y)
is a shorthand
for num.next(x,y)
. Actions can similary be traits of types. For example:
object num = {
type this
action plus(x:this,y:this) returns (z:this) = {
z := x + y;
}
}
In this case, x.plus(y)
is a shorthand for the action call num.plus(x,y)
.
Parameterized objects
An array of instances of the same module can be created like this:
type foo
type bar
instance c(X:bar) : counter(foo)
This creates one instance c(X)
of module counter
for for every
element of type bar
. Since we haven’t said how many elements there
are in type bar
, we have effectively created a collection of objects
of arbitrary but fixed size.
If x
is of type bar
, we can treat c(x)
as we would any object,
for example:
call c(x).down;
if c(x).is_zero {
call c(x).up
}
The parameter X
can also be passed to the module being instantiated.
This is useful to create a collection of objects with unique identifiers.
For example:
type id_t
module thing(id) = {
action my_id returns (x:id_t) = {
x := id
}
}
instance c(X:id_t) : thing(X)
In this case, calling c(id).my_id
will return id
.
An alternative way to write the above would be:
type id_t
object c(id:id_t) = {
action my_id returns (x:id_t) = {
x := id
}
}
Notice that the object parameter is given as a logical constant rather than a placeholder. This constant can be referred to in the body of the object.
Types in Ivy are never parameterized. For example, if we write:
object foo(self:t) = {
type t
}
this creates a single type called foo.t
, not a collection of types
foo.t(self)
for all values of self
.
Monitors
While embedding assertions in code is a useful way to write specifications, there are good reasons to separate a specification from the object being specified. For example, this allows you to reuse specifications, to construct modular proofs and to refine specifications into implementations.
The Ivy language supports these goals using monitors. A monitor is
an ordinary object, except that its actions are synchronized with the
actions of other objects. For example, suppose that in the
client/server example above, we want to specify that callers to
connect
do not request a connection to a server whose semaphore is
down. We could express this property as a monitor like this:
object mon = {
action pre_connect(x:client,y:server) = {
require semaphore(y)
}
execute pre_connect before connect
}
The execute
declaration says that whenever connect
is called,
action pre_connect
should be executed first, with the same
parameters. If any caller tries to connect a client to a busy server,
the assertion will fail. Notice we used require
here, so the
blame for the failure is on the caller of connect
.
Monitors can also check the return values of actions. For example:
action post_incr(inp:t) returns(out:t) = {
ensure inp < out
}
execute post_incr after incr
Here, we have an action incr
that is supposed to increment a value,
and we specify that the output must be greater than the input. Here,
we use ensure
, so the blame for any failure falls in the
implementation of action incr
.
As a shorthand, we can write our monitor action like this:
after c.post(inp:t) returns(out:t) {
ensure inp < out
}
This creates a monitor action called post.after
that is executed after c.post
.
Similarly, we can write:
before connect(x:client,y:server) {
require semaphore(y)
}
If we drop the input or output parameters, they are inherited from the monitored action. For example:
after c.post {
ensure inp < out
}
This is a useful shorthand when the declaration of c.post
is nearby,
but should probably be avoided otherwise.
We can write this:
around foo {
stmts1
...
stmts2
}
as a shorthand for this:
before foo {
stmts1
}
after foo {
stmts2
}
At present, local variables declared in stmts1
cannot be referenced
in stmts2
, but the intention is to make this possible, to reduce the
need to use old
in after monitors.
Monitor state
Usually, monitors contain state components that allow them to remember
some of the history of past events. For example, here is a monitor specifying a
property of counter
objects. It requires that immediately after a call to up
,
the is_zero
action cannot return true:
module counter_prop(c) = {
relation was_up
after init {
was_up := false
}
after c.up {
was_up := true
}
after c.down {
was_up := false
}
after c.is_zero returns (z:bool) {
ensure was_up > ~z
}
}
This module is parameterized on c
, the counter being specified. This
makes the specification reusable. It has a single state component
was_up
that remembers whether the last counting action was
up
. This is accomplished by the actions up
and down
that
synchronize with actions of counter c
(in this case it doesn’t make
any difference whether it is before or after). The action is_zero
executes after calls for the counter’s is_zero
action and asserts a
fact about the return value: if the last action was up
the result
cannot be true.
Action implementations
It is often useful to separate the declaration of an action from its implementation. We can declare an action like this:
action incr(x:t) returns(y:t)
and then give its implementation separately like this:
implement incr {
y := x + 1
}
Initializers
As noted above, an initializer is a special action that is executed once initially, before any exported actions are called. For example:
var bit : bool
after init {
bit := false
}
This behaves like a monitor after a special internal action called
init
. Initializers are executed once in the order they are declared.
Initializers may call other actions. For example, suppose we have a
module collection
representing a set of objects that is initially
empty. If we wanted a set that initially contained the value zero, we
could use an initializer like this:
type t
object foo = {
instance myset : collection(t)
after init {
call myset.add(0)
}
}
This action is called exactly once after myset
is initialized.
Parameterized objects can also have initializers. For example, we may want to have a collection of objects that each contain a bit, where initially only the bit of object 0 is true:
type t
object foo(self:t) = {
var bit : bool
after init {
bit := (self = 0)
}
}
There are some restrictions in initializers of parameterized objects, however. These are:

Conditions of
if
statements may not refer to the parameter, and 
In assignments, the lefthand side must contain the parameter if the righthand side does.
For example, this initializer would not be legal:
type t
var bit : bool
object foo(self:t) = {
after init {
bit := (self = 0)
}
}
This is because the component bit
being assigned is not
parameterized. This means it is in effect being assigned a different
value for each value of self
. The restrictions guarantee that the
result of the initializer does not depend on the order in which it is
called for different parameter values.
Definitions
We can define the value of a previously declared function like this:
function square(X:t):t
definition square(X) = X * X
Notice we don’t have to give the type of X in the definition, since it
can be inferred from the type of square
. Logically, the definition
is equivalent to writing:
axiom square(X) = X * X
However, definitions have several advantages. Primarily, they are safer,
since definitions are guaranteed to be consistent. In addition they can be
computed. If we use an axiom, the only way that Ivy can compile the
function square
is to compile a table of squares. On the other hand,
Ivy can compile the definition of square
into a procedure.
Ivy doesn’t (currently) allow recursive definitions. So, for example, this is not allowed:
definition factorial(X) = X * factorial(X1) if X > 0 else 1
Macro definitions
A macro is a definition that is only “unfolded” when it is used. For
example, let’s say we want to define a predicate rng
that is true of
all the elements in range of function f
. We could write it like
this:
definition rng(X) = exists Y. f(Y) = X
The corresponding axiom might be problematic, however. Writing it out with explicit quantifiers, we have:
axiom forall X. (rng(X) <> exists Y. f(Y) = X)
This formula has an alternation of quantifiers that might result in
verification conditions that Ivy can’t decide (see the
decidability discussion). Suppose though, that we only need
to know the truth value of rng
for some specific arguments. We can instead
write the definition like this:
definition rng(x:t) = exists Y. f(Y) = x
Notice that the argument of rng
is a constant x
, not a placeholder
X
. This definition acts like a macro (or an axiom schema) that can be
instantiated for specific values of x
. So, for example, if we have an assertion
to prove like this:
ensure rng(y)
Ivy will instantiate the definition like this:
axiom rng(y) <> exists Y. f(Y) = y
In fact, all instances of the macro will be alternationfree, since Ivy guarantees to instantiate the macro using only ground terms for the constant arguments. A macro can have both variables and constants as arguments. For example, consider this definition:
definition g(x,Y) = x < Y & exists Z. Z < x
Given a term g(f(a),b)
, Ivy will instantiate this macro as:
axiom g(f(a),Y) = f(a) < Y & exists Z. Z < f(a)
Choice functions
Suppose we want to define a function finv
that is
the inverse of function f
. We can write the definition like this:
definition finv(X) = some Y. f(Y) = X in Y
This special form of definition says that finv(X)
is Y
for some
Y
such that f(Y) = X
. If there is no such Y
, finv(X)
is left
undefined. The corresponding axiom is:
axiom forall X. ((exists Y. f(Y) = X) > f(finv(X)) = X)
With this definition, finv
is a function, but it isn’t fully
specified. If a given element Y
has two inverses, finv
will yield
one of them. This isn’t a nondeterministic choice, however. Since f
is a function, it will always yield the same inverse of any given
value Y
.
If we want to specify the value of finv
in case there is no inverse,
we can write the definition like this:
definition finv(X) = some Y. f(Y) = X in Y else 0
The else
part gives us this additional axiom:
axiom forall X. ((~exists Y. f(Y) = X) > finv(X) = 0)
Notice that this axiom contains a quantifier alternation. If this is a problem, we could use a macro instead:
definition finv(x) = some Y. f(Y) = x in Y else 0
The axiom we get is
axiom (~exists Y. f(Y) = x) > finv(x) = 0)
which is alternationfree.
Interpreted types and theories
The normal way of using Ivy is to declare uninterpreted types and to give the necessary axioms over those types to prove desired properties of a system. However, it is also possible in Ivy to associate types with sorts that are interpreted in the underlying theorem prover.
For example:
type idx
interpret idx > int
This says that Ivy type idx
should be interpreted using sort int
of the theorem prover. This does not mean that idx
is equated with
the integers. If we also interpret type num
with int
, we still
cannot compare values of type idx
and type num
. In effect, these
two types are treated as distinct copies of the integers.
When we declare idx
as int
, certain overloaded functions and
relations on idx
are also automatically interpreted by the
corresponding operators on integers, as are numerals of that
type. So, for example, +
is interpreted as addition and <
as
‘less than’ in the theory of integers. Numerals are given their normal
interpretations in the theory, so 0:idx = 1:idx
would be false.
Concrete sorts that are currently available for interpreting Ivy types are:
 int: the integers
 nat: the nonnegative integers
 {X..Y}: the subrange of integers from X to Y inclusive
 {a,b,c}: an enumerated type
 bv[N]: bit vectors of length N, where N > 0
Arithmetic on nat
is saturating. That is, any operation that would yield
a neagtive number instead gives zero.
An arbitrary function or relation symbol can be interpreted. This is useful for symbols of the theory that have no predefined overloaded symbol in Ivy. For example:
type t
type s
function extract_lo(X:t) : s
interpret t > bv[8]
interpret s > bv[4]
interpret extract_lo > bfe[3][0]
Here bfe[3][0]
is the bit field extraction operator the takes the
low order 4 bits of a bit vector.
Parameters
A parameter is a value supplied by the environment before initialization. A parameter is declared like this:
parameter p : t
where p is the parameter name and t is the type. Parameters may be declared anywhere in the object hierarchy. Except for the fact that it is initialized by the environment, a parameter is identical to an individual. The manner in which parameters are supplied is dependent on the compiler. For example, if a program is compiled to an executable file, the parameter values are supplied on the command line. If it is compiled to a class in C++, parameters are supplied as arguments to the constructor. In either case, the order of parameters is the same as their order of declaration in the program.
Imported actions
An imported action is an action whose implementation is provided by the environment. For example:
action callback(x:nat) returns (y:nat)
import callback
or simply:
import action callback(x:nat) returns (y:nat)
Like any action, the imported action may be given preconditions and postconditions. For example:
before callback {
require x > 0;
}
after callback {
ensure y = x  1;
}
The require
in this case is guarantee for the program and an
assumption for the environment. Similarly, the ensure
is an
assumption for the program and a guarantee for the environment. The
environment is assumed to be noninterfering, that is, Ivy assumes
that the call to callback
has no visible side effect on the program.
An imported action may not be implemented by the program.
Assume/guarantee reasoning
Ivy doesn’t require us to prove all at once that a program is safe. Instead, we can break the proof down into smaller proofs using the assume/guarantee approach.
For example, suppose we have the following program with two objects:
#lang ivy1.7
object num = {
type this
interpret this > nat
function even(X:this) = (X / 2 * 2 = X)
function odd(X:this) = ~even(X)
}
object evens = {
var number : num
after init {
number := 0
}
action step = {
call odds.put(number + 1)
}
action put(n:num) = {
number := n;
}
invariant number.even
}
object odds = {
var number : num
after init {
number := 1
}
action step = {
call evens.put(number + 1)
}
action put(n:num) = {
number := n;
}
invariant number.odd
}
export evens.step
export odds.step
Each object stores a natural number when its put
action is called
and sends this number plus one to the other object when its step
action is called by the environment. We want to prove the invariants
that evens.number
remains even, and odds.number
remains odd.
Moreover, we would like to prove these invariants by reasoning about
evens
and odds
in isolation. To do this, we use an
assume/guarantee specification.
Here is the evens
object with separate specification and implementation:
isolate evens = {
action step
action put(n:num)
specification {
before put {
require n.even
}
}
implementation {
var number : num
after init {
number := 0
}
implement step {
call odds.put(number + 1)
}
implement put(n:num) {
number := n;
}
invariant number.even
}
}
with odds,num
An isolate is a special kind of object that acts as a unit of
verification. It generally has three parts. It starts with a
declaration of the interface of the object. This usually consists of
types, functions and actions that are provided by the object. The next
section is the specification. This usually consists of variables,
properties and monitors that are visible outside the
isolate. Finally, we have the implementation. It usually consists
of variables, function definitions and action implementations that are
hidden. An isolate may depend on the visible parts of other objects.
This is declares using the keyword with
. In this case evens
depends on odds
and nat
.
The isolate for odds
is similar:
isolate odds = {
action step
action put(n:num)
specification {
before put {
require n.odd
}
}
implementation {
var number : num
after init {
number := 1
}
implement step {
call evens.put(number + 1)
}
implement put {
number := n;
}
invariant number.odd
}
}
with evens,num
Effectively, this breaks the proof that the two assertions always hold
into two parts. In the first part, we assume the object evens
gets
correct inputs and prove that it always sends correct outputs to
odds
. In the second part, we assume the object odds
gets correct
inputs and prove that it always sends correct outputs to evens
.
This argument seems circular on the surface. It isn’t, though, because when we prove one of the assertion holds, we are only assuming that the other assertion has always held in the past. So what we’re really proving is that neither of the two objects is the first to break the rules, and so the rules always hold.
In the first isolate, we prove the assertion that evens
guarantees. We do this using the visible part of odds
, but we forget
about the hidden state of the odds
object (in particular, the
variable odss.number
). To model the call to evens.put
in the
hidden part of odds
, Ivy exports evens.put
to the environment.
The requires
statement in the specification even.put
thus becomes a
guarantee of the environment. That is, each isolate only guarantees those assertions for
which it receives the blame. The rest are assumed.
When we verifiy isolate evens
, the result is as if we had actually entered the following program:
#lang ivy1.7
object nat {
...
}
object evens = {
var number : nat
after init {
number := 0
}
action step = {
call odds.put(number + 1)
}
action put(n:nat) = {
require even(nat)
number := n;
}
invariant number.even
}
object odds = {
action put(n:nat) = {
require odd(nat)
}
}
export evens.step
export evens.put
Notice the implementation of odds.put
has been eliminated, and what
remains is just the assertion that the input value is odd (Ivy
verifies that the eliminated side effect of odds.put
is in fact
invisible to evens
). The assertion that inputs to evens
are even
has in effect become an assumption. We can prove this isolate is safe
by showing that even.number
is invariantly even, which means that
odds.put
is always called with an odd number.
The other isolate, odds
, looks like this:
#lang ivy1.7
object nat {
...
}
object evens = {
action put(n:nat) = {
require even(nat)
}
}
object odds = {
var number : nat
after init {
number = 1
}
action step = {
call evens.put(number + 1)
}
action put(n:nat) = {
require odd(nat)
number := n;
}
invariant number.odd
}
export odds.step
export odds.put
If both of these isolates are safe, then we know that neither assertion is the first to fail, so the original program is safe.
The general rule is that a require
assertion is a guarantee for the
calling isolate and and assumption for the called isolate, while an ensure
action is
a guarantee for the called isolate and an assumption for the callinf isolate. When we
verify an isolate, we check only those assertions that are gurantees
for actions in the isolate.
Changes between Ivy language versions
New in version 1.2
 Keywords: returns, mixin, before, after, isolate, with, export, import, delegate, include
Deprecated in version 1.2
 Keywords: state, set, null, match
New in version 1.5
 Keywords: function, class, object, method, execute, destructor, some, maximizing, maximizing, private, implement, using, property, while, invariant, struct, definition, ghost, alias, trusted, this, var, attribute, scenario, proof, named, fresh
New in version 1.6
 Keywords: variant, of, globally, eventually, temporal
New in version 1.7
 Keywords: decreases, specification, implementation, require, ensure, around, parameter
 The
iterable
module is added the standard library fileorder
. This makes it possible to declare a type that is finite and iterable, and whose size is a parameter.  Due to an error, the
>
and<>
operators changed from rightassociating to leftassociating.
Deprecated in version 1.7
 The init declation (only ‘after init’ is now supported for initialization)