Table of Contents


1. Introduction

1.1. The ABS Language

The ABS language is an actor-based, object-oriented, executable modeling language. Its prime features are:

Algebraic user-defined data types and side effect-free functions

All data (except the state of objects and future variables) is immutable, and functions are free of side effects. This makes understanding and reasoning about models easier.

User-defined data types are used for data modeling instead of objects, so ABS models are typically smaller than their Java counterparts.

A syntax that is close to Java.

Programmers that are used to Java can easily learn the ABS language.

Distributed, actor-based semantics

Method calls are asynchronous and create a new process in the target. Processes are scheduled cooperatively and run within the scope of one object. Futures are used to synchronize with and get the result of another process.

Interfaces for specifying object behavior

Similar to Java, the behavior of a class is defined by implementing zero or more interfaces with their corresponding methods.

Safe concurrency

Processes run cooperatively within one object and do not have access to other objects' state, and data structures are immutable. The most common error causes of concurrent systems (aliasing, insufficient locking) are avoided by the language semantics.

Distributed computing

The combination of asynchronous method calls, immutability and strong encapsulation makes it very easy to model distributed systems.

A formal semantics and compositional proof theory

ABS is designed to be amenable to program analysis and verification. A variety of tools (deadlock checker, resource analysis, formal verification) have been developed.


Languages are eco-systems, and a language containing all possible features will be easy to use for no one. The following areas are currently under-served by ABS:

Parallel computing

Algorithms relying on multiple processes operating on mutable state, e.g., from the domain of scientific computing, can only be expressed in roundabout ways.

Close-to-the-metal programming

ABS is not designed to be a systems programming language.

1.2. The ABS Actor and Concurrency Model

As mentioned, ABS method calls are asynchronous and create a new process in the target, while the caller process continues to run in parallel, as shown in Figure Process call semantics. At point ①, P1 issues an asynchronous call to some object residing on another cog. In response, a new process P2 is created; P1 and P2 can run in parallel. At point ②, P1 needs the result of the method call and suspends itself. At point ③, P2 finishes and returns a value. P1’s cog then reactivates P1 to continue execution.

Process call semantics
Figure 1. Process call semantics

The paragraph above elides some details. An asynchronous method call (see Asynchronous Call Expression) produces a future variable, which is used both to synchronize with the callee process (see Await Statement) and to get the result (see Get Expression). Future variables are first-class objects that can be passed along, so multiple processes can synchronize on the same future.

The processes created by method calls are scheduled cooperatively and run within the scope of the target object. Objects are grouped into COGs (Concurrent Object Groups). Each cog runs one process at a time, while processes on different cogs run in parallel, as shown in Figure Processes running inside their cogs. This means that each cog is a unit of concurrency and is in charge of scheduling the processes running on its objects. Each process runs until it suspends itself (see Await Statement and Unconditional Release: Suspend) or terminates, at which point the cog chooses the next process to run.

Processes running inside their cogs
Figure 2. Processes running inside their cogs

A new cog is created by creating an object with a new expression (see Figure Creating an object in a new cog).

Creating an object in a new cog
Figure 3. Creating an object in a new cog

An object in an existing cog is created via the new local expression (see Figure Creating an object in the same cog).

Creating an object in the same cog
Figure 4. Creating an object in the same cog

2. Lexical Structure

This section describes the lexical structure of the ABS language. We use the following EBNF conventions for specifying the syntax of ABS elements.

Table 1. EBNF syntax for this manual

typewriter text

Terminal symbols (occurring in program source code)


Non-terminals (production rule names)


Separator between left hand side and right hand side of a rule


Variant; either of the element(s) separated by |

[ ]

Optionals; the enclosed elements can be omitted

{ }

Repetition; zero or more occurrences of the enclosed elements

? ?

Special group (elements in the group are specified informally)

[: :]

A character class, as in extended regular expression syntax

( )


2.1. Line Terminators and White Spaces

Line terminators and white spaces are defined as in Java.


LineTerminator ::=

\n | \r | \r\n

WhiteSpace ::=

LineTerminator | | \t | Comment


ABS supports the two common Java-style styles of comments: end-of-line comments and block comments.

An end-of-line comment starts with two slashes, e.g., // text. All text that follows // until the end of the line is treated as a comment.


Comment ::=

LineComment | BlockComment

LineComment ::=

// { ? characters except LineTerminator ? } LineTerminator

BlockComment ::=

/* { ? characters except */ ? } */

// this is a comment
module A; // this is also a comment

A block comment is enclosed in /* */, e.g., /* this is a comment */. Block comments can span multiple lines and do not nest.

/* this
is a multiline
comment */

2.3. Identifiers

Identifiers consist of a letter followed by a sequence of letters, numbers and underscores (_).

ABS distinguishes identifiers and type identifiers. Identifiers start with a lower-case character, type identifiers start with an upper-case character. Identifiers name local variables, fields, methods and functions. Type identifiers name interfaces, classes, types, type constructors, deltas and products.

Identifiers can be qualified with a module name (see Modules) or simple (without module name prefix).


SimpleIdentifier ::=

[: lower :] { [: alpha :] | [: digit :] | _ }

SimpleTypeIdentifier ::=

[: upper :] { [: alpha :] | [: digit :] | _ }

QualifiedIdentifier ::=

{ SimpleTypeIdentifier . } SimpleIdentifier

QualifiedTypeIdentifier ::=

{ SimpleTypeIdentifier . } SimpleTypeIdentifier

Identifier ::=

SimpleIdentifier | QualifiedIdentifier

TypeIdentifier ::=

SimpleTypeIdentifier | QualifiedTypeIdentifier

2.4. Keywords

The following words are keywords in the ABS language and are invalid as identifiers.




































2.5. Literals

A literal is a textual representation of a value. ABS supports three kinds of literals, integer literals, string literals, and the null literal.

Strings are enclosed in double quotes ("). Line feed in a string is written as \n, carriage return as \r.

ABS does not support floating point numbers currently. Rational numbers are written using the division operator /, e.g., 1/4 for one quarter.

The null literal is written as null.


Literal ::=

IntLiteral | StringLiteral | ThisLiteral | NullLiteral

IntLiteral ::=

0 | ( ( 1 | …​ | 9] ) { [: digit :] } )

StringLiteral ::=

" { ? Valid String Character ? } "

ThisLiteral ::=


NullLiteral ::=


Valid string characters are defined as in the Java language.

2.6. Annotations

Annotations consist of a syntactically valid pure expression, optionally preceded by a type identifier (the “tag”) and a colon (:). They can be put in front of statements and definitions.


Annotation ::=

[ [ TypeIdentifier : ] PureExp ]

Annotations are used to write auxiliary information that can be used by various tools. Unknown (user-defined) annotations are ignored by the toolchain. Pre-defined annotations are usually type-checked.

[Near] class Example { ... }

This is an example of an annotation with a tag:

[Cost: 15] skip;

Annotations are associated with the following language construct. In the examples above, the first annotation pertains to the class definition of Example, the second annotation pertains to the skip statement.

There can be more than one annotation in one place.

In general, it is not an error to have more than one annotation with the same tag in the same place. However, some pre-defined annotations might forbid this.

3. Types

ABS has a static, nominal type system. Local variables, object fields, function parameters and method parameters are statically typed. A type name can refer to a algebraic data type, an interface, a type synonym. There are a number of pre-defined data types which are documented in Chapter The Standard Library.

A type name is a sequence of letters, digits and underscores (_) starting with an uppercase letter. In case of a parametric data type, the type name continues with a left angle (<), a list of type names separated by commas and ends with a right angle (>).


Type ::=

TypeIdentifier [ < Type { , Type } > ]

New types are defined as either interfaces or algebraic data types. Algebraic data types can be parametric, which is useful for defining “container-like” data types. Currently only algebraic data types can be parameterized, i.e., ABS does not currently offer class templates.

Note that classes are not types in ABS.

String (1)
A_s1mple_type (2)
Map<Int, List<String>> (3)
1 The type name is String. The string type is defined in the standard library.
2 This is a type name containing underscores and digits.
3 This type name denotes a map from integers to lists of strings.

3.1. Built-in Types

ABS offers the following built-in datatypes:

Table 2. ABS built-in types
Name Descrition Example


The empty (void) type



Boolean values

True, False


Integers of arbitrary size

0, -15


Rational numbers

1/5, 22/58775



"Hello world\n"




Int type is a subtype of Rat; this means that Int values are assignable to places of type Rat. Rational values can be converted to integers via the truncate function.

The future type Fut<A> is a special built-in type that denotes that an ABS value of type A will become available in the future. The value that a future holds and will return can be of any concrete type.

Fut<String> (1)
Fut<List<Rat>> (2)
1 This future will contain a value of type String
2 This future will contain a list of rational numbers

3.2. Algebraic Data Types

Algebraic Data Types in ABS are used to implement user-defined, immutable data values. Because values of algebraic data types are immutable, they can be safely passed on to other objects and cogs and make it easy to reason about program correctness.


DataTypeDecl ::=

data SimpleTypeIdentifier [ TypeParams ] [ = DataConstr { | DataConstr } ] ;

TypeParams ::=

< SimpleTypeIdentifier { , SimpleTypeIdentifier } >

DataConstr ::=

SimpleTypeIdentifier [ ( Type [ SimpleIdentifier ] { , Type [ SimpleIdentifier ] } ) ]

Data Type Constructors enumerate the possible values of a data type. Constructors can have zero or more arguments. Each argument can have an optional accessor function (see Accessor Functions).

data IntList = NoInt | ConsInt(Int head, IntList tail); (1)
data Bool = True | False; (2)
data NotInstantiable; (3)
1 The data type IntList has two constructors: NoInt and ConsInt. Both define an accessor function.
2 This is the definition of the built-in data type Bool.
3 This type does not have constructors and therefore cannot be instantiated.

Accessor Functions

Data constructor arguments can optionally have a name, which needs to be a valid identifier. If a name is given, it defines a function that, when passed a value expressed with the given constructor, return the argument.

The name of an accessor function must be unique in the module it is defined in. It is an error to have multiple accessor functions with the same name, or to have a function definition with the same name as an accessor function.

data Person = Person(String name, Int age);
  Person john = Person("John", 34);
  Int age = age(john); (1)
1 The call to age returns 34.

Parametric Data Types

Algebraic data types can carry type parameters. Data types with type parameters are called parametric data types.

Parametric Data Types are useful to define “container” data types, such as lists, sets or maps. Parametric data types are declared like normal data types but have an additional type parameter section inside broken brackets (< >) after the data type name.

data List<A> = Nil | Cons(A, List<A>);

When using a parametric data type, concrete types are given for the type parameters.

List<Int> l = Cons(1, Cons(2, Nil));

N-ary Constructors

Literal values of recursive data types like lists and sets can be arbitrarily long, and nested constructor expressions can become unwieldy. ABS provides a special syntax for n-ary constructors, which are transformed into constructor expressions via a user-supplied function.

def Set<A> set<A>(List<A> l) = (1)
    case l {
       Nil => EmptySet;
       Cons(x,xs) => insertElement(set(xs), x);

  Set<Int> s1 = set(Cons(1, Cons(2, Cons(3, Nil)))); (2)
  Set<Int> s = set[1, 2, 3]; (3)
1 The parametric function set is defined to take a list of elements and return a set.
2 set is called with a literal list constructed as normal.
3 set is called with the special n-ary constructor syntax. The two calls return the same value.

The constructor function usually has the same name as the type it is constructing. For example, a value of type Set is constructed via the function set.

Fully Abstract Data Types

Using the module system it is possible to define abstract data types. For an abstract data type, only the functions that operate on them are known to the client, but not its constructors. This can be easily realized in ABS by putting such a data type in its own module and by only exporting the data type and its functions, without exporting the constructors.

3.3. The Future Type

Futures are placeholders for return values of asynchronous methods calls.

Future values are produced by asynchronous method calls (see Asynchronous Call Expression). The current process can suspend itself until a future is resolved, i.e., until the return value of the asynchronous method call is available (see Await Statement). The get expression returns the value of a future (see Get Expression). In case the future is not yet resolved, the get expression blocks the current cog.

Fut<Int> f = o!add(2, 3); (1)
await f?; (2)
Int result = f.get; (3)
1 This statement defines a future variable f to hold the integer result of the method call to add.
2 The await statement suspends the current process until f is resolved.
3 The get expression returns the value computed by the add call.

Futures are first-class values that can be stored and passed around. In case only the return value of the method call is needed and not the future itself, a shorthand can be used that combines the above three statements:

Int result = await o!add(2, 3); (1)
1 This statement invokes add, suspends the current process until the result is available, then stores it in result.

3.4. The Exception Type

In higher-level programming languages, exceptions are generally used to signal an erroneous or abnormal runtime behaviour of the program, that should be treated (handled) separately compared to normal values.

The Exception type is a special built-in data type that looks similar to an Algebraic Data Type (immutable, no identity) but with a notable difference: the exception data type can be extended with new (user-provided) data constructors. Based on this fact, the user has the ability to, besides using the predefined exceptions of the ABS standard library, write arbitrary exceptions specific to the user’s program.

To define a new exception (data constructor) the user has to write:

exception MyException;

An exception can also take any number of arguments as:

exception AnotherException(Int, String, Bool);

In ABS, exceptions are first-class citizens of the language; the user can construct exception-values, assign them to variables or pass them in expressions. All these exception-values are typed by the type Exception . However, an exception-value can only acquire the special meaning of abnormal behaviour when the user explicitly says so with a throw keyword. We will visit the throw keyword together with how to recover from exceptions (catch keyword) in a later section.

Predefined exceptions in the Standard Library


Raised in arithmetic expressions when the divisor (denominator) is equal to 0, as in 3/0


The assert keyword was called with False as argument


The pattern matching was not complete. In other words all c catch-all clause


A method was called on a null object


The calling stack has reached its limit (system error)


The memory heap is full (system error)


The user pressed a key sequence to interrupt the running ABS program

3.5. Interface Types

Interfaces in ABS describe the functionality of objects. Thus, Interfaces in ABS are similar to interfaces in Java. Unlike Java, objects are only typed by interfaces and not by their class.

The syntax of interfaces is given in Interfaces.

3.6. Type Synonyms

A Type Synonym is an alternative type name for a type. Type synonyms are introduced with the keyword type. Parametric type synonyms are not currently supported.


TypeSynDecl ::=

type SimpleTypeIdentifier = Type ;

type Filename = String;
type Filenames = Set<Filename>;
type Servername = String;
type Packet = String;
type File = List<Packet>;
type Catalog = List<Pair<Servername,Filenames>>;

4. Expressions

This chapter specifies all ABS expressions. ABS expressions can either be side effect-free (i.e., part of the functional sublanguage) or have side effects.


Exp ::=

PureExp | EffExp

The functional sublanguage of ABS is a purely-functional, side effect-free language. It comprises functions and operators on built-in datatypes, user-defined algebraic datatypes, and user-defined functions defined on datatypes.

Additionally, ABS contains a number of special expressions with well-defined side effects, such as the new expression which creates a new object. Expressions with side effects cannot be combined with other expressions, for example as an argument to a function call. This slight notational inconvenience makes it easier to develop static analysis techniques and tools for ABS.

4.1. Pure Expressions

Pure Expressions are side effect-free expressions. The value of these expressions only depends on their arguments, and they can be evaluated multiple times without influencing the execution semantics.


PureExp ::=

SimpleIdentifier | this . SimpleIdentifier | this | null | Literal | LetExp | DataConstrExp | FnAppExp | FnAppListExp | IfExp | CaseExp | OperatorExp | ( PureExp )

Literal Expressions

Literals, as defined in Literals, are expressions.

Operator Expressions

ABS has a range of unary and binary operators working on pre-defined datatypes. All operators are pure (side effect-free).


OperatorExp ::=

UnaryExp | BinaryExp

UnaryExp ::=

UnaryOp PureExp

UnaryOp ::=

! | -

BinaryExp ::=

PureExp BinaryOp PureExp

BinaryOp ::=

|| | && | == | != | < | <= | > | >= | + | - | * | / | %

The following table describes the meaning as well as the associativity and the precedence of the different operators. The list is sorted from low precedence to high precedence.

Table 3. ABS Operators
Expression Meaning Associativity Argument types Result type

e1 || e2

logical or




e1 && e2

logical and




e1 == e2





e1 != e2





e1 < e2

less than




e1 <= e2

less than or equal to




e1 > e2

greater than




e1 >= e2

greater than or equal to




e1 + e2





e1 + e2





e1 - e2





e1 * e2





e1 / e2





e1 % e2






logical negation





integer negation




Semantics of Comparison Operators

ABS has generic equality and less-than comparison between two values of the same type.

Equality and inequality comparison is standard: by value for functional datatypes and by reference for objects and futures. I.e., two strings "Hello" compare as identical via ==, as do two sets containing identical values. Two references to objects or futures compare as identical via == if they point to the same object or future. The inequality operator != evaluates to True for any two values that compare to False under == and vice versa.

For the comparison operator <, an ordering is defined in the following way.

  • Numbers compare as usual.

  • Strings compare lexicographically.

  • Algebraic datatypes compare first by constructor name, then by comparing constructor arguments left to right.

Cons(_, _) < Nil
Cons(1, _) < Cons(2, _)
  • Objects and futures are compared by identity, in an implementation-specific but stable way. This means that for any two variables a and b that point to different objects, the value of a < b does not change as long as a and b are not re-assigned.[1]

The Let Expression

The expression let (T v) = p in b evalutes b, with v bound to the value of evaluating the expression p. The newly-introduced binding of v can shadow a binding of v outside of the let expression.


LetExp ::=

let ( Type SimpleIdentifier ) = PureExp in PureExp

let (Int x) = 2 + 2 in x * 2

The Data Constructor Expression

Data Constructor Expressions are expressions that create data values by applying arguments to data type constructors. Data constructor expressions look similar to function calls, but data constructors always start with an upper-case letter.

For data type constructors without parameters, the parentheses are optional.


DataConstrExp ::=

TypeIdentifier [ ( [ PureExp { , PureExp } ] ) ]

Cons(True, Nil)

Defining new data types and their constructors is described in Algebraic Data Types.

The Function Call Expression

Function calls apply arguments to functions, producing a value. Function call expressions look similar to data constructor expressions, but function names always start with a lower-case letter. The parentheses are mandatory in function calls.


FnAppExp ::=

Identifier ( [ PureExp { , PureExp } ] )

tail(Cons(True, Nil))
The N-ary Function Call Expression

Calls to n-ary Constructors (see N-ary Constructors) are written with brackets ([]) instead of parentheses (()).


FnAppListExp ::=

Identifier [ [ PureExp { , PureExp } ] ]

The Conditional Expression

The value of the conditional expression if c then e1 else e2 is either the value of e1 or the value of e2, depending on the value of c, which must be of type Bool. Depending on the value of c, either e1 or e2 is evaluated, but not both.


IfExp ::=

if PureExp then PureExp else PureExp

if 5 == 4 then True else False

Case Expressions

ABS supports pattern matching via the Case Expression. A case expression consists of an input expression and a series of branches, each consisting of a pattern and a right hand side expression.

The case expression evaluates its input expression and attempts to match the resulting value against the branches until a matching pattern is found. The value of the case expression itself is the value of the expression on the right-hand side of the first matching pattern.

It is an error if no pattern matches the expression.

There are four different kinds of patterns available in ABS:

  • Variables (with different semantics depending on whether the variable is bound or not)

  • Literal Patterns (e.g., 5)

  • Data Constructor Patterns (e.g., Cons(Nil,x))

  • Underscore Pattern (_)


CaseExp ::=

case PureExp { { CaseExpBranch } }

CaseExpBranch ::=

Pattern => PureExp ;

Pattern ::=

_ | SimpleIdentifier | Literal | ConstrPattern

ConstrPattern ::=

TypeIdentifier [ ( [ Pattern { , Pattern } ] ) ]

The Variable Pattern

Variable patterns are written as identifiers starting with a lower-case letter. If the identifier does not name a variable in the current scope, the variable pattern matches any value and introducues a binding of the given identifier to the matched value for the right-hand side of the branch and the rest of the pattern itself. In case a binding for that identifier is already in scope, its value is compared to the value being matched against.

The variable being named by the variable pattern can be used in the right-hand-side expression of the corresponding branch. Typically, pattern variables are used inside of data constructor patterns to extract values from data constructors. For example:

let (Pair<Int, Int> a) = Pair(5, 5) in
  case a {
    Pair(x, x) => x; (1)
    Pair(x, y) => y; (2)
  } (3)
1 This branch matches a pair with identical values.
2 This branch matches every pair. Since pairs with identical values are matched by the previous branch, x and y will be different.
3 The value of the whole expression is 5, produced by the first branch.
let (x = 7) in
  case Pair(5, 5) {
    Pair(x, x) => x; (1)
    Pair(x, y) => y; (2)
    Pair(y, z) => z; (3)
  } (4)
1 This pattern does not match since x is bound to 7 and does not match 5.
2 This pattern does not match either, for the same reason.
3 This pattern contains only unbound variable patterns and therefore matches.
4 The value of the whole expression is 5, produced by the third branch.
The Literal Pattern

Literals can be used as patterns. The pattern matches if the value of the case expression is equal to the literal value.

let (Pair<Int, Int> a) = Pair(5, 5) in
  case a {
    Pair(3, x) => x; (1)
    Pair(x, y) => y; (2)
  } (3)
1 The pattern 3 does not match the value in the first position of the Pair constructor pattern.
2 This pattern matches.
3 The value of the whole expression is 5, produced by the second branch.
The Data Constructor Pattern

A data constructor pattern is written like a standard data constructor expression. Constructor arguments are again patterns.

let (List<Int> l) = list[1, 2, 3] in
  case l {
    Nil => 0; (1)
    Cons(1, _) => 15; (2)
    Cons(_, Cons(y, _)) => y; (3)
  } (4)
1 This pattern matches the empty list.
2 This pattern matches a list starting with the literal 1.
3 This pattern matches a list of at least length 2, and binds the second element to y.
4 The value of the whole expression is 15, produced by the second branch.
The Wildcard Pattern

The wildcard pattern, written with an underscore (_) matches any value.

let (List<Int> l) = list[1, 2, 3] in
  case l {
    Nil => True; (1)
    _ => False; (2)
}; (3)
1 This pattern matches the empty list.
2 This pattern matches anything.
3 The value of the whole expression is False, produced by the second branch.

The wildcard pattern can be used as the last pattern in a case expression to define a default case.

Typing of Case Expressions

A case expression is type-correct if and only if all its expressions and all its branches are type-correct and the right-hand side of all branches have a common super type. This common super type is also the type of the overall case expression. A branch (a pattern and its expression) is type-correct if its pattern and its right-hand side expression are type-correct. A pattern is type-correct if it can match the corresponding case expression.

4.2. Expressions with Side Effects

ABS has expressions with side effects. These expressions are only legal “stand-alone”, i.e., not as a sub-expression of another expression. This means that subexpressions of expressions can only be pure expressions. This restriction simplifies the reasoning about expressions in the ABS modeling language.


EffExp ::=

NewExp | SyncCall | AsyncCall | GetExp

New Expression

A new expression creates a new object from a class name and a list of arguments. In ABS objects can be created in two different ways. Either they are created in the current COG, using the new local expression, or they are created in a new COG by using the new expression (see The ABS Actor and Concurrency Model for more details about cogs).


NewExp ::=

new [ local ] TypeIdentifier ( [ PureExp {, PureExp } ] )

new local Foo(5)
new Bar()

Classes can declare an init block (see Classes), which is executed for each new instance. The semantics of the new expression guarantee that the init block is fully executed before the new object begins receiving method calls. Classes can also declare a run method, which is automatically invoked after the init block and subject to the normal scheduling rules for processes.

Synchronous Call Expression

A synchronous call consists of a target expression evaluating to an interface type, a method name declared in that interface, and a list of argument expressions.


SyncCall ::=

PureExp . SimpleIdentifier ( PureExp { , PureExp } )

Bool b = x.m(5, 3);

The semantics of the synchronous method call differ depending on whether the caller and callee are in the same cog. A synchronous method call between objects in the same cog has Java-like semantics, i.e., the caller is suspended and the called method starts executing immediately. When the called method finishes, the caller process is scheduled and resumes execution.

In the case when caller and called object are in different cogs, a synchronous method call is equivalent to and asynchronous method call immediately followed by a get expression on the resulting future. This means that the intuitive semantics of synchronous method calls are preserved, but introduces the possibility of deadlocks in case the callee tries to call back to an object of the caller cog.

Asynchronous Call Expression

An asynchronous call consists of a target expression evaluating to an interface type, a method name declared in that interface, and a list of argument expressions.


AsyncCall ::=

PureExp ! SimpleIdentifier ( PureExp { , PureExp } )

An asynchronous method call creates a new task in the COG that contains the target. This means that the caller task proceeds independently and in parallel with the callee task, without waiting for the result. The result of evaluating an asynchronous method call expression o!m(e) is a future of type (Fut<V>), where V is the return type of the callee method m.

This future is resolved (i.e., it gets a value) when the callee task finishes. It can be used to synchronize with the callee task and obtain the result of the method call.

Fut<Bool> f = x!m(5);

Get Expression

A get expression is used to obtain the value from a future. The current task is blocked until the future has been resolved, i.e., until the value of the future is available. No other task in the COG can be activated in the meantime.


GetExp ::=

PureExp . get

Bool b = f.get;

Await Expression

An await expression is a way to asynchronously call a method, wait for the callee to finish, and get the result in one expression.


AwaitExp ::=

await AsyncCall

A x = await o!m();

The statement above is equivalent to the three statements in the following example.

Fut<A> fx = o!m();
await fx?;
A x = fx.get;

5. Function Definitions

Functions take a list of arguments and evaluate the expression in their body, producing a return value. ABS functions are always pure. This means the body of a function can use all pure expressions (see Pure Expressions) but no expressions with side effects (see Expressions with Side Effects).

Functions can be parametric, which means that they can take and return parametric datatypes. This means that a function head defined over a parametric list datatype can return the first element of a list, regardless of its type. Parametric functions are defined like normal functions but have an additional type parameter section inside angle brackets (< >) after the function name.


FunctionDecl ::=

def Type SimpleIdentifier [ < SimpleTypeIdentifier { , SimpleTypeIdentifier } > ]

( [ Type SimpleIdentifier { , Type SimpleIdentifier } ] ) = PureExp ;

def Rat abs(Rat x) = if x > 0 then x else -x; (1)

def Int length<A>(List<A> list) = (2)
case list {
  Nil => 0;
  Cons(_, ls) => 1 + length(ls);

def A head<A>(List<A> list) = (3)
  case list { Cons(x, _) => x; };
1 The abs function returns the absolute value of its argument.
2 This parametric function takes lists with arbitrary values and returns an Integer.
3 This parametric function returns the same type that is contained in the list. (Note that head is a partial function which is not defined for empty lists.)
The ABS standard library contains some special functions that cannot be defined with pure expressions, for example the function println. Each special function has to be implemented in each backend. The details of implementing special functions are outside of the scope of this manual.

6. Statements

This chapter specifies all ABS statements.


Statement ::=

SkipStmt | VarDeclStmt | AssignStmt | ExpStmt | AssertStmt | AwaitStmt | SuspendStmt | ThrowStmt | ReturnStmt | Block | IfStmt | CaseStmt | WhileStmt | TryCatchFinallyStmt

6.1. Skip

The skip statement is a statement that does nothing.


SkipStmt ::=

skip ;


6.2. Variable Declarations

A variable declaration statement is used to declare variables. Variable declarations can occur at any point in a sequence of statements; i.e., it is not necessary to declare variables only at the beginning of methods or blocks.

Variables declared inside a block are in scope for the duration of the block. It is an error to declare a variable with the same name of another variable in scope. A local variable can have the same name as an object field.

A variable declaration has an expression that defines the initial value of the variable. The initialization expression is mandatory except for variables of reference types (interfaces and futures), in which case the variable is initialized with null if the initialization expression is omitted.


VarDeclStmt ::=

Type SimpleIdentifier [ = Exp ] ;

Bool b = True;

6.3. Variable Assignment

The assign statement assigns a value to a variable or a field.

Assignments to a field f can be written either this.f = e; or f = e;. In case a local variable f is in scope at the point of the assignment statement, the this prefix has to be used to assign to the field f; assignment to f will change the value of the local variable.


AssignStmt ::=

[ this . ] SimpleIdentifier = Exp ;

this.f = True;
x = 5;

6.4. Expressions as Statements

An expression statement is a statement that consists of a single expression. When an expression statement is executed, the expression is evaluated and the resulting value is discarded.

Expression statements are used for their side effects, for example issuing an asynchronous method call without waiting for its result.


ExpStmt ::=

Exp ;

Creating an object without storing a reference (and hence never invoking a method on the new object) can be a meaningful operation, for example when the object has a run method and interacts with the rest of the system by calling methods on references passed in via the new expression.
new Client(server);

6.5. Assertions

An assert statement is a statement for asserting certain conditions. If the expression evaluates to True, executing an assertion is equivalent to skip;. If the expression evalutes to False, it is equivalent to throw AssertionFailException;.


AssertStmt ::=

assert PureExp ;

assert x != null;

6.6. Await Statement

An await statement suspends the current task until the given guard becomes active (evalutes to True). While the task is suspended, other tasks within the same COG can be scheduled.

In general, each cog will continue running a task without preempting it until the task is finished or it reaches a scheduling point. Await statements are scheduling points, as are suspend statements and assignment or expression statements containing an await expression (see Await Expression).


AwaitStmt ::=

await Guard ;

Guard ::=

[ this . ] SimpleIdentifier ? | PureExp | Guard & Guard | duration ( PureExp , PureExp )

Fut<Bool> f = x!m();
await f?; (1)
await this.x == True; (2)
await f? & this.y > 5; (3)
await duration(3, 5); (4)
1 A claim guard becomes active when the future is resolved (contains a value).
2 A field guard is a Boolean expression over the object state.
3 A guard conjunction becomes active when both its components are active.
4 A duration guard becomes active after a certain amount of simulated time has passed. See Timed ABS for more on timed models.

6.7. Unconditional Release: Suspend

The suspend statement causes the current task to be suspended.


SuspendStmt ::=

suspend ;

There is no guarantee that the cog will choose another task to run; the current task might be resumed immediately after suspending itself.

6.8. Return

A return statement returns a value from a method. A return statement can only appear as a last statement in a method body.

For asynchronous method calls, executing the return statement will cause the future to be resolved so that it contains a value. Any claim guards awaiting the future will become active.

Methods that have a Unit return type do not need an explicit return statement. The future will be resolved when the method terminates.


ReturnStmt ::=

return Exp ;

ABS does not allow exiting a method from multiple points, e.g., via multiple return statements. This makes model analysis easier.
return x;

6.9. Throw

The keyword-statement throw is used to signal exceptions (runtime errors). It takes a single argument which is the exception-value to throw. For example:

 Int x = -1;
 if (x<0) {
    throw NegativeNumberException(x);
 else {
   if (x==0) {
      throw ZeroNumberException;
   else ...
The 'throw' statement can only be used inside imperative code. Throwing user-exceptions inside functional code is considered bad practice: the user’s function must be written instead to return an Either<Exception, A> value, as in the example:
def Either<Exception, Int> f(x,y) = if (y < 0)
                                    then Left(NegativeNumberException)
                                    else Right(...)

Despite this, there are certain built-in system-exceptions (see Section 3.3) that can originate from erroneous functional code. Examples of these are DivisionByZeroException and PatternMatchFailException, implicitly signaled by the ABS system.

When an exception is raised (signaled), the normal flow of the program will be abrupted. In order to resume the normal flow, the user has to explicitly handle the exception.

6.10. Blocks of Statements

A sequence of statements is called a block. A block introduces a scope for local variables.


Block ::=

{ { Statement } }

Semantically, a whole block is a single statement and can be written anywhere a single statement is valid.
  Int a = 0; (1)
  a = a + 1;
  n = a % 10;

{ } (2)
1 The variable a is in scope until the end of the block.
2 An empty block is equivalent to skip;.

6.11. Conditionals

if (5 < x) {
  y = 6;
else {
  y = 7;
if (True)
  x = 5;

6.12. Case: Pattern Matching

The case statement, like the case expression (see Case Expressions), consists of an expression and a series of branches, each consisting of a pattern and a statement (which can be a block).

When a case statement is executed, its input expression is evaluated and the value matched against the branches until a matching pattern is found. The statement in the right-hand side of that branch is then executed. Any variable bindings introduced by matching the pattern are in effect while executing that statement.

It is an error if no pattern matches the expression.

For a description of the patterns available, see Case Expressions.


CaseStmt ::=

case PureExp { { CaseStmtBranch } }

CaseStmtBranch ::=

Pattern => Stmt

Pair<Int, Int> p = Pair(2, 3);
Int x = 0;
case p {
  Pair(2, y) => { x = y; skip; }
  _ => x = -1;

6.13. The While Loop

The while loop repeats its body while the condition evalutes to True. The condition is re-evaluated after each iteration of the loop.


WhileStmt ::=

while ( PureExp ) Stmt

while (x < 5) {
  x = x + 1;

6.14. Handling Exceptions with Try-Catch-Finally

To handle an exception --- either explicitly signaled using the throw keyword or implicitly by a system exception --- the user has to surround the offending code with a try block. The statements in the try block will be executed in sequence until an exception happens. Upon an exception, the execution of the try block will stop and the exception will be matched against the exception-patterns defined in the catch block.

The catch block behaves similar to the case statement, with the only difference that the patterns can only have the type Exception. When the exception-pattern is matched, the statements associated with its catch clause will be executed.

After defining the catch block, the user can optionally supply a finally block of statements, that will be executed regardless of an exception happening or not.

The syntax is the following:

try {
catch {
  exception_pattern1  => stmt_or_block;
  exception_pattern2  => ... ;
  _ => ...
finally {

If there are no matching catch-clauses, the finally block will first be accordingly executed, before re-throwing the exception to its parent caller. Conversely, if the parent caller does not (correctly) handle the re-thrown exception, the exception will be propagated to its own parent caller, and so forth and so on.

7. Interfaces

Interfaces in ABS are similar to interfaces in Java. They have a name, which defines a nominal type, and they can extend zero or more other interfaces. The interface body consists of a list of method signature declarations. Method names start with a lowercase letter.


InterfaceDecl ::=

interface SimpleTypeIdentifier [ extends InterfaceList ] { { MethSig } }

InterfaceList ::=

TypeIdentifier { , TypeIdentifier }

MethSig ::=

Type SimpleIdentifier ( [ Type SimpleIdentifier { , Type SimpleIdentifier } ] ) ;

The interfaces in the example below represent a database system, providing functionality to store and retrieve files, and a node of a peer-to-peer file sharing system. Each node of a peer-to-peer system plays both the role of a server and a client.

interface DB {
  File getFile(Filename fId);
  Int getLength(Filename fId);
  Unit storeFile(Filename fId, File file);
  Filenames listFiles();
interface Client {
  List<Pair<Server,Filenames>> availFiles(List<Server> sList);

  Unit reqFile(Server sId, Filename fId);
interface Server {
  Filenames inquire();
  Int getLength(Filename fId);
  Packet getPack(Filename fId, Int pNbr);
interface Peer extends Client, Server {
  List<Server> getNeighbors();

8. Classes

Classes in ABS are used to create objects via the new expression. Classes can implement an arbitrary number of interfaces. Since classes are not types in ABS, classes typically implement one or more interfaces.

Classes in ABS have zero or more class parameters. Each class parameter defines a field of the class which is assigned a value via arguments the new expression.

Classes have an optional init block, which is executed before any other code. The init block cannot contain processor release points (i.e., await or suspend).


ClassDecl ::=

class SimpleTypeIdentifier [ ( [ ClassParameterList ] ) ] [ implements InterfaceList ]

{ [ FieldDeclList ] [ Block ] [ MethDeclList ] }

ClassParameterList ::=

Type SimpleIdentifier { , Type SimpleIdentifier }

InterfaceList ::=

TypeIdentifier { , TypeIdentifier }

FieldDeclList ::=

{ Type SimpleIdentifier [ = PureExp ] ; }

MethDeclList ::=

Type SimpleIdentifier ( [ Type SimpleIdentifier { , Type SimpleIdentifier } ] ) Block

class DataBase(Map<Filename,File> db) implements DB {
	File getFile(Filename fId) {
		return lookup(db, fId);

	Int getLength(Filename fId){
		return length(lookup(db, fId));

	Unit storeFile(Filename fId, File file) {
		db = insert(Pair(fId,file), db);

	Filenames listFiles() {
		return keys(db);


class Node(DB db, Peer admin, Filename file) implements Peer {

	Catalog catalog;
	List<Server> myNeighbors;
	// implementation...

Active Classes

A class can be active or passive. Active classes start an activity on their own upon creation. Passive classes only react to incoming method calls. A class is active if and only if it has a run method:

Unit run() {
	// active behavior ...

The run method is called after object initialization.

9. Modules

All ABS definitions (classes, interfaces, functions data types, type aliases) are contained in modules. All definitions are visible in their own module only, except when the module exports the name and it is imported in another module or referenced by its qualified name.

The export clause in a module definition exports names, not definitions as such. This means that if a module defines a class and an interface with the same name, both definitions will be accessible if that name is contained in the export clause.

9.1. Defining a Module


ModuleDecl ::=

module TypeIdentifier ; { Export } { Import } { Decl } [ Block ]

Export ::=

export IdentifierList [ from TypeIdentifier ] ;

| export \* [ from TypeIdentifier ] ;

Import ::=

import IdentifierList [ from TypeIdentifier ] ;

| import * from TypeIdentifier ;

IdentifierList ::=

AnyIdentifier { , AnyIdentifier }

AnyIdentifier ::=

Identifier | TypeIdentifier

Decl ::=

FunDecl | TypeSynDecl | DataTypeDecl | InterfaceDecl | ClassDecl

A module name is a type name and must always start with an upper case letter.

Every module starts with a declaration of the form

module MyModule;

This declaration starts a new module named MyModule. All declarations after this line until the next module declaration belong to the module MyModule.

The module ABS.StdLib contains the standard library and is automatically imported by every module. There is no need for an explicit import * from ABS.StdLib; clause.

9.2. Exporting Identifiers

By default, modules do not export any names. In order to make names defined within a module available to other modules, the names have to be exported. For example, to export a data type and a data constructor, one can write something like this:

module Drinks;
export Drink, pourMilk, pourWater;
data Drink = Milk | Water;
def Drink pourMilk() = Milk;
def Drink pourWater() = Water;

Note that in this example, the data constructors are not exported, and other modules can only create values of type Drink by calling the exported constructor functions pourMilk and pourWater. By only exporting the data type without any of its constructors, one can realize abstract data types in ABS.

A special export clause export *; exports all names that are defined in the module. Note that imported names are not re-exported by export *; (but can be re-exported via export * from OtherModule; clauses).

module Test;
export *;
export * from OtherModule;
import * from OtherModule;

9.3. Importing Identifiers

In order to use exported names of a module in another module, the names have to be imported. In a module definition, a list of import clauses follows the list of export clauses. After being imported, these names are accessible in the current module.

Names can be accessible either qualified (with package prefix) or unqualified, depending on how they are imported.

The following example makes the Drink data type of the module Drinks accessible as Drinks.Drink:

module Bar;
import Drinks.Drink; (1)
import pourMilk from Drinks; (2)
1 The name Drink is accessible in module Bar as Drinks.Drink.
2 The name pourMilk is accessible in module Bar both as Drinks.pourMilk and pourMilk.

The import * from Module; statement makes all names that are exported from module Module accessible without module qualifier in the current module.

module Bar;
import * from Drinks; (1)
1 All names from Drinks are accessible in Bar with and without the Drinks. prefix.

Re-exporting Imported Names

It is possible to re-export names that are imported from another module. For example,

module Bar;
export * from Drinks;
import * from Drinks;

re-exports from Bar all names that are exported by module Drinks. Another module that writes import * from Bar; will have the names from Drinks accessible as well.

To re-export only selected names, include only these names in the export list:

module Bar;
export Drink; (1)
import * from Drinks;

Only Drink is exported from Bar.

Note that only names that have been imported can be re-exported. For example:

module Bar;
export * from Drinks;
import Drink from Drinks;

only re-exports Drink, as this is the only name imported from module Drinks.

10. The Standard Library

This chapter documents the ABS standard library. All definitions, except where noted otherwise, are contained in the module ABS.StdLib which is included by default in every module. Therefore, no import statement is necessary to use these definitions.

10.1. Boolean values

Datatypes and Constructors

The literals for Boolean values are True and False. The name of the datatype is Bool.

Bool value = True;


The following operators apply to Boolean values:

Expression Meaning Associativity Argument types Result type

e1 || e2

logical or


Bool, Bool


e1 && e2

logical and


Bool, Bool


e1 == e2





e1 != e2





e1 < e2

less than




e1 < = e2

less than or equal to




e1 > e2

greater than




e1 >= e2

greater than or equal to




! e

logical negation




~ e

logical negation (deprecated)




10.2. Numbers

Datatypes and constructors

The two numeric datatypes are Int and Rat. See Built-in Types for their syntax.


Expression Meaning Associativity Argument types Result type

e1 == e2





e1 != e2





e1 < e2

less than




e1 < = e2

less than or equal to




e1 > e2

greater than




e1 >= e2

greater than or equal to




e1 + e2



number, number


e1 - e2



number, number


e1 * e2



number, number


e1 / e2



number, number


e1 % e2



number, number



min, max

These functions calculate the maximum and minimum of their two arguments. Since ABS datatypes are ordered, they can be applied to arguments of all types.

A max<A>(A a, A b)
A min<A>(A a, A b)

This function calculates the absolute (positive) value of its argument.

Rat abs(Rat x)

Converts a rational number to an integer by truncating towards zero.

Int truncate(Rat a)

This function calculates b to the power of n.

Rat pow(Rat b, Int n)

This function approximates the square root of x; it stops when two subsequent estimates (as per Newton’s algorithm) differ by less than epsilon. estimate is an initial estimate of the square root.

Rat sqrt_newton(Rat x, Rat estimate, Rat epsilon)

This function approximates e to the power of x; it stops when two subsequent estimates (as per Newton’s algorithm) differ by less than epsilon.

Rat exp_newton(Rat x, Rat epsilon)

Returns an integer between 0 and its argument.

Int random(Int below)

10.3. Strings

Datatypes and Constructors

The datatype for strings is String.

String literals are enclosed in double quotes ("). Line feed in a string literal is written as \n, carriage return as \r.


Expression Meaning Associativity Argument types Result type

e1 == e2





e1 != e2





e1 < e2

less than




e1 < = e2

less than or equal to




e1 > e2

greater than




e1 >= e2

greater than or equal to




e1 + e2



String, String




This function converts any data into a printable string representation.

def String toString<T>(T t)

Returns a substring of a given string str with length length starting from position start (inclusive). The first character in a string has position 0.

def String substr(String str, Int start, Int length)

Returns the length of the given string str. The empty string ("") has length 0.

def Int strlen(String str)

Prints the given string s to standard output, followed by a newline, meaning that the next output will not continue on the same line.

def Unit println(String s)

Prints the given string s to standard output. Does not cause the next output to begin on a new line.

def Unit print(String s)

10.4. Unit

Unit is the empty (void) datatype.

Datatypes and Constructors

Both the datatype and the single constructor are named Unit.

10.5. Lists

A list is a sequence of values of the same type. Lists are expressed as recursive datastructures. The time to access a value is proportional to the length of the list. The first value of a list can be accessed in constant time.

Datatypes and Constructors

A list is defined either as the empty list (Nil) or as a value a followed by another list l (Cons(a, l)).

data List<A> = Nil | Cons(A head, List<A> tail);

Literal lists of arbitrary length can be written using a special function list. In the following example, l1 and l2 contain the same elements.

List<Int> l1 = list[1, 2, 3];
List<Int> l2 = Cons(1, Cons(2, Cons(3, Nil)));



Returns the head of a list.

def A head(List<A> l);

Returns the tail (rest) of a list.

def List<A> tail(List<A> l);

Returns the length of a list. The length of Nil is 0.

def Int length(List<A> l);

Checks if a list is empty. Returns True for Nil, False otherwise.

def Bool isEmpty(List<A> l);

Returns the n-th element of a list. Returns the head of l for n=0, returns the last element of l for n=lenght(l)-1.

It is an error if n is equal to or larger than length(l).

def A nth(List<A> l, Int n);

Returns a fresh list where all occurrences of a have been removed.

def List<A> without<A>(List<A> list, A a);

Returns a list containing all elements of list list1 followed by all elements of list list2.

def List<A> concatenate<A>(List<A> list1, List<A> list2);

Returns a list containing all elements of list l followed by the element p in the last position.

def List<A> appendright<A>(List<A> l, A p);

Returns a list containing all elements of l in reverse order.

def List<A> reverse<A>(List<A> l);

Returns a list of length n containing p n times.

def List<A> copy<A>(A p, Int n);

10.6. Sets

Datatypes and Constructors

The datatype for sets with elements of type A is Set<A>. Sets are constructed with a special function set. The expresssion set[] produces the empty set.

The following example produces a set with the three elements 1, 2, 3.

Set<Int> s = set[1, 2, 3, 3];



Returns True if set ss contains element e, False otherwise.

def Bool contains<A>(Set<A> ss, A e);

Returns True if set xs is empty, False otherwise.

def Bool contains<A>(Set<A> ss, A e);

Returns the number of elemewnts in set xs.

def Int size<A>(Set<A> xs);

Returns a set containing all elements of sets set1 and set2.

def Set<A> union<A>(Set<A> set1, Set<A> set2);

Returns a set containing all elements that are present in both sets set1 and set2.

def Set<A> intersection<A>(Set<A> set1, Set<A> set2);

Returns a set containing all elements of set set1 not present in set set2.

def Set<A> intersection<A>(Set<A> set1, Set<A> set2);

Returns a set with all elements of set xs plus element e. Returns a set with the same elements as xs if xs already contains e.

def Set<A> insertElement<A>(Set<A> xs, A e);

Returns a set with all elements of set xs except element e. Returns a set with the same elements as xs if xs did not contain e.

def Set<A> remove<A>(Set<A> xs, A e);

Returns one element from a set.

def A take<A>(Set<A> ss);
To iterate over a set, use take to extract one value and remove to remove it from the set. Repeat until the set is empty.

10.7. Maps

Datatypes and Constructors

The datatype for a map from type A to type B is is Map<A, B>. Maps are constructed using pairs of type Pair<A, B> and the special function map. The expresssion map[] produces an empty map.

The following example produces a set with two entries 1 → "ABS" and 3 → "SACO".

Map<Int, String> m = map[Pair(1, "ABS"), Pair(3, "SACO")];
In case the arguments contain duplicate keys, the resulting map will contain all the given entries, with the first entry shadowing the following ones.



Returns a map with the first occurrence of key removed.

def Map<A, B> removeKey<A, B>(Map<A, B> map, A key);

Returns a list of all values within the map.

def List<B> values<A, B>(Map<A, B> map);

Returns a set of all keys of the map.

def Set<A> keys<A, B>(Map<A, B> map);

If value v is associated with a given key k, return Just(v). Otherwise, return Nothing.

def Maybe<B> lookup<A, B>(Map<A, B> ms, A k);

Returns the value associated with key k. If the map does not contain an entry with key k, return the value d.

def B lookupDefault<A, B>(Map<A, B> ms, A k, B d);
If you need to know whether the map contains an entry for key k, use the function lookup instead.

Returns the value associated with key k. It is an error if the map does not contain an entry with key k.

def B lookupUnsafe<A, B>(Map<A, B> ms, A k);

Returns a map with all entries of map plus an entry p, which is given as a pair (Pair(key, value)) and maps key to value. If map already contains an entry with the same key key, it is not removed from the map but lookup will return the new value value. (The function removeKey removes the first entry for a given key and thus “undoes” the effect of calling insert.)

def Map<A, B> insert<A, B>(Map<A, B> map, Pair<A, B> p);

Returns a map with all entries of ms plus an entry mapping k to v, minus the first entry already mapping k to a value.

def Map<A, B> put<A, B>(Map<A, B> ms, A k, B v);

10.8. Pairs

Datatypes and Constructors

The Pair<A, B> datatype holds a pair of values of types A and B, respectively. The constructor is called Pair as well.

Pair<Int, String> pair = Pair(15, "Hello World");



The function fst returns the first value in a pair.


The function snd returns the second value in a pair.

10.9. Triples

Datatypes and Constructors

The Triple<A, B, C> datatype holds a triple of values of types A, B and C, respectively. The constructor is called Triple as well.

Triple<Int, String, Bool> triple = Pair(15, "Hello World", False);



The function fstT returns the first value in a triple.


The function sndT returns the second value in a triple.


The function trdT returns the third value in a triple.

10.10. Optionals

Datatypes and Constructors

The datatype Maybe<A> wraps a concrete value of type A. The value Nothing denotes the absence of such a value.

Maybe<Int> answer = Just(42);
Maybe<String> question = Nothing;



The function isJust returns False if the Maybe value is Nothing, True otherwise.

def Bool isJust<A>(Maybe<A> a);

The function fromJust returns the wrapped value of a Maybe. It is an error to call fromJust on Nothing.

def A fromJust<A>(Maybe<A> m);

11. Timed ABS

Timed ABS is an extension to the core ABS language that introduces a notion of abstract time. Timed ABS can be used to model not only the functional behavior but also the timing-related behavior of real systems running on real hardware. In contrast to real systems, time in an ABS model does not advance by itself. The time model of Timed ABS takes inspiration from formalisms such as Timed Automata and Real-Time Maude.

All untimed ABS models are valid in Timed ABS. An ABS model that contains no time-influencing statements will run without influencing the clock and will finish at time zero.

The ABS notion of time is dense time with run-to-completion semantics. Timed ABS adds a clock to the language semantics that advances in response to certain language constructs. Time is expressed as a rational number, so the clock can advance in infitesimally small steps.

Time only advances when all processes are blocked or suspended and no process is ready to run. This means that for time to advance, all processes are in one of the following states:

  • the process is awaiting for a guard that is not enabled (see Await Statement)

  • the process is blocked on a future that is not available (see Get Expression)

  • the process is suspended waiting for time to advance

  • the process is waiting for some resources

In practice this means that all process run as long as there is “work to be done.”

11.1. Datatypes and Constructors

Time is expressed as a datatype Time. Its definition in the standard library is as follows:

data Time = Time(Rat timeValue);

11.2. Functions

The function now always returns the current time.

def Time now()

Note that since ABS uses simulated time, two calls to now can return the same value. Specifically, the result of now() changes only by executing duration or await duration statements, or by waiting for resources to become available.

  Time t1 = now();
  Int i = pow(2, 50);
  Time t2 = now();
  assert (t1 == t2); (1)
1 This assertion will not fail, since no time has passed in the model. Time advance in ABS is explicit.

11.3. Statements

The duration(min, max) statement blocks the cog of the executing process until at least min and at most max time units have passed. The await duration(min, max) statement (see Await Statement) suspends the current process until at least min and at most max time units have passed.


DurationStmt ::=

duration ( PureExp , PureExp ) ;

AwaitStmt ::=

await Guard ;

Guard ::=

…​ | DurationGuard

DurationGuard ::=

duration ( PureExp , PureExp )

The difference between duration and await duration is that in the latter case other processes in the same cog can execute while the awaiting process is suspended. In the case of the blocking duration statement, no other process in the same cog can execute. Note that processes in other cogs are not influenced by duration or await duration, except when they attempt to synchronize with that process.

A subtle difference between duration and await duration is that in the latter case, the suspended process becomes eligible for scheduling after the specified time, but there is no guarantee that it will actually be scheduled at that point. This means that more time might pass than expressed in the await duration guard!
  Time t = now();
  await duration(1/2, 5); (1)
  Time t2 = now(); (2)
1 Here the process suspends for 1/2-5 time units
2 t2 will be at least 1/2 time units larger than t
  Time t = now();
  duration(1/2, 5); (1)
  Time t2 = now(); (2)
1 Here the cog blocks for 1/2-5 time units
2 t2 will be between 1/2 and 5 time units larger than t

11.4. Semantics of Time Advancement

The simulated clock advances such that it makes the least amount of “jumps” without missing any point of interest. This means that when a process waits or blocks for an interval (min, max), the clock will not advance more than max, since otherwise it would miss unblocking the process. On the other hand, the clock will advance by the highest amount allowed by the model. This means that if only one process waits for (min, max), the clock will advance by max.

Big-step time advance
Figure 5. Big-step time advance

Figure Big-step time advance shows a timeline with two process, P1 and P2. They are waiting for time to advance between (4, 6) and (3, 5) units, respectively. Assuming that no other process is ready to run, the clock will advance the maximum amount that still hits the earliest interval, in this case 5. Since the clock is now within both intervals, both processes are unblocked and ready to run.

12. Resource Modeling in Timed ABS

ABS can be used to simulate the effects of deployment decisions on the cost and performance of running a distributed system. To achieve this, we need to add the following aspects to a model:

  • A notion of time to express the runtime effects of varying the system (see Timed ABS)

  • A notion of location to describe where some component of the overall system is executing (see Deployment Components)

  • A notion of cost of executing parts of a system, against various resource types (see Resource Types)

In this chapter, we deal with the non-functional properties of systems: code deployment on varying numbers and kinds of machines, and the effects of code locality and different resource types such as CPU speeds, interconnection bandwidth, etc. on the performance of a system.

All language identifiers described in this section reside in the ABS.DC module.

12.1. Deployment Components

In ABS, processes run inside cogs. Deployment components are used to provide a location to cogs. Cogs residing on the same deployment component share the resources provided by the deployment component.

Deployment Components are first-class constructs in the ABS language. A reference to a deployment component is treated the same way as a reference to an object. Deployment Components are created using the new expression. Any other cog can be created "on" a deployment component by using a DC annotation to the new statement.

DeploymentComponent dc = new DeploymentComponent("Server 1", map[Pair(Speed, 10)]); (1)
[DC: dc] Worker w = new CWorker(); (2)
1 A new deployment component dc is created with 10 Speed resources <2> w is created on the new deployment component dc
It is an error to try to locally create deployment components (via new local DeploymentComponent(…​)) or new local objects on another cog (via [DC: x] new local C()).
Resources and Deployment Components

As seen above, each deployment component “carries” some amount of resources for each resource type. This is expressed as a map from resource type to a number, for example map[Pair(Speed, 10), Pair(Bandwidth, 20)]. When no amount is given for some resource type, it is infinite. See Resource Types for a description of the available resource types.


[Atomic] Rat load(Resourcetype rtype, Int periods)

Return the load (0-100) for given resource type rtype over the last n periods. If resource is infinite, return 0.

[Atomic] InfRat total(Resourcetype rtype)

Return the total available amount for given resourcetype. If the resource type is infinite, return InfRat; if it has value value, return Fin(value).

Unit transfer(DeploymentComponent target, Rat amount, Resourcetype rtype)

Transfer amount resources of type rtype from the current deployment component to target. Takes effect on the next time period.

(This method is implemented via decrementResources and incrementResources.)

Unit decrementResources(Rat amount, Resourcetype rtype)

Decrement available resourcetype by given amount from the next time interval onwards.

Unit incrementResources(Rat amount, Resourcetype rtype)

Increment available resourcetype by given amount from the next time interval onwards.

[Atomic] String getName()

Returns the name of the deployment component. The name is set by the first argument to the new expression.

[Atomic] Time getCreationTime()

Get the creation time of the deployment component, in terms of the simulated clock.

[Atomic] Rat getStartupDuration()

Get the specified startup duration, or 0 if none specified.

[Atomic] Rat getShutdownDuration()

Get the specified shutdown duration, or 0 if none specified.

[Atomic] Int getPaymentInterval()

Get the specified payment interval, or 1 if none specified.

[Atomic] Rat getCostPerInterval()

Get the specified cost per interval, or 0 if none specified.

Bool shutdown()

Shut down the deployment component. It is an error to create a new object on a deployment component that has been shutdown, or to invoke a method on an object residing on a deployment component that has been shut down.

[Atomic] Unit setProvider(CloudProvider provider)

Set the cloud provider that manages this deployment component. See The CloudProvider API for a discussion of cloud providers.

[Atomic] CloudProvider getProvider()

Get the cloud provider that manages this deployment component. Returns null if no cloud provider set. See The CloudProvider API for a discussion of cloud providers.

Bool acquire()

Convenience method for calling acquireInstance of the associated cloud provider. If no cloud provider is set, returns True.

Bool release()

Convenience method for calling releaseInstance of the associated cloud provider. If no cloud provider is set, returns True.

12.2. Resource Types

The term Resource can be used in different ways. In ABS, we understand a Resource to be a countable, measurable property that is influenced by program execution and the passage of time. The resources currently supported by the ABS language are defined in the ABS.DC module as follows:

data Resourcetype = Speed | Bandwidth | Memory | Cores ;


The Speed resource type models execution speed. Intuitively, a deployment component with twice the number of Speed resources will execute twice as fast. Not all statements consume Speed resources while executing — Speed resources are consumed when execution in the current process reaches a statement that is annotated with a Cost annotation.

[Cost: 5] skip;

Executing the above skip statement will consume 5 Speed resources from the deployment component where the cog was deployed. If the deployment component does not have infinite Speed resources, executing the skip statement might take an observable amount of time.


Bandwidth is a measure of transmission speed. Bandwidth resources are consumed during method invocation and return statements. Bandwidth resources are consumed on both the sending and the receiving deployment component.

Bandwidth consumption is expressed via a Size annotation:

[DataSize: 2 * length(x)] o!m(x);

Executing the above method invocation statement will consume bandwidth resources proportional to the length of list x. The resources will be consumed both from the deployment component where the cog was deployed, and from the one where o was deployed.


The Memory resource type abstracts from the size of main memory, as a measure of how many and which cogs can be created on a deployment component. In contrast to bandwidth and speed, memory does not influence the timed behavior of the simulation of an ABS model; it is used for static deployment modeling.


The Cores resource type expresses the number of CPU cores on a deployment component. It is used for static deployment decisions and does not have influence on the timing behavior of simulations (use the Speed resource type for this purpose).

12.3. Modeling Resource Usage

As described above, resource models are added to an ABS model using annotations. Adding annotations to specific statements and declarations causes side-effects on the status of an applicable deployment component.

module Test;
import * from ABS.DC; (1)
interface I {
  Unit process();
[DataSize: 3] (2)
class C implements I {
  Unit process() {
    [Cost: 10] skip; (3)

  DeploymentComponent dc = new DeploymentComponent("Server",
    map[Pair(CPU, 5), Pair(Bandwidth, 10), Pair(Memory, 5)]);
  [DC: dc] I i = new C(); (4)
  [DataSize: 5] i!process(); (5)
1 Make all necessary identifiers accessible in the current module
2 Declare the memory needed to instantiate a cog of class C
3 Executing this statement costs 10 CPU units; the time needed depends on the CPU capacity of the deployment component, and on other cogs executing in parallel on the same deployment component. In this example, executing the skip statement will take two time units.
4 Creating a new cog succeeds since the available memory (5) is more than the necessary memory (3). Trying to create a second cog of the same class will fail.
5 Executing this method call consumes 5 Bandwidth resources. Since dc has 10 bandwidth per time unit, the message will be transported instantly.

12.4. The CloudProvider API

(pre)launchInstance might have a delay, the others are instantaneous. launchInstance might hand out an already-running instance if it has been released; in this case there will be no delay.

acquireInstance, releaseInstance are called from deployment components. launchInstance does the equivalent of acquireInstance.

Instance descriptions. Call setInstanceDescriptions with a map of (name → resources) information. Then, (pre)launchInstanceNamed returns a deployment component with the specified resources, or null if the given name could not be found. The resulting deployment components are then handled as normal (acquireInstance/releaseInstance/killInstance).

interface CloudProvider {
    DeploymentComponent prelaunchInstance(Map<Resourcetype, Rat> d);
    DeploymentComponent launchInstance(Map<Resourcetype, Rat> description);
    Bool acquireInstance(DeploymentComponent instance);
    Bool releaseInstance(DeploymentComponent instance);
    Bool killInstance(DeploymentComponent instance);

    [Atomic] Rat getAccumulatedCost();
    [Atomic] Unit shutdown();

    [Atomic] Unit setInstanceDescriptions(Map<String, Map<Resourcetype, Rat>> instanceDescriptions);
    [Atomic] Map<String, Map<Resourcetype, Rat>> getInstanceDescriptions();
    DeploymentComponent prelaunchInstanceNamed(String instancename);
    DeploymentComponent launchInstanceNamed(String instancename);

13. Feature Modelling

13.1. Deltas

ABS supports the delta-oriented programming model, an approach that aids the development of a set of programs simultaneously from a single code base, following the software product line engineering approach. In delta-oriented programming, features defined by a feature model are associated with code modules that describe modifications to a core program. In ABS, these modules are called delta modules. Hence the implementation of a software product line in ABS is divided into a core and a set of delta modules.

The core consists of a set of ABS modules that implement a complete software product of the corresponding software product line. Delta modules (or deltas in short) describe how to change the core program to obtain new products. This includes adding new classes and interfaces, modifying existing ones, or even removing some classes from the core. Delta modules can also modify the functional entities of an ABS program, that is, they can add and modify data types and type synonyms, and add functions.

Deltas are applied to the core program by the ABS compiler front end. The choice of which delta modules to apply depends on the selection of a set of features, that is, a particular product of the SPL. The role of the ABS compiler front end is to translate textual ABS models into an internal representation and check the models for syntax and semantic errors. The role of the back ends is to generate code for the models targeting some suitable execution or simulation environment.

DeltaDecl      ::= 'delta' TypeId [DeltaParams] ';' [ModuleAccess] ModuleModifier*
ModuleModifier ::= 'adds' ClassDecl
                 | 'removes' 'class' TypeName ';'
                 | 'modifies' 'class' TypeName
                   ['adds' TypeId (',' TypeId)*] ['removes' TypeId (',' TypeId)*]
                   '{' Modifier* '}'
                 | 'adds' InterfaceDecl
                 | 'removes' 'interface' TypeName ';'
                 | 'modifies' 'interface' TypeName '{' InterfaceModifier* '}'
                 | 'adds' FunctionDecl
                 | 'adds' DataTypeDecl
                 | 'modifies' DataTypeDecl
                 | 'adds' TypeSynDecl
                 | 'modifies' TypeSynDecl
                 | 'adds' Import
                 | 'adds' Export

InterfaceModifier ::= 'adds' MethSig ';'
                    | 'removes' MethSig ';'

Modifier ::= 'adds' FieldDecl
           | 'removes' FieldDecl
           | 'adds' MethDecl
           | 'removes' MethSig
           | 'modifies' MethDecl

DeltaParams ::= '(' DeltaParam (',' DeltaParam)* ')'

DeltaParam ::= Identifier HasCondition*
             | Type Identifier

ModuleAccess ::= 'uses' TypeId ';'

HasCondition ::= 'hasField' FieldDecl
               | 'hasMethod' MethSig
               | 'hasInterface' TypeId

The DeltaDecl clause specifies the syntax of delta modules, consisting of a unique identifier, a module access directive, a list of parameters and a sequence of module modifiers. The module access directive gives the delta access to the namespace of a particular module. In other words, it specifies the ABS module to which modifications using unqualified identifiers apply by default. A delta can still make changes to several modules by fully qualifying the TypeName of module modifiers.

While delta modelling supports a broad range of ways to modify an ABS model, not all ABS program entities are modifiable. These unsupported modifications are listed here for completeness. While these modifications could be easily specified and implemented, we opted not to overload the language with features that have not been regarded as necessary in practice:

Class parameters and init block

Deltas currently do not support the modification of class parameter lists or class init blocks.


currently only support adding functions, and adding and modifying data types and type synonyms. Removal is not supported.


Deltas currently do not support adding new modules or removing modules.

Imports and Exports

While deltas do support the addition of import and export statements to modules, they do not support their modification or removal.

Main block

Deltas currently do not support the modification of the program’s main block.

13.2. Products and Product Lines

ABS provides language constructs and tools for modelling variable systems following Software Product Line (SPL) engineering practices.

Software variability is commonly expressed using features which can be present or absent from a product of the product line. Features are organised in a feature model, which is essentially a set of logical constraints expressing the dependencies between features. Thus the feature model defines a set of legal feature combinations, which represent the set of valid software products that can be built from the given features.

Specifying the Product Line

The ABS configuration language links feature models, which describe the structure of a SPL, to delta modules, which implement behaviour. The configuration defines, for each selection of features satisfied by the product selection, which delta modules should be applied to the core. Furthermore, it guides the code generation by ordering the application of the delta modules.

Configuration ::= 'productline' TypeId ';' Features ';' DeltaClause*
Features      ::='features' FName (',' FName)*
DeltaClause   ::= 'delta' DeltaSpec [AfterCondition] [ApplicationCondition] ';'
DeltaSpec     ::= DeltaName ['(' DeltaParams ')']
DeltaName     ::= TypeId
DeltaParams   ::= DeltaParam (',' DeltaParam)*
DeltaParam    ::= FName | FName'.'AName
AfterClause   ::= 'after' DeltaName (',' DeltaName)*
WhenClause    ::= 'when' AppCond
AppCond       ::= AppCond '&&' AppCond
                | AppCond '||' AppCond
                | '!' AppCond
                | '(' AppCond ')'
                | FName

Features and delta modules are associated through application conditions, which are logical expressions over the set of features and attributes in a feature model. The collection of applicable delta modules is given by the application conditions that are true for a particular feature and attribute selection. By not associating the delta modules directly with features, a degree of flexibility is obtained.

Each delta clause has a DeltaSpec, specifying the name of a delta module name and, optionally, a list of parameters; an AfterClause, specifying the delta modules that the current delta must be applied after; and an application condition AppCond, specifying an arbitrary predicate over the feature names (FName) and attribute names (AName) in the feature model that describes when the given delta module is applied.

productline DeltaResourceExample;
features Cost, NoCost, NoDeploymentScenario, UnlimitedMachines, LimitedMachines, Wordcount, Wordsearch;
delta DOccurrences when Wordsearch;
delta DFixedCost(Cost.cost) when Cost;
delta DUnboundedDeployment(UnlimitedMachines.capacity) when UnlimitedMachines;
delta DBoundedDeployment(LimitedMachines.capacity, LimitedMachines.machinelimit) when LimitedMachines;

Specifying Products

ABS allows the developer to name products that are of particular interest, in order to easily refer to them later when the actual code needs to be generated. A product definition states which features are to be included in the product and sets attributes of those features to concrete values. In the simplest case products are declared directly, by listing the features that they include. It is also possible to declare products based on other products using product expressions. Product expressions use set-theoretic operations (union, intersection, complement) over products and sets of features.

Selection ::= 'product' TypeId ( '(' FeatureSpecs ')' ';' | '=' ProductExpr ';' )
ProductExpr: '{' FeatureSpecs '}'
			| ProductExpr '&&' ProductExpr
			| ProductExpr '||' ProductExpr
			| ProductExpr '-' ProductExpr
			| TypeId
			| '(' ProductExpr ')'
FeatureSpecs ::= FeatureSpec (',' FeatureSpec)*
FeatureSpec ::= FName [AttributeAssignments]
AttributeAssignments ::= '{' AttributeAssignment (',' AttributeAssignment '}'
AttributeAssignment ::= AName '=' Literal

Here are some product definitions for the DeltaResourceExample productline:

product WordcountModel (Wordcount, NoCost, NoDeploymentScenario);
product WordcountFull (Wordcount, Cost{cost=10}, UnlimitedMachines{capacity=20});
product WordsearchFull (Wordsearch, Cost{cost=10}, UnlimitedMachines{capacity=20});
product WordsearchDemo (Wordsearch, Cost{cost=10}, LimitedMachines{capacity=20, machinelimit=2});

Here are some product definitions for the CharityOrganizationExample with ProductExpr:

product Org1 = SekolahBermainMatahari || {Continuous};
product Org2 = SekolahBermainMatahari || {Continuous, Automatic_Report};
product Org3 = SekolahBermainMatahari || PKPU;
product Org4 = SekolahBermainMatahari || PKPU || RamadhanForKids;
product Org5 = SekolahBermainMatahari || PKPU || RamadhanForKids || BeriBuku;
product Org6 = SekolahBermainMatahari && RamadhanForKids;
product Org7 = SekolahBermainMatahari && BeriBuku;
product Org8 = SekolahBermainMatahari - {Eventual};
product Org9 = SekolahBermainMatahari - {Eventual, Income};
product Org10 = SekolahBermainMatahari && RamadhanForKids || {Money, Item};
product Org11 = SekolahBermainMatahari && (RamadhanForKids || {Money, Item});

The Feature Model

The FeatureModel clause specifies a number of "orthogonal" root feature models along with a number of extensions that specify additional constraints, typically cross-tree dependencies. Its grammar is as follows:

FeatureModel ::= ('root' FeatureDecl)* FeatureExtension*
FeatureDecl  ::= FName [ '{' [Group] AttributeDecl* Constraint* '}' ]
FeatureExtension ::= 'extension' FName '{' AttributeDecl* Constraint* '}'
Group ::= 'group' Cardinality '{' ['opt'] FeatureDecl (',' ['opt'] FeatureDecl)* '}'
Cardinality ::= 'allof' | 'oneof' | '[' IntLiteral '..' Limit ']'
AttributeDecl ::= 'Int' AName ';'
                | 'Int' AName in '[' Limit '..' Limit ']' ';'
                | 'Bool' AName ';'
                | 'String' AName ';'
Limit ::= IntLiteral | '*'
Constraint ::= Expr ';'
             | 'ifin'':'  Expr ';'
             | 'ifout'':' Expr ';'
             | 'require'':' FName ';'
             | 'exclude'':' FName ';'
Expr ::= 'True'
       | 'False'
       | IntLiteral
       | StringLiteral
       | FName
       | AName
       | FName '.'AName
       | UnOp Expr
       | Expr BinOp Expr
       | '(' Expr ')'
UnOp ::= '!' | '-'
BinOp ::= '||' | '&&' | '->' | '<->' | '=='
        | '!=' | '>'  | '<'  | '>='  | '<='
        | '+'  | '-'  | '*'  | '/'   | '%'

Attributes and values range over integers, strings or booleans.

The FeatureDecl clause specifies the details of a given feature, firstly by giving it a name (FName), followed by a number of possibly optional sub-features, the feature’s attributes and any relevant constraints.

The FeatureExtension clause specifies additional constraints and attributes for a feature, and if the extended feature has no children a group can also be specified. This is particularly useful for specifying constraints that do not fit into the tree structure given by the root feature model.

Here is an example feature model for the DeltaResourceExample productline, defining valid combinations of features and valid ranges of parameters for cost, capacity and number of machines:

root Calculations {
  group oneof {

root Resources {
  group oneof {
    Cost { Int cost in [ 0 .. 10000 ] ; }

root Deployments {
  group oneof {
    UnlimitedMachines { Int capacity in [ 0 .. 10000 ] ; },
    LimitedMachines { Int capacity in [ 0 .. 10000 ] ;
      Int machinelimit in [ 0 .. 100 ] ; }

Feature Model Reflection

There is support for limited reflection on the feature model and configured product in the module ABS.Productline. The datatype Feature contains constructors for all feature names. The function product_features returns a list of features contained in the current product, and product_name returns the name of the product, or the empty string if no product was specified.

The following sample code shows the usage, assuming that product Product was generated:

module Test;
import * from ABS.Productline;

  List<Feature> foo = product_features(); // => Cons(FeatureA, Cons(FeatureC, Nil))
  String name = product_name();           // => "Product"

productline Test;
features FeatureA, FeatureB, FeatureC;

product Product(FeatureA, FeatureC);

14. ABS Backends

This section describes the available and supported backends for ABS. Different backends have different purposes (simulation, code execution, visualization). Their respective section describes their features and usage.

The following table gives an overview of the features that different backends have.

Real-Time ABS

Simulating a dense-time clock, and language constructs expressing delays and task deadlines. Used for simulating time usage of ABS models.

Resource Models

Specification of resource availability (processor power, bandwidth) of Deployment Components and simulation of resource usage deployed thereon. Builds on the semantics of Real-Time ABS.


Running ABS code on a number of physical or virtual machines, with support for creating new cogs remotely.


Foreign-Language Interface, the ability to call backend-specific native code from ABS.

Table 4. Backend Capabilities
Backend Maude Erlang Haskell Java

Real-Time ABS


partly implemented (no deadlines)



Resource Models















14.1. Maude Backend

The Maude backend is a high-level, executable semantics in rewriting logic of the ABS language. Due to its relatively compact nature, it serves as a test-bed for new language features.

Executing a model on the Maude backend results in a complete snapshot of the system state after execution has finished.

The main drawback of the Maude backend is its relatively poor performance, making it not very suitable to simulate large models.


  • CPU and bandwidth resources

  • Simulation of resource usage on deployment components

  • Timed semantics

  • Executable formal semantics of the ABS language

How to run the Maude backend

Running a model on Maude involves compiling the code, then starting Maude with the resulting file as input.

Compiling all files in the current directory into Maude is done with the following command:

$ absc -maude *.abs -o model.maude

The model is started with the following commands:

$ maude
Maude> in model.maude
Maude> frew start .

This sequence of commands starts Maude, then loads the compiled model and starts it. The resulting output is a dump of the complete system state after execution of the model finishes.

In case of problems, check the following:

  • absc should be in the path; check the PATH environment variable.

  • absfrontend.jar should be in the environment variable CLASSPATH.

14.2. Erlang Backend

The Erlang backend runs ABS models on the Erlang virtual machine by translating them into Erlang and combining them with a small runtime library implementing key ABS concepts (cogs, futures, objects, method invocations) in Erlang.

Executing an ABS model in Erlang currently returns the value of the last statement of the main block; output via ABS.Meta.println is printed on the console. More introspective and interactive capabilities are planned and will be implemented in the future.

How to run the Erlang backend

Running a model in Erlang involves compiling the ABS code, then compiling and running the resulting Erlang code.

Compiling all files in the current directory into Erlang and starting the resulting model is done with the following commands:

$ absc -erlang *.abs
$ gen/erl/run

This sequence of commands starts Erlang, then compiles the generated Erlang code and starts it. Type gen/erl/run -h for a list of options accepted by the model.

14.3. Haskell Backend

The Haskell backend translates ABS models to Haskell source code, consequently compiled through a Haskell compiler and executed by the machine. The backend, albeit a work in progress, already supports most ABS constructs and, above that, augments the language with extra features, such as Type Inference, Foreign Imports and real Deployment Components.

Type Inference

With the feature of Type Inference enabled, the user can optionally leave out the declaration of types of certain expressions; the backend will be responsible to infer those types and typecheck them in the ABS program. The type inference is safe, in the sense that it will not infer any wrong types (soundness property).

To make use of this feature, the user puts an underscore _ in place of where a type would normally be, as in this ABS block of code:

{ _ x = 3;
  Int y = 4; // type inference is optional
  x = x+y;
  _ l = Cons(x, Cons(y, Nil));
  _ s = length(l) + 4; }
At the moment, the type inference cannot infer interface types as in _ o = new Class();. It can however infer all the other types, that is Builtin, Algebraic, and Exception data types. There is a plan to support this in the future.
Foreign Imports

The Haskell backend extends the ABS module system with the ability to include Haskell-written code inside the ABS program itself. This feature is provided by the foreign_import keyword, which syntactically follows that of the normal import keyword. To illustrate this:

module Bar;
foreign_import Vertex from Data.Graph;
foreign_import vertices from Data.Graph;

the programmer has imported the Vertex algebraic datatype and the vertices function from the Data.Graph Haskell library module into an ABS module named Bar. Any imported Haskell term will be treated as its ABS counterpart. In the example case, the programmer may re-export the foreign terms or use them as normal ABS terms:

  Graph g = empty_graph();
  List<Vertex> vs = vertices(g);
At the moment, the ABS programmer can reuse (with foreign_import) Haskell’s Algebraic Data types and Pure functions, but not monadic IO code (Haskell code with side-effects). This restriction is planned to be lifted in a later release of the backend.
Deployment Components

The Haskell backend implements the ABS feature of Deployment Components, faithfully as described in Chapter 8. The backend follows the view that Deployment Components are virtual machines running in the Cloud. As such, each single DC corresponds to one Cloud virtual machine (VM).

Two DC classes (implementations) are provided to support the OpenNebula and Microsoft Azure cloud computing platforms accordingly:

class NebulaDC(CPU cpu, Mem memory) implements DC {
class AzureDC(CPU cpu, Mem memory) implements DC {

The CPU and Mem datatypes are passed as arguments when creating the DC to parameterize its computing resources. These datatypes are simple defined as type synonyms to Int, but you can expect more sophisticated resource encodings for a future backend release.

type CPU = Int; // processor cores
type Mem = Int; // RAM measured in MB
The backend has only been developed on and tested against the OpenNebula platform. This hopefully will change when more cloud providers will be supported.

How to obtain and install

The compiler itself is written in Haskell and distributed as a normal Haskell package. Therefore to build abs2haskell you need either

1) a recent release of the Haskell platform (version >= 2013.2.0.0),

2) the GHC compiler accompanied by the Cabal packaging system:

  • GHC compiler (version >=7.6)

  • Cabal package (version >=1.4)

  • cabal-install program. The compiler depends on other community packages/libraries. This program will automatically fetch and install any library dependencies.

Downloading, building and installing the compiler

Clone the repository with the command:

$ git clone git://

To build and install the abs2haskell bakend run inside the abs2haskell/ directory:

sudo make install

How to run the Haskell backend

After installing the compiler, you should have the program abs2haskell under your PATH.

Examples of running:

$ abs2haskell Example.abs

# An ABS program may have multiple main blocks in different modules.
# So you have to specify in which module is the main block you want to build with

$ abs2haskell --main-is=Example.abs Example.abs

$ abs2haskell examples/   # will compile all ABS files under examples directory

The compiler will generate ".hs" files for each compiled ABS module. No other runtime system libraries and dependencies will be generated.

The final step before running the ABS program is to compile the generated Haskell code to machine code, as the example:

ghc --make -threaded Example.hs # put the generated haskell file that has the main block here
Running the final program
./Example -O # means run it on 1 core with default optimizations
./Example -O +RTS -N1 # the same as the above
./Example -O +RTS -N2 # run it on 2 cores
./Example -O +RTS -N4 # run it on 4 cores
./Example -O +RTS -NK # run it on K cores

14.4. KeY-ABS Backend

KeY-ABS is a proof checker for ABS models. It can be downloaded from

The KeY-ABS backend is currently under development and unfinished.

The KeY-ABS backend can be used to generate invariants from annotations in the ABS source code. A design goal is to support annotations written in familiar ABS syntax; some invariants that can be expressed in KeY syntax proper might not be expressible in the ABS-flavored annotation syntax.

This backend is a work-in-progress and under active development.


  • Class invariants over Integer-typed fields

Limitations / Future Work:

  • Support of other datatypes in invariants

  • Support of ABS functions in invariants

  • Support of pre- and postconditions of methods, in interfaces and classes

Expressing a class invariant

A class Invariant is a Boolean condition over the object’s fields. It is written using an Inv annotation in the following way:

module Account;
export *;

interface Account {
	Int getAid();
	Int deposit(Int x);
	Int withdraw(Int x);
	Int withdrawAsync(Int x);

	Bool transfer(Int amount, Account target);


[Inv: balance >= 0 && aid >= 0] (1)
class AccountImpl(Int aid, Int balance) implements Account {

    Int getAid() { return aid; }
    [Pre: x >= 0]
    Int deposit(Int x) { balance = balance + x; return balance;}
    Int withdraw(Int x) {
	if (balance - x >= 0) {
	    balance = balance - x;
	return balance;

    Int withdrawAsync(Int x) {
	Fut<Int> resFut = this!withdraw(x);
	await resFut?;
	return balance;

    Bool transfer(Int amount, Account target) {
	Bool success = False;
	if (balance - amount >= 0) {
	    Fut<Int> newBal = this!withdraw(amount);
	    await newBal?;
	    Fut<Int> result = target!deposit(amount);
	    await result?;
	    success = True;
	return success;

	new AccountImpl(1,1);
1 The Inv annotation defines a class invariant expressing that balance and aid must be non-negative integers

How to run the KeY-ABS backend

Proving the correctness of a model involves generating the invariants, then running KeY-ABS with the resulting file as input.

Generating invariants for all files in the current directory is done with the following command:

$ absc -keyabs *.abs -o model.inv

This generated file can then be used with KeY-ABS in the usual way.