Exceptions & Goto

This section discusses support for exceptions and goto in VerCors. The following topics are discussed:

• The support that is currently implemented and support that is still being worked on is listed here.
• Then a brief summary of exceptions in Java is given here.
• Then we discuss the signals contract clause here, which models exceptions in VerCors.
• Finally, support for goto is discussed here.

Exceptions

Support

VerCors currently only supports Java exceptions. They are not supported in PVL. We also do not support signal handlers in C. The table below lists which facets of exceptions in Java are currently supported in VerCors.

Feature	Supported
throw	Yes
throws	Yes
try-catch	Yes
try-finally	Yes
try-catch-finally	Yes
try-with-resources	No
Multi-catch	No
Defining custom exceptions	Yes, but only if directly inheriting from one of: Exception, RuntimeException, Throwable, Error. This limitation is temporary.
JML signals	Yes
JML signals_only	No

Support for exceptions is still being worked on currently. Progress on the implementation can be followed here.

Java Exceptions Example

We will now discuss a basic artificial example of exception usage in Java. For a more thorough overview, we refer the reader to the Java tutorial on exceptions: https://docs.oracle.com/javase/tutorial/essential/exceptions/index.html.

In the following code example, the find method determines if an array contains a specific integer value:

class MyFind {
    public static boolean find(int[] xs, int value) throws Exception {
        for (int i = 0; i < xs.length; i++) {
            if (xs[i] == value) {
                return true;
            } else if (xs[i] < 0) {
                throw new Exception();
            }
        }

        return false;
    }

    public static void main(String[] args) {
        int[] myXs = int[3];
        myXs[0] = 1;
        myXs[1] = 10;
        myXs[2] = -3;
       
        try {
            find(myXs, 22);
        } catch (Exception e) {
            System.out.println("An error occurred");
        }
    }
}

If the find method encounters a negative array element while searching, it throws an exception. The fact that the method throws an exception at all is indicated by the throws Exception modifier when the find method is defined. Specifically, the exception is thrown by the throw new Exception() statement in the find method.

The thrown exception is handled in the main method by wrapping the call to find in a try-catch block. Whenever an exception is thrown within a try-catch block, the exception is passed to the catch block of the type of the exception that matches the type of the catch block. This catch block can then handle the exception to allow the program to continue, or perform cleanup such that the program can exit safely. If none of the catch blocks can handle the exception, it is passed further up the call stack, possibly terminating the program if it is not caught and handled.

The signals clause

The signals clause supported in VerCors is very similar to the signals clauses supported in JML (documented here). It is a contract element like requires or ensures, and declares the postcondition in case an exception is thrown. The declared postcondition holds when the thrown type matches the type stated in the signals clause. When an exception is thrown, normal ensures post-conditions never hold, and instead only relevant signals clauses hold.

As an artificial example, we can define a signals clause for a method that sums two numbers. The method throws an exception if one of the numers is equal to five.

//@ signals (Exception e) a == 5 || b == 5;
//@ ensures \result == (a + b);
void sum(int a, int b) throws Exception {
    if (a == 5 || b == 5) {
        throw new Exception();
    } else {
        return a + b;
    }
}

Similar to the throws attribute, the signals clause can name both checked and unchecked exceptions. The only limitation is that the type must extend Throwable.

Signals does not guarantee an exception

A frequently occurring use-case is to guarantee that an exception is thrown, if a certain condition occurs. Furthermore, this is also how the semantics of the signals clause is sometimes misinterpreted. Applying this line of though to the previous example, one might expect the method sum to always throw if one of the arguments equals five. However, this is not the case. The implementation for pickySum below demonstrates this. The implementation for pickySum also satisfies the contract for sum, but clearly pickySum does not always throw an exception if one of the arguments equals 5:

//@ signals (Exception e) a == 5 || b == 5;
//@ ensures \result == (a + b);
void pickySum(int a, int b) {
    if ((a == 5 || b == 5) && dayOfTheWeek() == "tuesday") {
        throw new Exception();
    } else {
        return a + b;
    }
}

Instead, pickySum only throws an exception if one of the arguments equals five, and today is tuesday. Would pickySum be called on a monday with 5 and 10, an exception would not be thrown, and instead 15 would be returned.

This artificial example shows how a signals clause should be interpreted: when an exception of the appropriate type is thrown, the signals clause can be assumed to hold. We call this the "reactive" semantics.

It is not guaranteed that an exception is thrown if a signals condition occurs. We call this the "causal" semantics. VerCors does not implement this currently.

If needed, there is a way to model the causal semantics using an additional ensures clause. To do this, an ensures clause needs to be added that implies false when the signals condition occurs. For example, pickySum can be made consistent as follows:

//@ signals (Exception e) a == 5 || b == 5;
//@ ensures (a == 5 || b == 5) ==> false;
//@ ensures \result == (a + b);
void consistentSum(int a, int b) {
    if (a == 5 || b == 5) {
        throw new Exception();
    } else {
        return a + b;
    }
}

By ensuring that the method cannot terminate normally if one of the arguments equals 5, it is guaranteed that an exception is thrown when one of the arguments equals 5. This encodes the causal semantics using the reactive semantics supported by VerCors.

Exception guarantees

Java guarantees that methods only throw checked exceptions if they are explicitly mentioned in the throws attribute. Unchecked exceptions can always be thrown.

VerCors does not implement this exact semantics. Instead, it assumes that any exception that can be thrown is mentioned in either the throws attribute or in a signals clause. In other words, if a method has no throws clauses, nor signals clauses, it is 100% exception safe according to VerCors. A downside of this is that the VerCors exception semantics does not 100% reflect the Java semantics. The upside is that VerCors can now guarantee that all specified exceptions are caught, as all relevant exceptions are stated explicitly.

For example, if a method does not have a signals clause stating it throws a RuntimeException, VerCors assumes this exception will never be thrown by the method. Another example, if a throw new RuntimeException() statement occurs in method M, VerCors will give an error if M does not have a signals clause for RuntimeException.

In some situations it might be necessary to opt into the more realistic Java semantics of unchecked exceptions. VerCors does not support this directly, but it can be moddeled with an additional signals clause. To do this, an additional signals clause must be added with the condition true. For example, we can modify the contract of the earlier presented sum method to allow throwing a RuntimeException randomly:

//@ signals (ArithmeticException e) a == 5 || b == 5;
//@ signals (RuntimeException e) true;
//@ ensures \result == (a + b);
void sum(int a, int b) {
    if (a == 5 || b == 5) {
        throw new ArithmeticException();
    } else {
        return a + b;
    }
}

void useSum() {
    int result = sum(5, 10);
    System.out.println("Result: " + result);
}

If this example is checked by VerCors, it will yield an error in the useSum method. The error will complain that sum might throw a RuntimeException, but that it is not specified in the contract nor handled in the useSum body.

A way to resolve this would be to catch the RuntimeException by wrapping the call to sum in a try-catch block. However, since catching a RuntimeException is bad practice, it is sometimes better to indicate in the contract of useSum that useSum might also throw a RuntimeException. This propagates the responsibility for handling the unchecked exception to the caller.

The signals_only clause

The signals_only clause from JML (documented here) is not supported by VerCors. It guarantees that the only types that will be thrown by the method are the types listed in the signals_only clause.

To simulate the functionality of signals_only T1, ..., Tn, a signals clause with the condition true can be added for each Ti. For example, the clause signals_only T1, T2; can be simulated by adding two signals clauses to a method contract as follows:

//@ signals (T1 e) true;
//@ signals (T2 e) true;
void m() {
    
}

Alternatively, the abbreviation of signals_only documented in Section 9.9.5 of the JML reference manual can also be used to approximate the semantics of signals_only in VerCors.

Goto and labels

PVL has support for goto and label. They are useful for modeling control flow primitives not yet supported in VerCors. The semantics are standard: when the goto l statement is encountered, control flow is immediately transferred to the location indicated by the label l. For example, the following program verifies:

int x = 3;
goto l;
x = 4;
label l;
assert x == 3;

As PVL does not have a construct like finally in Java, there are no exceptions for the semantics of goto in PVL.

One example where use of goto might lead to confusing results is the following. In the below example, goto is used to exit the while loop. Because goto redirects control flow to the destination label immediately, checking the loop invariant is skipped.

int r = 10;
loop_invariant r == 10;
while (true) {
  r = 20;
  goto lbl2;
}
assert r == 10; // Never executed
label lbl2;
assert r == 20;

If it is desired that the loop invariant is checked at goto as well, this can be modeled by adding asserts at the exit labels of the while loop.