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.

Non-goals

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)

CursiveText

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

( )

Grouping

2.1. Line Terminators and White Spaces

Line terminators and white spaces are defined as in Java.

Syntax

LineTerminator ::=

\n | \r | \r\n

WhiteSpace ::=

LineTerminator | | \t | Comment

2.2. Comments

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.

Syntax

Comment ::=

LineComment | BlockComment

LineComment ::=

// { ? characters except LineTerminator ? } LineTerminator

BlockComment ::=

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

Example
// 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.

Example
/* 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).

Syntax

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.

adds

after

assert

await

builtin

case

catch

class

core

data

def

delta

die

else

exception

export

extends

features

finally

from

get

hasField

hasInterface

hasMethod

if

implements

import

in

interface

let

local

modifies

module

new

null

original

product

productline

recover

removes

return

skip

suspend

this

throw

trait

try

type

uses

2.5. Literals

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

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

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

The null literal is written as null.

Syntax

Literal ::=

IntLiteral | StringLiteral | ThisLiteral | NullLiteral

IntLiteral ::=

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

StringLiteral ::=

" { ? Valid String Character ? } "

ThisLiteral ::=

this

NullLiteral ::=

null

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.

Syntax

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 toolchain. Pre-defined annotations are usually type-checked.

Example
[Near] class Example { ... }

This is an example of annotations with a tag:

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

The same annotations, written in separate brackets:

Example
[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 (>).

Syntax

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.

Example
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

Unit

The empty (void) type

Unit

Unit

Bool

Boolean values

True, False

Boolean values

Int

Integers of arbitrary size

0, -15

Numbers

Rat

Rational numbers

1/5, 22/58775

Numbers

String

Strings

"Hello world\n"

Strings

Fut<A>

Futures

 — 

The Future Type

Exception

Exceptions

DivisionByZeroException

[exception-type]

List<A>

Lists of values of type A

list[1, 2, 3]

Lists

Set<A>

Sets of values of type A

set[True, False]

Sets

Map<A,B>

Maps from type A to B

map[Pair(1, True)]

Maps

Pair<A,B>

Pairs of values

Pair(1, True)

Pairs

Triple<A,B,C>

Triples of values

Triple(1, "hi", True)

Triples

Maybe<A>

Optional values

Just(True), Nothing

Optionals

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

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

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

Syntax

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

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

Accessor Functions

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

The name of an accessor function must be unique in the module it is defined in. It is an error to have 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.

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

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

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

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

Example
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 behaviour of the program, that should be treated (handled) separately compared to normal values.

Exceptions are declared with the keyword exception. Exceptions are of type ABS.StdLib.Exception, which is pre-defined in the standard library.

Syntax

ExceptionDecl ::=

exception SimpleTypeIdentifier ;

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

Example
exception MyException;

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

Unlike normal datatype constructors, exceptions cannot take arguments yet. This feature is planned for a future version of ABS.

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.

Syntax

TypeSynDecl ::=

type SimpleTypeIdentifier = Type ;

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

Syntax

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.

Syntax

PureExp ::=

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

Literal Expressions

Literals, as defined in Literals, are expressions.

Operator Expressions

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

Syntax

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

left

Bool

Bool

e1 && e2

logical and

left

Bool

Bool

e1 == e2

equality

left

compatible

Bool

e1 != e2

inequality

left

compatible

Bool

e1 < e2

less than

left

compatible

Bool

e1 <= e2

less than or equal to

left

compatible

Bool

e1 > e2

greater than

left

compatible

Bool

e1 >= e2

greater than or equal to

left

compatible

Bool

e1 + e2

concatenation

left

String

String

e1 + e2

addition

left

number

number

e1 - e2

subtraction

left

number

number

e1 * e2

multiplication

left

number

number

e1 / e2

division

left

number

Rat

e1 % e2

modulo

left

number

Int

!e

logical negation

right

Bool

Bool

-e

integer negation

right

number

number

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.

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

The Let Expression

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

Syntax

LetExp ::=

let ( Type SimpleIdentifier ) = PureExp in PureExp

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

Syntax

DataConstrExp ::=

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

Example
True
Cons(True, Nil)
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.

Syntax

FnAppExp ::=

Identifier ( [ PureExp { , PureExp } ] )

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

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

Syntax

FnAppListExp ::=

Identifier [ [ PureExp { , PureExp } ] ]

The Conditional Expression

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

Syntax

IfExp ::=

if PureExp then PureExp else PureExp

Example
if 5 == 4 then True else False

Case Expressions

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

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

It is an error if no pattern matches the expression.

There are four different kinds of patterns available in ABS:

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

  • Literal Patterns (e.g., 5)

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

  • Underscore Pattern (_)

Syntax

CaseExp ::=

case PureExp { { CaseExpBranch } }

CaseExpBranch ::=

Pattern => PureExp ;

Pattern ::=

_ | SimpleIdentifier | Literal | ConstrPattern

ConstrPattern ::=

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

The Variable Pattern

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

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

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

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

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

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

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

Typing of Case Expressions

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

4.2. Expressions with Side Effects

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

Syntax

EffExp ::=

NewExp | SyncCall | AsyncCall | GetExp

New Expression

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

Syntax

NewExp ::=

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

Example
new local Foo(5)
new Bar()

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

Synchronous Call Expression

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

Syntax

SyncCall ::=

PureExp . SimpleIdentifier ( PureExp { , PureExp } )

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

Syntax

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.

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

Syntax

GetExp ::=

PureExp . get

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

Example
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 get the result in one expression.

Syntax

AwaitExp ::=

await AsyncCall

Example
A x = await o!m();

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

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

5. Function Definitions

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

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

Syntax

FunctionDecl ::=

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

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

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

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

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

6. Statements

This chapter specifies all ABS statements.

Syntax

Statement ::=

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

Syntax

SkipStmt ::=

skip ;

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

Syntax

VarDeclStmt ::=

Type SimpleIdentifier [ = Exp ] ;

Example
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:

Example
{
    [Final] Int constant_i = 24;
    constant_i = 25;
}

6.3. Variable Assignment

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

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

Syntax

AssignStmt ::=

[ this . ] SimpleIdentifier = Exp ;

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

Syntax

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.
Example
server!operate();
new Client(server);

6.5. Assertions

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

Syntax

AssertStmt ::=

assert PureExp ;

Example
assert x != null;

6.6. Await Statement

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

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

Syntax

AwaitStmt ::=

await Guard ;

Guard ::=

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

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

Syntax

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.
Example
suspend;

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.

Syntax

ReturnStmt ::=

return Exp ;

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

6.9. Throw

The statement throw signals an exception (see Exceptions). It takes a single argument which is the exception value to throw.

Syntax

ThrowStmt ::=

throw PureExp ;

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

Syntax

Block ::=

{ { Statement } }

Semantically, a whole block is a single statement and can be written anywhere a single statement is valid.
Example
{
  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

Example
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, PatternMatchFailException is thrown.

For a description of the pattern syntax, see Case Expressions.

Syntax

CaseStmt ::=

case PureExp { { CaseStmtBranch } }

CaseStmtBranch ::=

Pattern => Stmt

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

6.13. The While Loop

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

Syntax

WhileStmt ::=

while ( PureExp ) Stmt

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

Syntax

ForeachStmt ::=

foreach ( Identifier ` in PureExp ) Stmt

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

Syntax

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

Example
try {
    Int 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
Example
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.

Syntax

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.

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

Syntax

ClassDecl ::=

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

{ [ FieldDeclList ] [ Block ] [RecoveryBlock] [ TraitUseList ][ MethDeclList ] }

ClassParameterList ::=

Type SimpleIdentifier { , Type SimpleIdentifier }

InterfaceList ::=

TypeIdentifier { , TypeIdentifier }

TraitUseList ::=

adds TraitName ; { adds TraitName ;}

FieldDeclList ::=

{ Type SimpleIdentifier [ = PureExp ] ; }

RecoveryBlock ::=

recover { { Pattern => Stmt } }

MethDeclList ::=

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 superinterfaces 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.
Example
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.

Example
class Sample {
    Int field = 12;

    {
        field = this.m();
    }

    [Atomic] Int m() {
        return 24;
    }
}

8.2. Constant Fields

Similar to variable declarations, field declarations 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 a compile-time error since we are trying to assign a new value to constant_i:

Example
class Sample {
    [Final] Int constant_i = 24;
    Unit m() {
        constant_i = 25;
    }
}

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

9. Traits

ABS does not support inheritance for code reuse. Method implementations that are common betwen 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.

Syntax

TraitDecl ::=

trait TraitName = ( { MethDeclList } | TraitName ) TraiOper*

TraitName ::=

SimpleIdentifier

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.

Explanation
  • 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:

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

The following two examples are valid:

Example
trait T = {Unit myMethod(){ skip; }} modifies {Unit myMethod(){ original(); }}
class C {uses T; }
Example
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 refered too

  • All traits used within a delta, in the order they are refered too

Example
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

Syntax

ModuleDecl ::=

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

Export ::=

export IdentifierList [ from TypeIdentifier ] ;

| export \* [ from TypeIdentifier ] ;

Import ::=

import IdentifierList [ from TypeIdentifier ] ;

| import * from TypeIdentifier ;

IdentifierList ::=

AnyIdentifier { , AnyIdentifier }

AnyIdentifier ::=

Identifier | TypeIdentifier

Decl ::=

FunDecl | TypeSynDecl | DataTypeDecl | 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:

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

Example
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:

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

Example
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,

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:

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

Operators

The following operators apply to Boolean values:

Expression Meaning Associativity Argument types Result type

e1 || e2

logical or

left

Bool, Bool

Bool

e1 && e2

logical and

left

Bool, Bool

Bool

e1 == e2

equality

left

compatible

Bool

e1 != e2

inequality

left

compatible

Bool

e1 < e2

less than

left

compatible

Bool

e1 < = e2

less than or equal to

left

compatible

Bool

e1 > e2

greater than

left

compatible

Bool

e1 >= e2

greater than or equal to

left

compatible

Bool

! e

logical negation

right

Bool

Bool

~ e

logical negation (deprecated)

right

Bool

Bool

11.2. Numbers

Datatypes and constructors

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

Operators

Expression Meaning Associativity Argument types Result type

e1 == e2

equality

left

compatible

Bool

e1 != e2

inequality

left

compatible

Bool

e1 < e2

less than

left

compatible

Bool

e1 < = e2

less than or equal to

left

compatible

Bool

e1 > e2

greater than

left

compatible

Bool

e1 >= e2

greater than or equal to

left

compatible

Bool

e1 + e2

addition

left

number, number

number

e1 - e2

subtraction

left

number, number

number

e1 * e2

multiplication

left

number, number

number

e1 / e2

division

left

number, number

Rat

e1 % e2

modulo

left

number, number

Int

Functions

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

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

Rat abs(Rat x)
truncate

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

Int truncate(Rat a)
numerator

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

Int numerator(Rat a)
denominator

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

Int denominator(Rat a)
pow

This function calculates b to the power of n.

Rat pow(Rat b, Int n)
sqrt_newton

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

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

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.

Operators

Expression Meaning Associativity Argument types Result type

e1 == e2

equality

left

compatible

Bool

e1 != e2

inequality

left

compatible

Bool

e1 < e2

less than

left

compatible

Bool

e1 < = e2

less than or equal to

left

compatible

Bool

e1 > e2

greater than

left

compatible

Bool

e1 >= e2

greater than or equal to

left

compatible

Bool

e1 + e2

concatenation

left

String, String

String

Functions

toString

This function converts any data into a printable string representation.

def String toString<T>(T t)
substr

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

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

def Int strlen(String str)
println

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

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.

Example
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:

Example
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.
DivisionByZeroException

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

AssertionFailException

The assert keyword was called with False as argument

PatternMatchFailException

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

NullPointerException

A method was called on null

StackOverflowException

The calling stack has reached its limit (system error)

HeapOverflowException

The memory heap is full (system error)

KeyboardInterruptException

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

ObjectDeadException

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.

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

Functions

head

Returns the head of a list.

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

Returns the tail (rest) of a list.

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

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

def Int length(List<A> l);
isEmpty

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

def Bool isEmpty(List<A> l);
nth

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

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

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

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

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

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

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

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

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

Returns a list of length n containing p n times.

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

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

Functions

contains

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

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

Returns True if set xs is empty, False otherwise.

def Bool emptySet<A>(Set<A> ss);
size

Returns the number of elements in set xs.

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

Returns a list with all elements in set xs.

def List<A> elements<A>(Set<A> xs);
union

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

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

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

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

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

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

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

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

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

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

Iterating through a map can be done via iterating over its set of keys, obtained via the keys function.

Datatypes and Constructors

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

Functions

emptyMap

Returns True if the map is empty, False otherwise.

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

Returns a map with the first occurrence of key removed.

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

Returns a list of all values within the map.

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

Returns a set of all keys of the map.

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

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

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

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

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

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

Functions

fst

The function fst returns the first value in a pair.

snd

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

Functions

fstT

The function fstT returns the first value in a triple.

sndT

The function sndT returns the second value in a triple.

trdT

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;

Functions

isJust

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

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

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. Timed ABS

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

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

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

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

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

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

  • the process is suspended waiting for time to advance

  • the process is waiting for some resources

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

12.1. Datatypes and Constructors

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

data Time = Time(Rat timeValue);

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

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

Syntax

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!
Examples
  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

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

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

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

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

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

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

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

method

String

Name of the method executed by the process

arrival

Time

Time when method call was issued

The attributes cost, procDeadline, 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.

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

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

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

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

14. 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 resoures 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.

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

delayed

yes

no

no

Invoke methods

delayed

yes

no

no

Process keep running

-

yes

yes/no

-

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 shutownInstance

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.

Methods

setInstanceDescriptions

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

This method returns the map of named instance configurations.

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

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.

prelaunchInstanceNamed

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.

launchInstance

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.

prelaunchInstance

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.

acquireInstance

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

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.

shutdownInstance

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

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

It is an error to try to create a deployment component via new local.
Example
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.

Methods

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

Unit decrementResources(Rat amount, Resourcetype rtype)

Decrease the total avilable amount for the given resourcetype by amount from the next time interval onwards. Trying to decrement infinite resources has no effect. It is an error to decrement resources by more than the available amount.

Unit incrementResources(Rat amount, Resourcetype rtype)

Increase the total avilable amount for the given resourcetype by amount from the next time interval onwards. Trying to increment infinite resources has no effect.

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

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

(This method is implemented via decrementResources and incrementResources.)

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

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

Speed

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.

Example
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

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:

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

Memory

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.

Cores

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

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

Example
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 resourcers 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.

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

15.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' TypeId [DeltaParams] ';' [ModuleAccess] ModuleModifier*
ModuleModifier ::= 'adds' ClassDecl
                 | 'removes' 'class' TypeName ';'
                 | 'modifies' 'class' TypeName
                   ['adds' TypeId (',' TypeId)*] ['removes' TypeId (',' TypeId)*]
                   '{' Modifier* '}'
                 | 'adds' InterfaceDecl
                 | 'removes' 'interface' TypeName ';'
                 | 'modifies' 'interface' TypeName '{' InterfaceModifier* '}'
                 | 'adds' FunctionDecl
                 | 'adds' DataTypeDecl
                 | 'modifies' DataTypeDecl
                 | 'adds' TypeSynDecl
                 | 'modifies' TypeSynDecl
                 | 'adds' Import
                 | 'adds' Export

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

Modifier ::= 'adds' FieldDecl
           | 'removes' FieldDecl
           | TraitOper

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

DeltaParam ::= Identifier HasCondition*
             | Type Identifier

ModuleAccess ::= 'uses' TypeId ';'

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

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

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

Class parameters and init block

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

Deltas

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

Modules

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.

15.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 productline, defining valid combinations of features and valid ranges of parameters for cost, capacity and number of machines:

root Calculations {
  group oneof {
    Wordcount,
    Wordsearch
  }
}

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

root Deployments {
  group oneof {
    NoDeploymentScenario,
    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);

15.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 behaviour. The configuration defines, for each selection of features satisfied by the product selection, which delta modules should be applied to the core. Furthermore, it guides the code generation by ordering the application of the delta modules.

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

Features and delta modules are associated through application conditions (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 productline:

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

Here are some product definitions for the CharityOrganizationExample with ProductExpr:

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

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

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

Deployment

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

FLI

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

Table 4. Backend Capabilities
Backend Maude Erlang Haskell Java

Real-Time ABS

yes

yes (deadline implementation missign)

-

-

User-defined Schedulers

yes

partial

-

-

Resource Models

yes

yes

-

-

Deployment

-

-

yes

?

FLI

-

-

yes

planned

Model API

-

yes

-

-

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

Features:

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

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

The Model API

The Erlang backend supports querying a running model via exposing selected objects. Such exposed objects serve as “entry points” into the model; their state can be inspected and selected methods can be invoked via HTTP requests.

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. Remark that 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();
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.

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

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

Currently supported parameter types are:

  • Bool: encoded in the query string as literal upper- or lowercase true / false, e.g., ?p=True, ?p=true, ?p=False, ?p=false

  • Int: encoded in the query string as a string of digits, e.g., ?p=42

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

The method can have an arbitrary return type, which will be returned as a string via the ABS toString() function, except for the following cases.

The following value types are handled specially as return type of an exposed method:

  • Bool, encoded as a JSON boolean value

  • String, encoded as a JSON string value

  • Int, encoded as a JSON integer.

  • Rat, converted to a floating point number. The behavior is unspecified if the given value is outside of floating point range.

  • List<A> (for supported type A), encoded as a JSON list

  • Set<A> (for supported type A), encoded as a JSON list; guaranteed to contain no duplicate elements

  • Map<A, B> (for supported types A, B), encoded as a JSON object. Keys in the resulting JSON object are generated from their ABS counterpart via toString() since JSON only supports keys of type String.

  • Datatypes with at least one named constructor argument, or a constructor argument with HTTPName annotation: encoded as a JSON object mapping argument names to their value. The resulting map will not contain the values of unnamed / unannotated constructor arguments. When an argument is both named and annotated, the annotation takes precedence.

In the following example, a return value D("x") will be encoded as {"effective key": "x"}.

data D = D([HTTPName: "effective key"] String overriden);
Starting the Model API

When an ABS model is started with the -p parameter naming a port number, the model will listen on the specified port for requests. The model will keep listening indefinitely for requests after its main block and all running methods have terminated but can be stopped manually at any time.

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.

Invoking methods

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

The map has the following entries:

  • 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

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

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.

16.3. Haskell Backend

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

Type Inference

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

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

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

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

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

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

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

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

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

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

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

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

How to obtain and install

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

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

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

  • GHC compiler (version >=7.6)

  • Cabal package (version >=1.4)

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

Downloading, building and installing the compiler

Clone the repository with the command:

$ git clone git://github.com/bezirg/abs2haskell

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

sudo make install

How to run the Haskell backend

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

Examples of running:

$ abs2haskell Example.abs

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

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

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

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

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

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

16.4. KeY-ABS Backend

KeY-ABS is a proof checker for ABS models. It can be downloaded from http://www.key-project.org/key-abs/key-abs.zip.

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

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

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

Features:

  • Class invariants over Integer-typed fields

Limitations / Future Work:

  • Support of other datatypes in invariants

  • Support of ABS functions in invariants

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

Expressing a class invariant

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

Example
module Account;
export *;

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

	Bool transfer(Int amount, Account target);

}

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

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


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



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

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

How to run the KeY-ABS backend

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

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

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

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


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.