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

1.3. Error Propagation and Recovery in ABS

ABS models exceptional (unforeseen and erroneous) situations using exceptions. This section gives an overview of the language constructs that deal with exception propagation and recovery.

Exceptions occur when a process cannot continue normal execution, e.g., when trying to divide by zero or when no pattern in a case expression matches the given value. Exceptions can also be thrown by the modeler via the throw statement: Throw. Exceptions thrown implicitly or explicitly are propagated and handled in the same way.

The modeler can define new exceptions; see [exception-type].

Exceptions can be caught and handled locally, i.e., in a lexically enclosing try-catch-finally block in the same method (see Handling Exceptions with Try-Catch-Finally). In that case, the process continues execution and will eventually produce a return value to its future.

In case of an unhandled exception, the future of the process does not receive a return value; instead, it will propagate the unhandled exception to the caller (or any process that tries to get its value). When evaluating f.get on a future that carries an exception instead of a normal return value, the exception will be re-thrown; it can be handled as usual via try-catch or left to propagate up the call chain of futures.

Additionally, terminating a process in the middle of execution might leave its object in an inconsistent state. To recover from this, ABS uses recovery blocks (see Classes). Unhandled exceptions are handed to the recovery block, which can take appropriate action to re-establish the class invariant and/or send asynchronous messages to other objects.

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 integer literals, floating-point literals, string literals, and the null literal. Rational numbers are written using the division operator /, e.g., 1/4 for one quarter.

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

The null literal is written as null.


Literal ::=

IntLiteral | FloatLiteral | StringLiteral |

IntLiteral ::=

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

FloatLiteral ::=

[ IntLiteral ] . [: digit :] { [: digit :] } [ ( e | E ) [ - | + ] IntLiteral ]

StringLiteral ::=

" { ? Valid String Character ? } "

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. Annotations are enclosed in square brackets ([]).

There can be more than one annotation in one place. When annotating a place with more than one annotation, writing the annotations in separate pairs of brackets or separated by commas in one pair of brackets produces the same effect.


AnnotationFragment ::=

[ TypeIdentifier : ] PureExp

Annotation ::=

{ [ Annotationfragment { , AnnotationFragment } ] }

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

[Near] class Example { ... }

This is an example of annotations with a tag:

[Cost: 15, Deadline: Duration(20)] o!m();

The same annotations, written in separate brackets:

[Cost: 15] [Deadline: Duration(20)] o!m();

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 asynchronous method call o!m().

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; object references are typed by an interface that the object’s class implements. (Classes that do not implement any interfaces can be instantiated, and can interact with the rest of the system via their run method and constructor arguments.)

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 Description Example Documentation


The empty (void) type




Boolean values

True, False

Boolean values


Integers of arbitrary size

0, -15



Rational numbers

1/5, 22/58775



Floating-point numbers

0.5, 1.0e-15




"Hello world\n"





The Future Type






Lists of values of type A

list[1, 2, 3]



Sets of values of type A

set[True, False]



Maps from type A to B

map[Pair(1, True)]



Pairs of values

Pair(1, True)



Triples of values

Triple(1, "hi", True)



Optional values

Just(True), Nothing


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. Float is a distinct numeric type.

Support for floating-point calculations is under development; calculations resulting in Inf or NaN currently have unspecified runtime behavior.

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. The second constructor defines two accessor functions.
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 a function definition with the same name as an accessor function or to have multiple accessor functions with the same name, unless they belong to the same data type.

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. 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.4. Exceptions

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

Exceptions are declared with the keyword exception, followed by the name of an exception and an optional list of parameters. The semantics are the same as for defining data constructors; naming a parameter will create an accessor function (see Accessor Functions).


ExceptionDecl ::=

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

Like any other constructor or datatype name, exceptions always start with an upper-case letter.

Exceptions are of type ABS.StdLib.Exception, which is pre-defined in the standard library. It is possible to store exception values in variables of type Exception.

exception MyException;
exception MyOtherException(String param, Int); // no accessor for second param

In ABS, exceptions are first-class values; the user can construct exception-values, assign them to variables, pass them in expressions, etc. An exception can be thrown via the throw statement (see Throw) and be caught in a catch block (see Handling Exceptions with Try-Catch-Finally). Additionally, the object itself can recover its invariant after an uncaught exception in a process via its recovery block (see Classes).

3.5. 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 ::=

| this . SimpleIdentifier
| this
| null
| Literal
| LetExp
| DataConstrExp
| FnAppExp
| FnAppListExp
| ParFnAppExp
| 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




Rat or Float

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 evaluates 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 Partially-Defined-Function Call Expression

Calls to partially defined functions (see Partial Function Definitions) are similar to function call expressions, but have an additional prepended set of arguments.


ParFnAppExp ::=

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

ParFnAppParam ::=

| AnonymousFunction

AnonymousFunction ::=

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

map(toString)(list[1, 2])
filter((Int i) => i > 0)(list[0, 1, 2])

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.

If no pattern matches the expression, a PatternMatchFailException is thrown.

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 introduces 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 sub-expressions of expressions can only be pure expressions. This restriction simplifies the reasoning about expressions in the ABS modeling language.


EffExp ::=

| SyncCall
| AsyncCall
| GetExp
| AwaitExp

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 asynchronously 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 either the return value is available or an exception has occurred in the callee task. No other task in the COG can be activated while the current task is blocked by a get expression.


GetExp ::=

PureExp . get

Bool b = f.get;

If the future contains a normal return value, the value of the get expression is that value. If the future contains an exception thrown by the callee process, evaluating the get expression will throw the same exception. The value thrown by a get expression can be caught by try-catch as normal (see Handling Exceptions with Try-Catch-Finally).

The following example assigns the return value contained in f to the variable b. In case of any error, b is assigned False.

try b = f.get; catch { _ => b = False; }

Await Expression

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


AwaitExp ::=

await AsyncCall

A x = await o!m();

The statement above is equivalent to these three statements:

Fut<A> fx = o!m();
await fx?;
A x = fx.get;
Exception Propagation and the Await Expression

As explained in Section Get Expression, exceptions propagate from callee to caller via the get expression. An await statement will proceed once the callee process has finished, but an exception in the future will not be raised when executing the await statement. To align the await expression with that behavior, an exception will only be raised when the return value of a method call is used, e.g., by assigning it to a variable. Hence the following line of code will not raise an error even if the call to o!m() results in an exception:

await o!m();

Since the return value is ignored in the statement above, it is equivalent to these two statements:

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

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.

5.1. Partial Function Definitions

For reasons of simplicity and analyzability, ABS does not offer higher-order functions. On the other hand, many common patterns of functional programming are extremely useful, for example the well-known map, filter and fold higher-order functions. For this reason, ABS supports partial function definitions.

Partial function definitions are function definitions taking an additional set of parameters. These additional parameters can be either names of normal functions, or anonymous functions (see Anonymous Functions). Partial function definitions define a set of functions which only differ in function applications but share overall structure. Put another way, partial function definitions define second-order functions — functions that take first-order functions as arguments. Partially defined functions can be used inside functional code, but cannot be passed as parameters to other partial functions.

A partially defined function is called the same way as a normal function, with a separate argument list containing the functional arguments. For recursion inside the body of a partially defined function, omit the function parameter list.


PartialFunctionDecl ::=

def Type SimpleIdentifier [ < SimpleTypeIdentifier { , SimpleTypeIdentifier } > ]
( [ SimpleIdentifier { , SimpleIdentifier } ] )
( [ Type SimpleIdentifier { , Type SimpleIdentifier } ] )
= PureExp ;

// Simply applies a function fn to a value.
def B apply<A, B>(fn)(A value) = fn(a);

def Int double(Int x) = x * 2;

  // doubled = 4
  Int doubled = apply(double)(2);
def List<B> map<A, B>(f)(List<A> list) = case list { (1)
    Nil => Nil;
    Cons(x, xs) => Cons(f(x), map(xs)); (2)

def Int double(Int x) = x * 2;

  // doubled = [2, 4, 6]
  List<Int> doubled = map(double)(list[1, 2, 3]);
1 This definition of map is contained in the standard library.
2 Note the recursive call to map omits the function parameter list.
For each call of a partial function, a normal function definition is generated at compile time by replacing the functional parameters syntactically by the functions passed in the additional parameter list. This is done before type checking and after delta and trait flattening — any type mismatch and similar errors are caught afterwards during type checking. If multiple statements call a partially defined function with the same function-name arguments, only one expansion is generated.

5.2. Anonymous Functions

To reduce the need to declare a function with a new function name explicitly every time a partially defined function is called, ABS uses anonymous functions. Anonymous functions are only allowed in the first arguments list calls to partially defined functions.


AnonymousFunction ::=

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

An anonymous function specifies a number of parameters and an expression that may refer to the declared parameters.

The following example is equivalent to the previous example, but does not define the double function explicitly.

  List<Int> list = list[1, 2, 3];
  list = map((Int y) => y * 2)(list);

Anonymous functions can refer to variables and fields accessible in the context of the partial function call. (Since anonymous functions are not first-class values, no closure is created.)

  Int factor = 5;
  List<Int> list = list[1, 2, 3];
  list = map((Int y) => y * factor)(list);
  // list = [5, 10, 15]
Anonymous functions are inlined into the expansion of the partial function definition. Errors caused by wrong typing are caught after the expansion during the type checking of core ABS, but the expanded function definition has an annotation referring to the statement that caused the expansion, hence error reporting will be accurate wrt. the original source code.

6. Statements

This chapter specifies all ABS statements.


Statement ::=

| VarDeclStmt
| AssignStmt
| ExpStmt
| AssertStmt
| AwaitStmt
| SuspendStmt
| ThrowStmt
| ReturnStmt
| Block
| IfStmt
| CaseStmt
| WhileStmt
| ForeachStmt
| 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;

Constant Declarations

Variable and field declarations can carry a Final annotation. the effect of such an annotation is to forbid re-assignment to such variables.

The following example will lead to a compile-time error since we are trying to assign a new value to constant_i:

    [Final] Int constant_i = 24;
    constant_i = 25;

6.3. 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 evaluates 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 (evaluates to True). While the task is suspended, other tasks within the same COG can be scheduled.

Guards can wait for a futures to become resolved, for a Boolean condition over the object state to become true, or (in timed ABS) for a certain duration to pass.

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 or an exception).
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.
It is tempting to misuse the suspend statement for busy-waiting (while (!condition) suspend; doTheThing();). In all cases, it is better to await on the condition: await condition; doTheThing();.

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 statement throw signals an exception (see Exceptions). It takes a single argument of type ABS.StdLib.Exception, which is the exception value to throw.


ThrowStmt ::=

throw PureExp ;

  throw AssertionFailException;

Note that the 'throw' statement can only be used inside imperative code. Functional code that cannot return a value in all cases should use the Maybe datatype.

def Maybe<Int> f(Int x, Int y) = if (y < 0) then None else Just(x);

Furthermore, note that some built-in exceptions, like DivisionByZeroException and PatternMatchFailException can originate from functional code. See Predefined exceptions in the Standard Library for a list of built-in exceptions.

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

ABS has the standard conditional statement. The condition has to evaluate to a Boolean value.


IfStmt ::=

if ( PureExp ) Stmt [ else Stmt ]

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.

If no pattern matches the expression, a PatternMatchFailException is thrown.

For a description of the pattern syntax, 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 evaluates 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. The Foreach Loop

The foreach loop repeatedly executes its body with the loop variable bound to each element of the given list, in sequence. The rules for the loop variable follow the rules of local variable declarations in blocks: the loop variable cannot shadow an existing variable, but can use the same name as an object field.

Also see the second-order functions like map and filter in Section Lists for common list processing idioms.

ForeachStmt ::=

foreach ( Identifier in PureExp ) Stmt

foreach (i in list[1, 2, 3]) {
  println("i = " + toString(i));

6.15. Handling Exceptions with Try-Catch-Finally

Executing a statement can result in an exception, either explicitly signaled using the throw keyword or implicitly, for example by dividing by zero. The try-catch-finally statement is used to handle exceptions and resume normal execution afterwards.


TryCatchFinallyStmt ::=

try Stmt
catch ( { { CaseStmtBranch } } | CaseStmtBranch )
[ finally Stmt ]

The statement protected by try (which can be a block) is executed first. If no exception is thrown, execution continues with the optional finally statement, then with the next statement after the try-catch-finally statement.

If during execution of the statement protected by try an exception is thrown, it is matched one-by-one against the exception patterns defined in the catch block. The statement following the first matching pattern will be executed, as in the case statement (see Case: Pattern Matching). Execution continues with the optional finally statement, then with the statement following the try-catch-finally statement.

If during execution of the statement protected by try an exception is thrown that is not matched by any branch in the catch block, the exception is unhandled. In this case, first the optional finally statement is executed. If the try-catch-finally was protected by another try-catch-finally statement, the unhandled exception is passed on to this surrounding try-catch-finally statement. Otherwise, the current process terminates and its future is resolved by storing the unhandled exception. Any get expression on this future will re-throw the exception (see Get Expression). The object that ran the aborted process will execute its recovery block with the unhandled exception as parameter (see Classes).

try {
    Rat z = 1/x; (1)
} catch {
    DivisionByZeroException => println("We divided by zero"); (2)
} finally {
    println("Leaving the protected area"); (3)
1 If x is zero, this will throw an exception
2 Division by zero is handled here; other exceptions will be left unhandled
3 This statement is always executed

As a syntactic convenience, when matching only a single pattern, the braces around the catch block can be omitted.

try b = f.get; catch _ => b = False; (1)
1 A “catch-all” exception handler that sets b to a default value in case an unhandled exception was propagated via f
The finally block has the same restrictions as the class init and recovery blocks, i.e., it cannot contain processor release points (i.e., await or suspend), blocking expressions (i.e., get), or explicitly throw an exception via the throw statement.

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 } ] ) ;

Method declarations can carry an [Atomic] annotation. The compiler will statically check that any definitions for such methods do not contain suspension points (suspend and await statements).

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), blocking expressions (i.e., get), or explicitly throw an exception via the throw statement.

Classes have an optional recovery block. In case an uncaught exception occurs in a method, the exception is matched against the patterns given in the recovery block, and the associated statement(s) are executed. If the exception does not match any pattern in the recovery block, or if the recovery block itself raises an exception, the object is killed. Code in the recovery block has the same restrictions as in the init block.


ClassDecl ::=

class SimpleTypeIdentifier [ ( [ ClassParameterList ] ) ] [ implements InterfaceList ]
{ [ FieldDeclList ] [ Block ] [RecoveryBlock] [ TraitUseList ] { MethDecl } }

ClassParameterList ::=

Type SimpleIdentifier { , Type SimpleIdentifier }

InterfaceList ::=

TypeIdentifier { , TypeIdentifier }

TraitUseList ::=

adds TraitName ; { adds TraitName ;}

FieldDeclList ::=

{ Type SimpleIdentifier [ = PureExp ] ; }

RecoveryBlock ::=

recover { { Pattern => Stmt } }

MethDecl ::=

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

A class definition contains zero or more method definitions. Each method has a name, return type and zero or more parameters. All methods declared in an interface that is implemented by the class or one of their super-interfaces must be defined in the class body or in one of its traits. A class is free to define methods not declared in an interface; such methods are private to the class and cannot be called from outside the class.

ABS currently does not support method overloading. Each method must have a unique name since methods are not disambiguated by their parameter lists.
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...


8.1. Atomic Methods

Definitions for atomic method declarations have to be annotated with [Atomic] as well. The compiler will statically check that the definition does not contain suspension points (suspend and await statements) and blocking get expressions. Such methods can be called inside init blocks and in finally clauses; all other methods cannot be called in these places.

The following example shows a call to an atomic method from an init block. Removing the Atomic annotation from method m would lead to a compile-time error.

class Sample {
    Int field = 12;

        field = this.m();

    [Atomic] Int m() {
        return 24;

8.2. Constant Fields

Similar to variable declarations, field declarations and class parameters can carry a Final annotation. the effect of such an annotation is to forbid re-assignment to such a field.

The following example will lead to compile-time errors since we are trying to assign new values to two fields declared as Final:

class Sample ([Final] Int constant_i) {
    [Final] Int constant_j = 24;
    Unit m() {
        constant_i = 25; // error
        constant_j = 24; // error

In addition to fields, method parameters and variables can also be declared Final.

8.3. 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 asynchronously called after object initialization.

9. Traits

ABS does not support inheritance for code reuse. Method implementations that are common between classes can be defined once and used inside these classes by using traits. A trait can add, remove and modify methods of a class or of another trait.

Traits are applied to classes at compile-time and do not change the interface(s) of a class. Classes and their methods are type-checked once all traits are applied.

Similar to classes, traits in ABS are not types.


TraitDecl ::=

trait TraitName = ( { { MethDecl } } | TraitName ) { TraitOper }

TraitName ::=


TraitOper ::=

adds TraitExpr
| modifies TraitExpr
| removes MethSig

A trait is defined with trait t = T at module level.

The effect of applying a trait T to a class (using uses T inside the class body) is to add the methods in that trait to the class definition.

  • The operation adds adds all the elements of the next MethodSet to the class. If a method with the same name is already present in the class (or set of methods), the error will be raised after applying all traits, during type checking.

trait T = { Unit x(){ skip; } }
trait T2 = { Unit y(){ skip; } } adds T

will be resolved to the set

{ Unit x(){ skip; } Unit y(){ skip; } }
  • The operation modifies changes all the elements of the next MethodSet in the class to the new implementation described in this MethodSet. A trait may contain original() calls which refer to the version of the method before the trait application. If a method with the same name is not present in the class (or set of methods), the method is added instead and the original() calls are not resolved.

A method may contain targeted original calls. These raise an error if the trait is used directly by a class The following is invalid:

trait T = {Unit myMethod(){ skip; }}  modifies {Unit myMethod(){ core.original(); }}
class C {uses T; }

The following two examples are valid:

trait T = {Unit myMethod(){ skip; }} modifies {Unit myMethod(){ original(); }}
class C {uses T; }
module M;
trait T = {Unit myMethod(){ skip; }}
class C {uses T; }

delta D;
modifies class M.C{
        modifies Unit myMethod(){ core.original(); }
  • The operation removes deletes the method with the provided signature. If a method with the same name is not present in the class (or set of methods), an error will be raised during trait application.

The order of trait application is as follows:
  • All traits used within a class, in the order they are referred to

  • All traits used within a delta, in the order they are referred to

module M;
interface I { Unit x(); Unit foo(); Unit bar(); }
trait T = Unit x() { this.foo(); original(); this.bar();  }
trait T2 = { Unit x() { println("T2"); } } modifies T
trait T3 = { Unit x() { println("T3"); } } modifies T
class C implements I {
        Int i = 0;
        uses T2;
        Unit foo(){ i = i+1; }
        Unit bar(){ i = i-1; }

class C2 implements I {
        Int i = 0;
        uses T3;
        Unit foo(){ i = i-1; }
        Unit bar(){ i = i+1; }

10. 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.

10.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 ::=

| PartialFunctionDecl
| TypeSynDecl
| DataTypeDecl
| ExceptionDecl
| InterfaceDecl
| ClassDecl
| TraitDecl

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.

10.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;

10.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.

11. 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.

11.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




11.2. Numbers

Datatypes and constructors

The numeric datatypes of ABS are Int (arbitrary-length integers), Rat (arbitrary-precision rational numbers) and Float (64-bit floating point). See Built-in Types for their syntax.

Support for floating-point calculations is under development; calculations resulting in Inf or NaN currently have unspecified runtime behavior.


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

Rat or Float

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)

Converts an integer or rational number into a floating-point number.

Float float(Rat a)

Converts a floating-point number into a rational number.

Rat rat(Float f)

Returns the largest integer smaller or equal to the argument.

Int floor(Float f)

Returns the smallest integer larger or equal to the argument.

Int ceil(Float f)

Returns the numerator of a rational number, or the number itself for an integer.

Int numerator(Rat a)

Returns the denominator of a rational number, or 1 for an integer.

Int denominator(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)

This function returns the square root of x. It is an error if x is negative.

Float sqrt(Float x)

This function returns the natural logarithm of its argument.

Float log(Float x)

This function returns Euler’s number e raised to the power of x.

Float exp(Float x)

Returns an integer between 0 (inclusive) and its argument (exclusive).

Int random(Int below)

11.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)

11.4. Unit

Unit is the empty (void) datatype.

Datatypes and Constructors

Both the datatype and the single constructor are named Unit.

11.5. 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.

11.6. Predefined exceptions in the Standard Library

ABS provides pre-defined exceptions that are thrown in specific circumstances. See Exceptions for information about exceptions.

This list is subject to revision in future versions of ABS. Not all these exceptions are currently thrown by different backends in the described situation.

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 null


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


A method was called on a dead (crashed) object

11.7. Lists

A list is a sequence of values of the same type. Lists are constructed via the list constructor function, e.g., list[1, 2, 3] creates a list of three integers. An empty list is created via list[] or Nil.

The time to access a value via nth is proportional to the length of the list. The first value of a list can be accessed in constant time, using the head function.

The map, fold and filter second-order functions described in this section implement common functional programming patterns. To execute some statements for each element in a list, use a foreach loop (see The Foreach Loop).

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=length(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);

Applies a function to each element of a list, returning a list of results in the same order. The function fn must take an argument of type A and return a value of type B.

def List<B> map<A, B>(fn)(List<A> l);

Returns a list containing only the elements in the given list for which the given predicate returns True. The function predicate must take an argument of type T and return a Boolean value.

def List<T> filter<T>(predicate)(List<T> l);

Accumulates a value starting with init and applying accumulate from left to right to current accumulator value and each element. The function accumulate must take two arguments: the first of type A (the type of the list) and the second of type B (the accumulator and result type), and return a value of type B.

def B foldl<A, B>(accumulate)(List<A> l, B init);

Accumulates a value starting with init and applying accumulate from right to left to each element and current accumulator value. The function accumulate must take two arguments: the first of type A (the type of the list) and the second of type B (the accumulator and result type), and return a value of type B.

def B foldr<A, B>(accumulate)(List<A> l, B init);

11.8. Sets

A set contains elements of the same type, without duplicates. Sets are constructed via the set constructor function, e.g., set[1, 2, 2, 3] creates a set of three integers 1, 2, 3. The expression set[] produces the empty set.

To add an element to a set, use the function insertElement, to remove an element, use remove. To test for set membership, use the function contains.

The takeMaybe function can be used to iterate through a set. It is used as follows:

def Unit printAll<A>(Set<A> set) =
  case takeMaybe(set) {
    Nothing => println("Finished");
    Just(e) => let (Unit dummy) = println("Element " + toString(e)) in printAll(remove(set, e));

Datatypes and Constructors

The datatype for sets with elements of type A is Set<A>. The set constructor function is used to construct sets.



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 emptySet<A>(Set<A> ss);

Returns the number of elements in set xs.

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

Returns a list with all elements in set xs.

def List<A> elements<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> difference<A>(Set<A> set1, Set<A> set2);

Returns True if set contains all elements of maybe_subset, False otherwise.

def Bool isSubset<A>(Set<A> maybe_subset, Set<A> set);

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 non-empty set. It is an error to call take on an empty set; consider using takeMaybe in that case.

def A take<A>(Set<A> ss);

Returns one element from a set, or Nothing for an empty set.

def Maybe<A> takeMaybe<A>(Set<A> ss);

11.9. Maps

Maps are dictionaries storing a value for each key.

Maps are constructed using by passing a list of type Pair<A, B> to the map constructor function. The keys of the resulting map are of type A and values are of type B. The expression map[] produces an empty map.

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

Map<Int, String> m = map[Pair(1, "ABS"), Pair(3, "SACO")];
In case of duplicate keys, it is unspecified which value the map will contain for a given key.

The value associated with a key can be obtained using the lookup and lookupDefault functions.

A map can be iterated over via the functions keys, values and entries, which return the set of keys and the list of values and entries of the map, respectively.

Datatypes and Constructors

The datatype for a map from type A to type B is is Map<A, B>. The map constructor function is used to construct maps.



Returns True if the map is empty, False otherwise.

def Bool emptyMap<A, B>(Map<A, B> map);

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);

Returns a list of all entries (i.e., pairs of key and value) of the map.

def List<Pair<A, B>> entries<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);

11.10. 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.

11.11. 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.

11.12. 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);

12. The Model API

The Erlang backend supports querying a running model. When creating objects, an annotation HTTPName makes them available via HTTP requests from outside the model under the name given by the annotation. Methods that are annotated HTTPCallable can be invoked from the outside on such objects. Additionally, datatypes can be annotated to influence how they are converted to JSON when they are returned from such methods.

The model API is supported by the Erlang backend.

All queries in this section can be prepended with a /v2/ prefix, i.e., http://localhost:8080/v2/call instead of http://localhost:8080/call. In case incompatible changes have to be introduced to the Model API in the future, the semantics of invocations of queries with prefix /v2/ will be preserved.

12.1. Starting the Model API

When an ABS model compiled with the Erlang backend is started with the -p parameter naming a port number, the model will listen on the specified port for requests. In the following example, we compile a model my-model.abs and start the model API on port 8080:

$ absc -erlang my-model.abs
$ gen/erl/run -p 8080

12.2. Shutting down the Model API

When running a model with the model API activated, it will not return to the command line after the simulation has finished. Instead, the model will keep listening for requests and method calls.

A running model can be terminated manually from the console (for example, via pressing Ctrl-C), or by requesting the URL /quit. The following command will terminate a model running on port 8080:

$ curl localhost:8080/quit
curl: (52) Empty reply from server

12.3. Exposing objects

Objects are exposed via a HTTPName annotation. In the following example, two objects of class C are exposed with the names C1 and C2 respectively. The HTTPName annotation can be used on assignment statements, variable declarations and new expression statements.

[HTTPName: "C1"] new C();
[HTTPName: "C2"] I x = new C();

12.4. Exposing methods

In an interface declaration, a HTTPCallable annotation exposes the annotated method such that it is callable from outside, given an exposed object that implements that interface.

interface I {
  [HTTPCallable] String method(String param1, Int param2);

It is a compile-time error if the method takes parameters whose types are not supported.

ABS type URLencoded format JSON format


literal upper- or lowercase true / false: ?p=True, ?p=true, ?p=False, ?p=false

JSON boolean


a string of digits, e.g., ?p=42

JSON integer


a floating-point number, e.g., ?p=3.14

JSON float


URLEncoded text, e.g., ?p=Hello%20World!

JSON string

List<A> (where A can be decoded)

not supported

JSON list with elements of type A

All others

not supported

not supported

The method can have any return type. Method call results will be returned as a string via the ABS toString() function, except for the types enumerated in the following table.

ABS type JSON format


JSON boolean value


JSON string value


JSON integer


JSON float, via integer division. The behavior is unspecified if the Rat value is outside of floating point range.


JSON float


JSON list, with elements converted one-by-one per this table.


JSON list; guaranteed to contain no duplicate elements, with elements converted one-by-one per this table.

Map<A, B>

JSON object, with keys generated from their ABS counterpart via toString(), values converted per this table.

Datatype, with at least one named or annotated constructor argument

JSON object (see below)


Converted via ABS toString()

User-defined datatypes are encoded depending on the presence of accessor functions and HTTPName annotations. If the datatype definition contains neither, values will be encoded as strings via toString(). If at least one accessor function or HTTPName annotation is present, values will be encoded as objects, with the HTTPName annotation value (or accessor function name, if no annotation is present) as key. Unnamed constructor argument values will not be contained in the JSON object.

Table 4. Example of encoding of user-defined data types
ABS definition Sample JSON encoding

data D1 = D1(String, Int);

'D1("x", 1)', as per toString()

data D2 = D2(String key, Int);

{ 'key': 'x' }

data D3 = D3([HTTPName: "effective key"] String key, Int);

{ 'effective key': 'x' }

12.5. Querying object state

The following query returns the names of all exposed objects.

GET http://localhost:8080/o

Inspecting an object state directly can be useful for debugging. The following query returns a JSON map of the state of the object exposed as C1, with object fields as keys.

GET http://localhost:8080/o/C1

The following query returns a JSON map containing the value of C1’s `field, with "field" as key.

GET http://localhost:8080/o/C1/field

When querying for an unknown object or an unknown field, the HTTP request will produce a 404 response code.

All queries in this section can be prepended with a /v2/ prefix, i.e., http://localhost:8080/v2/o. In case incompatible changes are introduced to the Model API in the future, for example by introducing new return value encodings, reasonable effort will be made to keep the semantics of invocations of queries with prefix /v2/ unchanged.

12.6. Querying exported methods of an object

The following query returns, for an object exposed as C1, a JSON array of objects with metadata about callable functions.

GET http://localhost:8080/call/C1

Each entry in the resulting list will be a JSON object with the following keys:

  • name: the name of the exposed method

  • parameters: an array with one object per parameter, each with the following entries:

  • name: name of the parameter

  • type: type of the parameter

  • return: return type of the method

12.7. Invoking methods

Exposed methods are called by querying a URL of the form


Parameters are passed to methods either as query parameters in the URL or in a JSON map passed in as the body of a POST request. For duplicate arguments, parameter values in the URL override values given in the JSON body.

The following query produces the return value of the method call method("value", 50) by invoking it on the object exposed as C1.

GET http://localhost:8080/call/C1/method?param1=value&param2=50

This query can be invoked from the shell in two ways, using the curl command, either using query parameters or a JSON body:

$ curl http://localhost:8080/call/C1/method?param1=value\&param2=50
$ curl -d "{ 'param1': 'value', 'param2': 50 }" http://localhost:8080/call/C1/method

The following example shows how to call a method that takes a List<Int> called mylist from Javascript using the JQuery library:

    url: "call/Model/testConfig",
    type: "POST",
    data: JSON.stringify({ "mylist": [1,2,3] }),
}).done(function(result) {
    console.log("Result: " + JSON.stringify(result));

Care must be taken to disable timeouts on the HTTP client when querying for long-running methods in this way.

When querying for unknown objects or methods, the HTTP request will produce a 404 response code.

When querying with invalid method parameters, the HTTP request will produce a 400 response code.

When the invoked method throws an exception, the HTTP request will produce a 500 response code.

12.8. The Model API and Timed ABS

The simulated clock of Timed ABS (Timed ABS) is accessible via the Model API.

The current value of the clock can be obtained with the following request:

GET http://localhost:8080/clock/now

The result is a JSON object with a key 'value' mapping to the current value of the clock.

When the model was started with a clock limit (see Timed ABS and the Model API), the limit can be increased via a request like the following:

GET http://localhost:8080/clock/advance?by=50

This call will always increase the clock limit by the given amount, even if the clock had not yet reached the previous limit. I.e., when now() = 10 and the limit is 20, after the call the limit will be 70, the same as when the clock was already stopped at the limit of 20 when the call was received by the Model API.

12.9. Customizing the Browser-Based Visualization

Since the Model API is implemented via HTTP, it can be accessed from a web browser. The -http-index-file command-line switch is used to supply an index.html file at compile-time:

$ absc -erlang -http-index-file ./index.html *.abs

When running a model on port 8080 and accessing http://localhost:8080/ from a browser, the contents of that file will be displayed.

Sometimes it is necessary to add additional files for visualization, e.g., CSS files, images or JavaScript libraries. The contents of one directory can be added to the model via the -http-static-dir command-line switch:

$ absc -erlang -http-index-file ./index.html -http-static-dir ./support-files/ *.abs

The contents of the given directory are copied at compile-time. The files within that directory are available within the Model API below the static/ path. For example, a file ./support-files/js/d3.js will be accessible as http://localhost:8080/static/js/d3.js.

13. 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 infinitesimally small steps.

It is possible to assign deadlines to method calls. Deadlines are expressed in terms of a duration value relative to the current time and decrease as the clock advances. The current deadline of a method is available via the function deadline and decreases down to zero.

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 processes run as long as there is “work to be done.”

13.1. Datatypes and Constructors

Time is expressed as a datatype Time, durations are expressed using the datatype Duration, which can be infinite. These datatypes are defined in the standard library as follows:

data Time = Time(Rat timeValue);
data Duration = Duration(Rat durationValue) | InfDuration;

13.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 and can only occur in suspension points.

The function deadline returns the deadline of the current process.

def Duration deadline()

The initial value of a deadline is set via a Deadline annotation at the caller site.

Unit m() {
  [Deadline: Duration(10)] this!n(); (1)

Unit n() {
  Duration d1 = deadline(); (2)
  await duration(2, 2);
  Duration d2 = deadline(); (3)
1 The Deadline annotation assigns a deadline to the process started by the asynchronous method call
2 The process can query its current deadline; if no deadline is given, deadline returns InfDuration
3 d2 will be two time units less than d1

13.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

13.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.

13.5. Timed ABS and the Model API

By default, the clock will advance when all processes within the model are waiting for the clock. However, it is sometimes desirable to synchronize the internal clock with some external event or system, and therefore to temporarily block it from advancing beyond a certain value.

When starting a model, the erlang backend (Erlang Backend) supports a parameter -l x or --clock-limit x which stops the clock at the given value x. This makes it possible to model infinite systems up to a certain clock value. When the clock limit is reached, the model will terminate even if there are processes which would be enabled by further clock advancement.

When starting a model with both the -l and -p parameters (i.e., with both the model api and a clock limit), a request to the model api of the form /clock/advance?by=x will increase the clock limit by x, thereby causing waiting processes to run until the new limit is reached.

14. User-Defined Schedulers

User-defined schedulers are an experimental feature of Timed ABS. They are available on the Maude and Erlang backends. This section describes the current state of the implementation on the Erlang backend.

All identifiers introduced in this section reside in the ABS.Scheduler module, which is not imported by default.

14.1. Defining Schedulers

A scheduler is a function that takes a list of processes and chooses one of them. Schedulers are ordinary ABS functions.

The following two example schedulers illustrate the concept. The first, deterministic scheduler takes the first process off the list; the second scheduler chooses a non-deterministic one.

def Process defaultscheduler(List<Process> queue) = head(queue);

def Process randomscheduler(List<Process> queue) = nth(queue, random(length(queue)));

It is possible to formulate an Earliest Deadline First (EDF) scheduler in ABS:

def Process earliest_deadline_scheduler(List<Process> queue) =
  foldl((Process a, Process b) =>
      if durationLessThan(proc_deadline(a), proc_deadline(b)) // a < b
      then a else b)
    (queue, head(queue));

All schedulers must have a result type Process and must take an argument of type List<Process>.

Schedulers can have more than one argument; arguments after the first one will be filled with the value of object fields of the same name at scheduling time. This feature is currently available in the Maude backend only.

14.2. Processes and Process Attributes

A process is an ABS abstract datatype; i.e., there is no constructor available to create a Process value inside ABS. Processes are created by the runtime and handed to schedulers.

Processes have attributes which can be used by schedulers to choose the next process to run. For example, a scheduler could always prefer processes that run a certain method. The following attributes are available:

Name Type Meaning



Name of the method executed by the process



Time when method call was issued



The (current) deadline value of the process (InfDuration if none)

The attributes cost, start, crit are available in the Maude backend only but will be implemented in the Erlang backend as well. The attributes value, finish are under consideration since their usefulness is questionable.

14.3. Using Schedulers

Schedulers apply to cogs since cogs are responsible for scheduling one of their processes when idle. Since cogs are created via new expressions, a scheduler can be given at that point via an annotation. Classes can have a default scheduler that is given as an annotation to the class definition; any cog created when instantiating this class will have that scheduler by default (unless overridden by an annotation at the new expression).

The following example shows how to define a class that uses the randomscheduler by default. The first argument (the list of processes) must have the name queue.

[Scheduler: defaultscheduler(queue)] class C implements I {

The following example shows how to create a cog with a different scheduler.

   [Scheduler: randomscheduler(queue)] I instance = new C();

15. Deployment and Resource Modeling

This chapter describes how to model 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.

To simulate the effects of deployment decisions on the cost and performance of running a distributed system, the following aspects need to be added to a model:

  • A notion of location to describe where different parts of the system will run

  • A notion of cost of executing code on such locations; and finally

  • A notion of time that allows us to observe the effects of varying the location and cost.

In ABS, the following language elements implement these aspects:

Deployment Components

ABS cogs can be created on a deployment component (see Deployment Components). Deployment components have a limited number of resources available.

Resource Annotations

ABS statements can be annotated with resource costs (see Resource Types). Executing such annotated statements incurs resource costs.

Timed ABS

The time model of Section Timed ABS naturally extends to observations on resource usage.

These elements work together as in Figure Resource Consumption:

Resource Consumption
Figure 6. Resource Consumption

The figure shows a process with a skip statement with an associated cost of 5, followed by a println statement with a cost of 10. The deployment component DC has 10 resources available in each time interval.

At time t, the skip statement consumes the five needed resources and is successfully executed. The println statement consumes the remaining five resources but is not executed yet.

At time t+1, the deployment component’s resources are refilled. The five remaining resources of the println statement are consumed and the statement is executed. The five remaining resources of DC are not used.

At time t+2, the deployment component’s resources are again refilled to 10.

The rest of this chapter explains these language elements concerning resource modeling in detail. All identifiers introduced in this section reside in the ABS.DC module.

15.1. The CloudProvider API

Deployment components are usually managed by a Cloud Provider instance. The Cloud Provider implements the life cycle shown in Figure Deployment Component lifecycle. A deployment component is managed by a cloud provider if it was created via one of the launchInstance methods.

Deployment Component lifecycle
Figure 7. Deployment Component lifecycle

The operations supported by deployment components during their lifecycle are summarized in Table [table-dc-lifecycle].

State Starting Running Terminating Terminated

Create objects





Invoke methods





Process keep running





Using the CloudProvider

To use deployment components via a cloud provider, follow these steps:

  1. Create a CloudProvider instance

  2. Set the instance descriptions via the setInstanceDescriptions method

  3. Create deployment components using the launchInstanceNamed method

  4. (optional) Manage access via releaseInstance / acquireInstance

  5. (optional) Release deployment components via shutdownInstance

module ProviderDemo;
import * from ABS.DC;

    CloudProvider p = new CloudProvider("Amazon");
    await p!setInstanceDescriptions(
        map[Pair("T2_MICRO", map[Pair(Memory,1), Pair(Speed,1)]),
            Pair("T2_SMALL", map[Pair(Memory,2), Pair(Speed,1)]),
            Pair("T2_MEDIUM", map[Pair(Memory,4), Pair(Speed,2)]),
            Pair("M4_LARGE", map[Pair(Memory,8), Pair(Speed,2)])]);
    DeploymentComponent dc = await p!launchInstanceNamed("T2_SMALL");
    // ... use the deployment component ...

Datatypes and Constructors

The type for cloud provider instances is ABS.DC.CloudProvider.

Cloud provider instances are created with a new CloudProvider(String name) expression. It is not mandatory but recommended that each cloud provider instance has a unique name.

It is recommended to call setInstanceDescriptions once after creating a cloud provider to set the list of named instance types that this cloud provider offers.



This method sets the named instance configurations that the cloud provider instance should support. These names are used in the methods launchInstanceNamed and prelaunchInstanceNamed.

[Atomic] Unit setInstanceDescriptions(Map<String, Map<Resourcetype, Rat>> instanceDescriptions);

This method returns the map of named instance configurations.

[Atomic] Map<String, Map<Resourcetype, Rat>> getInstanceDescriptions();

This method creates and returns a new deployment component with a resource configuration corresponding to instancename, as set by the setInstanceDescriptions method. If no description for instancename exists, launchInstanceNamed returns null.

DeploymentComponent launchInstanceNamed(String instancename);

The name of the new deployment component will be "<Cloud provider name>-<instancename>-<Counter>", i.e., a concatenation of the name of the cloud provider itself, the instance name, and a unique integer as suffix.

If the instance description specifies a startup duration, launchInstanceNamed will only return after that amount of simulated time has elapsed.

The returned deployment component will be acquired (as per acquireInstance) and can be used immediately.


This method creates and returns a new deployment component with a resource configuration corresponding to instancename, as set by the setInstanceDescriptions method. If no description for instancename exists, prelaunchInstanceNamed returns null.

DeploymentComponent prelaunchInstanceNamed(String instancename);

As with launchInstance, the name of the new deployment component will be "<Cloud provider name>-<instancename>-<Counter>", i.e., a concatenation of the name of the cloud provider itself, the instance name, and a unique integer as suffix.

The method prelaunchInstanceNamed returns immediately, but the method acquireInstance, when called on the returned deployment component, will not return before its startup duration (if specified) has elapsed.

The returned deployment component needs to be acquired (as per acquireInstance) before it can be used.


The launchInstance method creates and returns a new deployment component with the specified resource configuration. It can be used when, for whatever reason, the resource configuration should not be registered with the cloud provider, but the deployment component should still be managed by it.

DeploymentComponent launchInstance(Map<Resourcetype, Rat> description);

The name of the new deployment component will be "<Cloud provider name>-<Counter>", i.e., a concatenation of the name of the cloud provider itself and a unique integer as suffix.

If the resource configuration specifies a startup duration, launchInstanceNamed will only return after that amount of simulated time has elapsed.

The returned deployment component will be acquired (as per acquireInstance) and can be used immediately.


This method creates and returns a new deployment component with the specified resource configuration. As with launchInstance, this method can be used when, for whatever reason, the resource configuration should not be registered with the cloud provider, but the deployment component should still be managed by it.

DeploymentComponent prelaunchInstance(Map<Resourcetype, Rat> d)

The name of the new deployment component will be "<Cloud provider name>-<Counter>", i.e., a concatenation of the name of the cloud provider itself and a unique integer as suffix.

The method prelaunchInstance returns immediately, but the method acquireInstance, when called on the returned deployment component, will not return before its startup duration (if specified) has elapsed.

The returned deployment component needs to be acquired (as per acquireInstance) before it can be used.


This method, together with releaseInstance, implements exclusive access to a deployment component. After acquireInstance returns true, all further invocations will return false until releaseInstance is called for the deployment component.

Bool acquireInstance(DeploymentComponent instance);

If the deployment component passed as argument was not created by the cloud provider, the method returns false.

The methods acquireInstance and releaseInstance are used to implement exclusive access in a cooperative manner. Attempting to create a cog on a deployment component without having acquired it beforehand will not lead to a runtime error; ensuring exclusive access to deployment components is the responsibility of the modeler.

This method releases the deployment component, such that the next call to acquireInstance will return true.

Bool releaseInstance(DeploymentComponent instance);

This method returns true if the deployment component was successfully released. It returns false if the deployment component was already not acquired.

If the deployment component passed as argument was not created by the cloud provider, the method returns false.


This method shuts down a deployment component. The effect on the cogs, objects and running tasks deployed on that deployment component are backend-specific.

Bool shutdownInstance(DeploymentComponent instance);

[Atomic] Rat getAccumulatedCost();

[Atomic] Map<String, Map<Resourcetype, Rat>> getInstanceDescriptions();

15.2. 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.

A deployment component and its cogs
Figure 8. A deployment component and its cogs

Deployment Components are first-class constructs in the ABS language. References to deployment components can be stored in variables of type DeploymentComponent, and the methods documented in this section can be called via asynchronous method calls.

Deployment Components are usually created by a cloud provider instance (see The CloudProvider API), but can also be created using the new expression. A new cog is created on a deployment component by using a DC annotation to the new statement.

If no DC annotation is given for a new statement, the fresh cog (and its first object) are created on the same deployment component as the current cog.

It is an error to try to create a deployment component via new local.
DeploymentComponent dc = await provider!launchInstance(map[Pair(Speed, 10)]); (1)
[DC: dc] Worker w = new CWorker(); (2)
1 The cloud provider provider creates a new deployment component dc with 10 Speed resources
2 A new cog containing a CWorker object is created on the new deployment component dc
All objects of a cog must reside on the same deployment component, i.e., [DC: x] new local C() is an error.

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 the given resource type rtype over the last n periods. If the deployment component was created with infinite resources for the given resource type, load returns 0.

[Atomic] InfRat total(Resourcetype rtype)

Return the total available amount for the given resourcetype. If the deployment component was created with infinite resources for the given resource type, total returns InfRat, otherwise Fin(value).

[Atomic] Rat decrementResources(Rat amount, Resourcetype rtype)

Decrease the total available amount for the given resourcetype by amount from the next time interval onwards. Trying to decrement infinite resources has no effect. Trying to decrement by more than available will decrement the maximum amount possible. Returns the amount by which the resource was decreased.

[Atomic] Rat incrementResources(Rat amount, Resourcetype rtype)

Increase the total available amount for the given resourcetype by amount from the next time interval onwards. Trying to increment infinite resources has no effect. Returns the amount by which the resource was increased.

[Atomic] Rat 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. Returns the amount transferred, which will be lower than amount in case the deployment component has less resources available.

(This method is implemented via decrementResources and incrementResources.)

[Atomic] String getName()

Returns the name of the deployment component. Deployment components created via a CloudProvider are guaranteed to have a unique name if no two cloud providers have the same name.

[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 (price) 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] CloudProvider getProvider()

Get the cloud provider that manages this deployment component. Returns null if the deployment component was not created by a cloud provider. 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. See The CloudProvider API for a discussion of cloud providers.

Bool release()

Convenience method for calling releaseInstance of the associated cloud provider. If no cloud provider is set, returns True. See The CloudProvider API for a discussion of cloud providers.

15.3. Resource Types

The term “Resource” can be understood in different ways. In ABS, we define “Resource” to be a countable, measurable property of a deployment component. Some resources stay constant throughout the life of a deployment component (e.g., the number of cores), some others are influenced by program execution (e.g., the available bandwidth in the current time slot).

The resource types currently supported by the ABS language are defined in the ABS.DC module as follows:

data Resourcetype = Speed | Bandwidth | Memory | Cores ;

When a deployment component is created without explicitly giving a value for a resource type, it is assumed to have an infinite amount of that resource. E.g., when modeling a denial of service attack, the deployment component running the attacker code will have infinite speed and bandwidth.


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

Time t1 = now();
[Cost: 5] skip;
Time t2 = now();

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, i.e., t1 and t2 might be different.


Bandwidth is a measure of transmission speed. Bandwidth resources are consumed during method invocation and return statements. No bandwidth is consumed if sender and receiver reside on the same deployment component.

Bandwidth consumption is expressed via a DataSize annotation:

Time t1 = now();
[DataSize: 2 * length(datalist)] o!process(datalist);
Time t2 = now();

Executing the above method invocation statement will consume bandwidth resources proportional to the length of list datalist.


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).

15.4. Modeling Resource Usage

As described above, resource information is added to statements of an ABS model using Cost and DataSize annotations. Executing such annotated statements causes observable changes in the simulated time and deployment component load during simulation.

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

  DeploymentComponent dc = new DeploymentComponent("Server",
    map[Pair(Speed, 5), Pair(Bandwidth, 10)]);
  [DC: dc] I i = new C();
  [DataSize: 5] i!process(); (3)
1 Make all necessary identifiers accessible in the current module
2 Executing this statement costs 10 Speed units; the time needed depends on the capacity of the deployment component, and on other cogs executing in parallel on the same deployment component.
3 Executing this method call consumes 5 Bandwidth resources. Since dc has 10 bandwidth resources per time unit, the message will be transported instantly. Executing the skip statement in the method body will not finish instantaneously because dc only has 5 Speed resources in total.

16. Software Product Line Engineering

ABS supports the development of software product lines with a set of language constructs for defining system variants. Following a feature-oriented software development approach, variants are described as sets of features. Features and their dependencies are specified in a feature model. Each feature has its corresponding ABS implementation. A feature’s implementation is specified in terms of the code modifications (i.e., additions and removals) that need to be performed to a variant of the system that does not include that feature in order to add it. This style of programming is called delta-oriented programming. The ABS code modules that encapsulate feature implementations are called delta modules (deltas).

16.1. Delta-Oriented Programming

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 SimpleTypeIdentifier [ ( DeltaParam { , DeltaParam } ) ] ;
{ ModuleAccess } { ModuleModifier }

DeltaParam ::=

Type SimpleIdentifier
| QualifiedTypeIdentifier HasCondition

HasCondition ::=

hasField FieldDecl
| hasMethod MethSig
| hasInterface TypeId

ModuleAccess ::=

uses TypeId ;

ModuleModifier ::=

adds ClassDecl
| removes class TypeIdentifier ;
| modifies class TypeIdentifier
  [adds TypeIdentifier { , TypeIdentifier } ]
  [removes TypeIdentifier { , TypeIdentifier } ]
  { { ClassModifier } }
| adds InterfaceDecl
| removes interface TypeIdentifier ;
| modifies interface TypeIdentifier { { InterfaceModifier } }
| adds FunctionDecl
| adds DataTypeDecl
| modifies DataTypeDecl
| adds TypeSynDecl
| modifies TypeSynDecl
| adds Import
| adds Export

ClassModifier ::=

adds FieldDecl
| removes FieldDecl
| adds Method
| modifies Method
| removes MethodSig

InterfaceModifier ::=

adds MethSig
| removes MethSig

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 modifications to classes and interfaces in several modules by fully qualifying the TypeName of module modifiers.

While delta modeling 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.

16.2. The Feature Model

Software variability is commonly expressed using features which can be present or absent from a product of the product line. Features are defined and 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 variants that can be built.

Specifying 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 product line, 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);

16.3. Software Product Lines and Products

A (software) product line is a set of software variants that can be built by selecting any combination of features allowed by the feature model and applying the deltas that provide the implementation for those features to the core program. How features are associated with their implementation is defined in ABS with a SPL configuration.

An ABS product is simply a set of features associated with a name.

Specifying the Product Line

The ABS configuration language links feature models, which describe the structure of a SPL, to delta modules, which implement behavior. 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 (a.k.a. activation 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 product line:

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

Checking the SPL

Because the number of variants in an SPL can be very large, checking them efficiently (e.g., to ensure that they are all well-typed) is challenging. Building each variant in order to type-check it is usually not feasible from a performance perspective. Instead, the ABS compiler employs a number of efficient consistency checks. These fall into two categories.

  • Family-based analysis steps operate on the SPL definition itself,

  • Analysis steps operate on lightweight abstractions of the SPL variants.

These checks are performed automatically upon compilation and help ensure that all variants defined by an SPL specified in ABS can be built and are well-typed ABS programs.

17. 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 5. Backend Capabilities
Backend Maude Erlang Haskell Java

Real-Time ABS


yes (deadline implementation missing)



User-defined Schedulers





Resource Models















Model API





17.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.

17.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.StdLib.println is printed on the console. For additional introspective and interactive capabilities, the Erlang backend supports a Model API (see below).

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.

Generating code coverage information

The Erlang backend can optionally generate code coverage information in a format inspired by gnu gcov (see https://gcc.gnu.org/onlinedocs/gcc/Invoking-Gcov.html). The coverage information contains line numbers and execution count, but not the source code itself. This is sufficient for some tools to visualize code coverage, e.g., cov-mode for Emacs (https://github.com/AdamNiederer/cov).

To generate code coverage information, compile an abs model with the -cover switch, then run it as normal, i.e.,

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

For each .abs file, running the model will generate a .abs.gcov file in the directory gen/erl/absmodel after the simulation finishes.

17.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 type-check 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://github.com/bezirg/abs2haskell

To build and install the abs2haskell backend 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

1. This ordering is not guaranteed to be stable between two invocations of a program. If ABS ever develops object serialization, care must be taken to uphold any datatype invariants across program invocations, e.g., when reading back an ordered list of objects.