The Jass Page

Documentation

Trace-Assertions

[English] printer friendly version

1 Foreword

The documentation of Trace-Assertions serves as a tutorial to learn the basic concepts of Trace-Assertions in Jass. Since the subject of Trace-Assertions is rather complex, the tutorial does not encompass any aspect of the subject. It concentrates on selected issues to give the reader the idea what Trace-Assertions are and how they can be used to improve Software-Engineering.

The documentation is part of the mastersthesis of Michael Plath.

The mastersthesis serves as a reference of Trace-Assertions in Jass. The concept of Trace-Assertions was invented by Clemens Fischer, who describes his concept at his PhD Thesis.

2 Introduction

Trace-Assertions are a new feature of Jass 2.0. They help to specify the dynamic behaviour of your program at runtime. Trace-Assertions lay down the order of valid method invocations. Furthermore a method invocation can be bound to certain conditions.

Here comes a simple example of what a Trace-Assertion looks like:

init().b -> init().e -> start().b -> start().e.

It says that the method start() can only be invoked after init() finished its execution: The suffix '.b' indicates the begin of a method. '.e' indicates end accordingly. Thus the assertion describes a sequence of method calls. It forbids nested calls like:

public void init() {
 start();
}

If you want to allow nested calls you should modify the above expression:

init().b -> start().b -> start().e -> init().e.

init().b -> init().e can be abbreviated to init(). So the first example can also be written as

init() -> start().

The runtime package of Jass checks for every method call if any Trace-Assertion of the program is violated. If so, the program is stopped and a Trace-Assertion exception is thrown. In addition the trace stack is dumped. This helps you as a programmer to determine the reason of the abnormal program execution.

A sequence of method calls is called a Trace. In the first example init() start() is a valid Trace while init() init() leads to a Trace-Assertion violation.

3 Trace-Assertions are class invariants

Since Trace-Assertions describe the global behaviour of class instances, they are part of the class invariant. To identify an assertion as a Trace-Assertion the keyword trace is used. The following code shows how Trace-Assertions are written in Jass:

/** invariant
 [AssertionName] trace (
  ...
 );
**/

Remember that class invariants must allways be at the end of a sourcefile.

4 Basic Processes

Trace-Assertions contain one ore more declarations of processes. A process describes the valid behaviour of a program at runtime. In the context of Trace-Assertions the term 'process' has a special meaning and must not be mixed up with a Java process (Thread).

Jass knows three Basic Processes which describe a program's behaviour:

  1. STOP - no further method invocations are allowed
  2. ANY - any method invocation is allowed
  3. TERM - the actual object must terminate

Remark: The realization of TERM has a more theoretical background. While TERM is a mapping this.finalize() -> STOP the following documentation is restricted to the two Basic Processes STOP and ANY.

5 Trace-Alphabet

To understand the semantics of the Basic Processes look at the following Trace-Assertion:

trace(
 init() -> STOP
);

While «init() init()» is no valid Trace, «init() start()» is valid. This may suprise you, because the semantics of STOP says "no further invocations". However the invocation of start() is possible, because the Trace-Assertion does not know the method start(). The checking mechanism of a Trace-Assertion is limited by a finite Trace-Alphabet. The Trace-Alphabet may be determined implicitly or set explicitly. In the above example the Alphabet consists of the two entries init().b and init().e. If you want to extend the alphabet you must set it explicitly:

/** invariant
      trace{init(), start()}  /# explicit Trace-Alphabet #/
        ( 
          init() -> STOP 
        )
 **/

The Alphabet sets the scope of a Trace-Assertion. When a certain method is not in scope of a Trace-Assertion T, T will have no effect on this method at runtime (a call of this method).

In the above example the alphabet is given by a simple enumeration. Moreover you can use common wildcards to define the alphabet. The following examples give you the idea how wildcards can be used for the Trace-Alphabet.

this.*
All methods of the belonging class
* EXCEPT init()
All methods, but init()
{public A.*, public B.*}
All public methods of class A and B
m(*)
All methods with name m with no consideration for method parameters
m(?)
All methods with name m with just one parameter
m(int, ?, *)
All methods m with at least two parameters. First parameter must be of the type 'int'.

A further description of possible abstractions with wildcards is not subject of this documentation. You may find help reading the Jass grammar. A complete description of this issue can be found at the #WorkPlath#.

6 Processes

As mentioned before the valid behaviour of a program is described by process declarations. Look at the following example of a Trace-Assertion:

/** invariant
 trace{public this.*} (
  MAIN() {
   STOP
  }
 );
**/

This example shows a declaration of a process named MAIN. While the declaration only consists of the Basic Process STOP the semantics of MAIN is equal to the semantics of STOP. The process named MAIN has a special meaning. It marks the starting point of every Trace-Assertion. Assume that the above Trace-Assertion is defined in a Java class C. Then the meaning of the Trace-Assertion is "No public methods of class C may be invoked". Probably there is no domain for this kind of Trace-Assertion. But look at the following Trace-Assertion:

/** invariant  trace{public this.*} (
  MAIN() {
   init() -> CALL Initialized()
  }

  Initialized() {
   * EXCEPT init() -> CALL Initialized()
  }
 );
**/

Here a second process 'Initialized' is declared. MAIN refers to 'Initialized' by using the CALL-Operator . 'Initialized' refers to itself and creates a local loop. The meaning of the Trace-Assertion can be described as follows:

  1. The first method call must be init()
  2. After init() no further invocation of init() is allowed

In more abstract terms one may say "The class must be initialized correctly".

7 Operators for Choice and Parallelism

The previous examples of Trace-Assertions limited the program flow to a single sequence of method invocations. To overcome this limitation Jass provides an operator to define branches or 'choice points'. A branch is expressed by the choice-operator <|>. The choice-operator symbolizes a branch by showing two arrows pointing to the left and to the right.

The following process shows an expression which has the meaning "After a() either b() or c() may be invoked".

MAIN() {
 (a() -> b() -> STOP) <|> (a() -> c() -> STOP)
}

To underline the character of the choice-operator the following declaration shows the same expression using the CALL-operator.

MAIN() {
 CALL P() <|> CALL Q()
}

P() {
 a() -> b() -> STOP
}

Q() {
 a() -> c() -> STOP
}

In general P() and Q() can be arbitrary processes which describe certain properties of your program's behaviour. Because of the choice-operator either P() or Q() must be satisfied. If your program should satisfy more than one property you may want to say that P() and Q() must be satisfied. You achive this goal by using the parallel-operator |<>|. The operator symbolizes that the current path is splitted into two new paths.

So what is the semantics of the above example if we use the parallel-operator instead of the choice-operator?

MAIN() {
 CALL P() |<>| CALL Q()
}

P() {
 a() -> b() -> STOP
}

Q() {
 a() -> c() -> STOP
}

With the choice-operator the valid Traces were:

Now we have also

The parallel-operator yields a conjunction of expressions. It got its name, because it instantiates more than one process in parallel to check the current Trace-Assertion. To make this clearer we give a equivalent to the above example using two independent assertions:

/** invariant
 trace (
  MAIN() {
   a() -> b() -> STOP
  }
 );

 trace (
  MAIN() {
   a() -> c() -> STOP
  }
 );
**/

You may use this alternative if your program's properties are static and can be described as single Trace-Assertions.

8 Variables

You may have noticed that the syntax of a process declaration is derived from a method declaration in Java. Moreover a process can be called by another process using the CALL-Operator like a method is called at runtime of a Java program. The similarity between processes and Java methods goes even further: process declarations can have arguments and processes may have variables. The following example shows a propagation of the string value "initalized" from the process MAIN to the process Q.

MAIN() {
 init() -> CALL P("initialized")
}

P(String status) {
 m() -> CALL Q(status)
}

Q(String status) {
 String msg = "Status:" + status;

 n() -> ...
}

Process Q declares a local variable msg. Local variables must allways be declared at the beginning of the process declaration.

As long as you cannot operate on the variables, declaring variables is useless. There are three possibilities how variables come in use.

  1. Certain method invocations can depend on conditions. Variables can be used to store information about the actual program state to define complex conditions
  2. Processes can execute arbitrary Java code. In connections with conditional method invocations a method invocation can be bound to any condition which can be expressed with the Java language. A second important ability is the printing of status messages
  3. Variables can be used to define branches within processes (if-else)

9 Conditional method invocations

Due to Trace-Assertions any method invocation at runtime of a program can be bound to certain conditions. To distinguish the ability from usual assertions (pre- and postconditions) we emphasize that any method invocation can have a certain condition. Consider a trace m() m(). A Trace-Assertion can demand different conditions for each call of m. A usuall assertion does not distinct these two calls. This is why the concept of Trace-Assertions is called dynamic, while usual assertions are rather static.

The real power of conditional method invocation can not be revealed until we present the concept of exchanging data between a Trace-Assertion and the running program. However we will present here an academical example of a condition to give insight in this feature.

MAIN() { CALL Counter(0) }

Counter(int num) {
 m() WHERE(num <3)
 ->  CALL Counter(num + 1)
}

The meaning of this example is: "method m may at most be invoked three times". The condition given after the keyword WHERE must hold before the body of m is executed. Remember that m() stands for an abbreviation of m().b -> m().e. Thus the condition is related to m().b.

10 Execution of Java code

Trace-Assertions offer the feature of executing arbitrary Java code depending on the state of your program. This is possible for two main purposes:

  1. To allow complex boolean expressions for conditional method invocations
  2. To follow your program's state by writing status messages (monitoring)

Here we give a simple example how Trace-Assertions can be used to monitor the state of your program.

MAIN() {
 EXECUTE(System.out.println("init");)
 -> init() -> ANY
}

The invocation of init() causes the message "init" to be print to the default output stream. You may ask whether "init" is printed before or after the execution of init(). To answer this question we must remind that init() stands for (init().b -> init().e). Thus the printing of "init" appears before (at the begin) of the execution of init(). If you want to be informed when the initialization is over you should write:

MAIN() {
 EXECUTE(System.out.println("initialized");)
 -> init().e -> ANY
}

The execution of java code is linked to the following method call: in the example above we wrote EXECUTE(...) -> init().e and not init().e -> EXECUTE. This will come clearer if you look at the next example (as an abbreviation we us prt instead of System.out.print:

MAIN() {
 a() -> EXECUTE(prt("#");) ->
 (EXECUTE(prt("b");) -> b() -> STOP
 <|> EXECUTE(prt("c";) -> c() -> STOP)
}

What kind of messages do we expect of this kind of Trace-Assertion? Consider the trace a() b(). After the execution of a() no message will be printed. The second invocation b() yields the message "#b".

11 Branches - If/Else

Trace-Assertions can have branches. The following code fragment shows a possible branch structure:

IF(b) {
  CALL P()
} ELSE {
  CALL Q()
}

Branches allow to express complex dynamical behaviour of a program. For a more eloquent example read the next section.

12 Data exchange

Till now it seems that method calls were only interpreted by their signature. E.g. a method call m("", true) was interpreted as "a method with name m and first argument of type String and second of type Boolean". This is loss of information, because the argument values are not known (in the example: 'empty string' and 'true').

Trace-Assertions offer a mechanism to overcome this loss of information. In general speaking it is possible to exchange (argument) values between the running program and the guarding Trace-Assertion. If the Trace-Assertion should have access to the argument value a preceding '?' is used:

?s

In more detail, the above example could look like:

MAIN() {
 String s;
 boolean b;

 m(?s, ?b) WHERE(s != null) -> CALL Q(b)
}

When you use the notation '?x', x must allways be a process variable. Hence x must be declared. In the example above s is declared as type String and b is declared as type boolean. The notation m(?s, ?b) yields the signature m(String, boolean).

The notation '?x' is called data exchange, because the value of the underlying argument is passed from the program to the process variable x. It is also possible to pass a value from the process to the running program. Unlike passing from program to process this kind of data exchange needs a special interpretation. A Trace-Assertion is a guard which restricts the possible behaviour of the running program. Thus the Trace-Assertion should be able to restrict the possible values of the arguments of a method call. A strong restriction is m("x") which expresses that only 'x' is a valid value for the call of m. A more general notation is m(!x). Here the two values of x and the argument of m must coincide.

The following processes P,Q,R demonstrate different applications of data exchange. They are all equivalent in semantics.

P() {
 m(7) -> STOP
}

Q() {
 int i = 7;
 m(!i) -> STOP
}

R() {
 int i;
 m(?i) WHERE(i == 7) -> STOP
}

You can specify the result value of a method call as well. If m is a method which returns a boolean value, ?b m() passes the return value to the variable b (assuming that b is declared as boolean). Accordingly !b m() restricts the return value to the value of b.

You have to be carefull if you refer to the result value and use a conditional method at the same time. If you want to express that a method m should return 'true' the following Trace-Assertion is wrong:

P() { /# Caution #/
 boolean b = false;
 ?b m() WHERE(b) -> CALL Q()
}

The WHERE-expression will be evaluated at the beginning of the method call m (at the top of the method body). At this point the result value of m is not known yet and the value of b is false (initial value). If you want to refer to the result value right after the method execution you should use a If/Else expression:

P() {
 boolean b = false;
 ?b m() -> IF(!b)
  CALL E()
 } ELSE {
  CALL Q()
}

E() {
 EXECUTE(throw new RuntimeException();) -> STOP
}