Eclipse Project Instructions

Contents

1  Introduction

Welcome! We’d like to thank you again for bidding on this project.

You will be given a small program, and your job is to describe the conditions that are necessary to prevent the program from crashing. For example, a Java program crashes if it dereferences null (a NullPointerException) or uses an illegal array index (an ArrayIndexOutOfBoundsException). If a method in the program dereferences its argument, then you would write a specification that says that the method’s argument must not be null.

To perform this task, you will write Java-like specifications in the source code, and an Eclipse plugin will tell you whether the specifications you wrote are correct and sufficient.

The job has the following steps:

  1. Read Section 2 of this document carefully.
  2. Perform the warmup task in Section 3 to become acquainted with the tool.
  3. Answer an online quiz to check that you understood the core concepts: http://bit.ly/zSJp5M .
  4. Contact us via vWorker before continuing.
  5. Perform the main task (see Section 5).
  6. Answer a short online survey about your experience.

Note: we wish to learn how long the main task takes. We expect it will take between 1-3 hours. Therefore, we ask that you do not take any breaks when performing the main task. If you have to take a break, please record the time and length of the break. Additionally, we will be monitoring your progress remotely.

If you have any questions about the project, please contact us via vWorker.

2  How to write program specifications

A program specification describes the behavior of a program. A verification tool can check the specification and verify that the program behaves as expected. However, for this to work, the specification must be precise and sufficient.

2.1  Method Specifications

A method specification consists of three parts:

You will write specifications using the Java Modeling Language (JML). We now give some examples.

2.2  Trivial example

Consider the following method:

/** Adds five to its argument. */
public Integer addFive(Integer x) throws IllegalArgumentException{
    if (x < 0){
        throw new IllegalArgumentException("x cannot be negative");
    }   
    return x + 5;
}

It is often possible to determine some of the specifications from the method’s documentation. When the documentation is not comprehensive, you have to determine them yourself.

2.3  Class Invariants

Class invariants are properties of a class’s member variables that must be true after the constructor is called; additionally, they are true whenever a public method is called and exits (even with an exception).

You’ll see an example of class invariants in the warm-up project (See Section 3).

2.4  Another example

Here is an example of a method specification written in JML, the Java Modeling Language. JML is Java-like, with some additional expressions. The method preconditions and postconditions are written between the method body and the method signature using the @requires, @ensures and @exsures annotations. A method can have multiple clauses of each type. 

class Queue{

    private int currentSize;

    private int theArray[];

    ...

    /**
    * Insert a new item into the queue.
    * @param x the item to insert.
    * @exception Overflow if queue is full.
    **/
    public void enqueue( Object x ) throws RuntimeException
    /*@ requires x != null; */
    /*@ ensures currentSize == \old(currentSize) + 1; */
    /*@ exsures (RuntimeException) \old(currentSize) == theArray.length; */
    {
      if( isFull( ) )
        throw new RuntimeException( "Overflow" );
      if ( ++back == theArray.length )
        back = 0;
      theArray[ back ] = x;
      currentSize++;
    }

    ...
}

In an exceptional postcondition (@exsures), the exception type (RuntimeException above) is written in parentheses between @exsures and the expression. Notice that contracts begin with a @ directly following the comment opening. Also notice that each contract ends with a semicolon.

2.5  JML syntax

Here is table that describes the JML expressions you will need to know for your task:

ExpressionTypeMeaning
a && bbooleanjust like in Java
a || bbooleanjust like in Java
!abooleanjust like in Java
a ==> bbooleanif a is true, then b is true; equivalent to (!a) || b
\forall decl; pred; exprbooleanused to express that expr holds over the range of values for which pred holds (Section 2.5.2)
\resultsame as the method’s return typethe return value of the method (can only be used in the method’s postcondition)
\old(expr)same as the type of exprrefers to the value of expr at the entry of a method (can only be used in a postcondition)

2.5.1  Implication

Implication, written as ==>, is related to conditional expressions (i.e., if and else). Saying that "a implies b", written in JML as a ==> b, means that if a is true then b must also be true. However, if a is false, b can be anything. In other words, false implies anything. For example, the statement "France is in Asia implies apples are oranges" is a true statement because France is not in Asia.

2.5.2  \forall statement: properties that hold for a range of values

The \forall statement is used to express that a fact holds over a range of values. For example, the following expression states that all of the values in the array array are non-null:

(\forall int i; 0 <= i && i < array.length; array[i] != null);

Notice that the middle expression 0 <= i && i < array.length is used to specify which values of i are important.

You can declare multiple variables in a \forall statement, as in the following example:

(\forall int i,j; 0 <= i && i < j && j < array.length; array[i] != array[j]);

2.5.3  Do not delete special annotations and expressions

In the warmup and main project, you may come across the annotations @modifies, @set, @spec_public, and @pure. You may also come across the expression \typeof. We’ve added these annotations for you in the correct places, do not delete comments that contain them. We’ve added additional comments to these lines to remind you. For example, in the warmup you will see the following comment:

/**
* Fill an array with one of two objects, based on whether the index 
* is in this set.
**/
public void fillDigits(Object[] digits, Object zero, Object one)
/*@ requires \typeof(digits) == \type(Object[]); */ //DO NOT DELETE THIS LINE
{
   ...
}

3  Warmup: Using Eclipse to verify a program

Before starting the main project, you’ll familiarize yourself with the interface by verifying the warmup project FixedSizeSet. FixedSizeSet represents a mutable set of integers between 0 and 7. The walkthrough is meant to introduce and reinforce the main concepts needed to complete the main task. You should spend about 1 hour on the warmup.

Don’t hesitate to ask us questions about the tool, or the process of verification, during the warmup.

The Eclipse plugin checks the program properties that the user writes as preconditions, postconditions, and class invariants. The plugin reads the source code (and annotations) and warns about annotations that might not be universally true. The plugin also warns about potential runtime exceptions.

The Eclipse plugin is a modular checker: it reasons about code by examining the body of one method at a time. Therefore, the plugin both checks and depends on properties. For instance, suppose method A calls method B. If you have not written properties describing the return value of B, VeriWeb may not be able to prove a property about method A.

3.1  Running Eclipse via Remote Desktop

  1. Remote Desktop into the specified server
    1. On Windows
      1. Go to Start > All Programs > Accessories > Remote Desktop Connection
      2. Enter the host IP that was given to you and click connect
    2. On Linux
      1. Go to Applications > Internet > Terminal Server Client
      2. Click Add Connection > Windows Terminal Service
      3. Enter a name for the connection (e.g., VERIFY) and the host IP that was given to you. Click OK
      4. Double click on the connection icon in the list
  2. Login using the username and the password provided to you; Eclipse will automatically load. Closing Eclipse will close your remote connection.
  3. Eclipse should start in the Verification perspective. If not, open the "Verification" perspective:
    1. Click the "Open Perspective" button to the left of the Java perspective button above the class outline view. Click "Other..." in the drop-down menu.
    2. In the dialog that opens, select "Verification" and click "OK".

3.2  Running the checker

Browse the library class FixedSizeSet.java and the client class FixedSizeSetCheck.java. You can see that the methods in FixedSizeSetCheck throw runtime exceptions if the library class does not behave as expected.

Let’s run the plugin on the project to see what warnings are reported:

  1. Save all of the files that you want to check
  2. Select the project or package in the Package Explorer. For example:
  3. Click the green check-mark in the toolbar to run the plugin on the selected project or package; clicking the red X will remove warnings from the selected object.

3.2.1  Plugin output

The plugin’s output is shown in the console; additionally, errors are marked and underlined in the source files (just like compilation errors and warnings). You can view the warning message at a location by hovering your mouse over the squiggly red line or over the corresponding red and white "E" on the left side of the editor.

Console output

When you first run the checker on the FixedSizeSet project, the end of the report will be:

------------------------------------------------------------------------
    [0.327 s 53322112 bytes]  failed
  [0.468 s 53365744 bytes total]
6 cautions
8 warnings
Escjava checker ended, status code 0

Each of the warnings corresponds to a place where an unexpected exception might be thrown, or a condition might not be met. The console output includes warning information for each method. If a method passes, a message like the following is shown:

  FixedSizeSetCheck: checkFillDigits() ...
    [0.011 s 42779336 bytes]  passed

, otherwise the error and associated information is displayed. For example, look at the console output for the checkConstructor method in FixedSizeSetCheck:

FixedSizeSetCheck: checkConstructor() ...
------------------------------------------------------------------------
.../FixedSizeSet/src/FixedSizeSetCheck.java:18: Warning: Possible unexpected exception (Exception)
    }
    ^
MARKER ...\FixedSizeSet\src\FixedSizeSetCheck.java 18 Warning: Possible unexpected exception (Exception)
Suggestion [18,4]: none
Execution trace information:
    Reached top of loop after 0 iterations in ".../FixedSizeSet/src/FixedSizeSetCheck.java", line 13, col 8.
    Executed then branch in ".../FixedSizeSet/src/FixedSizeSetCheck.java", line 14, col 33.
    Executed throw in ".../FixedSizeSet/src/FixedSizeSetCheck.java", line 15, col 16.

------------------------------------------------------------------------
    [1.716 s 51704352 bytes]  failed

The plugin is reporting that a method can throw an exception that is not declared in throws clause (it is unexpected). The “Execution trace” describes the source code location where the exception is thrown. Note that unexpected exceptions are marked on the line with the method’s closing brace.

Below is the source code for the checkConstructor method:

You can see that the plugin cannot determine that a newly created set is contains no number. Eventually, you should add a postcondition to the constructor FixedSizeSet() that describes this property. This will enable the plugin to reason that the exception cannot be thrown.

3.2.2  Known bug

NOTE: There is a known bug in the plugin that causes the following caution to be generated for each file when run on Windows:

  Caution: Using given file as the .java file, even though it is not the file for XXX on the classpath

You can (and should) safely ignore this caution.

3.3  Adding a class invariant

Let’s start our task by looking at the first warning in the FixedSizeSet file. There’s a warning in the add method that the program may attempt to dereference bits when it is null:

FixedSizeSet: add(int) ...
------------------------------------------------------------------------
.../FixedSizeSet/src/FixedSizeSet.java:23: Warning: Possible null dereference (Null)
        bits[n] = true;
            ^
MARKER ../FixedSizeSet\src\FixedSizeSet.java 23 Warning: Possible null dereference (Null)
Suggestion [23,12]: perhaps declare instance field 'bits' at 7,41 in .../FixedSizeSet/src/FixedSizeSet.java with 'non_null'
------------------------------------------------------------------------
    [0.015 s 75303928 bytes]  failed

3.3.1  Condition suggestions

Here, the plugin also provides a suggestion: perhaps declare instance field 'bits' at 7,41 in .../FixedSizeSet/src/FixedSizeSet.java with 'non_null'. The suggestion is to add a class invariant that bits != null. Based on the constructor and the other methods, you can see that bits should never be null. Therefore, the property is a good candidate for a class invariant (see Section 2.3):

3.3.2  Adding the invariant

Add the invariant /*@ invariant bits != null; */ just above the class’s field declarations.

public class FixedSizeSet{

    /*@ invariant bits != null; */

    /*@ invariant bits.owner == this; */ //DO NOT DELETE THIS LINE
    /*@ spec_public */ private boolean[] bits;
 
    ...
}

After you’ve added the invariant, save the file, and rerun the checker. Notice that the add method still has a warning, but the warning is different. We’ll address this warning in the next section.

To clear the old plugin output, right click on the console output screen and click “Clear” in the context menu.

Remove the @ from the invariant line you just added, and rerun the plugin. The warning from before will reappear, since the plugin now considers the line to be a regular comment rather than a specification. Re-add the @ and save the file.

3.4  Adding a precondition to add(...)

Look at the method add, for which the plugin reports that an array bounds exception can occur:

FixedSizeSet: add(int) ...
------------------------------------------------------------------------
.../FixedSizeSet/src/FixedSizeSet.java:24: Warning: Possible negative array index (IndexNegative)
        bits[n] = true;
            ^
MARKER ...\FixedSizeSet\src\FixedSizeSet.java 24 Warning: Possible negative array index (IndexNegative)
Suggestion [24,12]: perhaps declare method 'add' at 22,16 in .../FixedSizeSet/src/FixedSizeSet.java with 'requires 0 <= n;'
------------------------------------------------------------------------
    [0.016 s 79646288 bytes]  failed

Clearly the input n must be restricted so that it is non-negative and is less than the size of bits. To specify this, add a @requires clause to the method: /*@ requires 0 <= n && n < bits.length; */

/**
* Adds n to this set
**/
public void add(int n) 
/*@ requires 0 <= n && n < bits.length; */
{
    bits[n] = true;
}

Save the file and rerun the checker on the project. A warning should no longer be reported for the add method. You can double-check this by looking at the plugin’s console output for the add method:

FixedSizeSet: add(int) ...
    [0.007 s 63329648 bytes]  passed

3.5  Adding a postcondition to union(...)

Next, look at the method union, which performs the union of this set with another set other by setting all of the bits set in other. In other words, when the method exits, a bit is set if it was set originally in this.bits or was set in other.bits. In JML, for all bits, the following expression holds: bits[i] == (\old(bits[i]) || other.bits[i]. Here the \old(...) expression is used to refer to the bits array when the method is called. To indicate that the property holds for every element in the array, we use a \forall statement:

/*@ ensures (\forall int i; 0 <= i && i < bits.length; bits[i] == (\old(bits[i]) || other.bits[i])); */

3.6  Adding an exceptional postcondition to similar(...)

Look at the method similar which takes a set other, and potentially throws a runtime exception. The plugin reports a warning that the method can throw an unexpected exception (the warning marker is on the closing brace of the function; the console output describes where the exception is thrown). To eliminate this warning, we’ll have to add an @exsures clause that describes what is true when the method throws a RuntimeException. In particular, we know that other == null. So, we write the specification accordingly:

/*@ exsures (RuntimeException) other == null; */

Additionally, we must also specify what is true about other when the method executes normally, using an @ensures clause:

/*@ ensures other != null; */

3.7  Finishing the warmup

This concludes the walkthrough; add additional specifications to FixedSizeSet.java until you have eliminated all of the warnings from the plugin.

If you get stuck after the walkthrough, you can "cheat" by referring to the included project FixedSizeSet-Solved, which contains a set of annotations that permit the plugin to verify FixedSizeSet and FixedSizeSetCheck. This is only one possible solution among many; your solution might include more / different annotations. The purpose of looking at the solution is to help your skills in reasoning about programs, not just to get you through the warmup quickly.

When finished, compare your solution to the one provided in the FixedSizeSet-Solved project.

4  Quiz

Answer the online quiz to check that you understood the core concepts: http://bit.ly/zSJp5M. Then, contact us via vWorker before continuing with the main project.

5  Main Project

Follow these instructions after you have completed the warmup project (see Section 3), and have confirmed with us via vWorker that you should proceed.

  1. Load the Eclipse environment.
  2. Open the StackAr project, which consists of a library file StackAr.java and a client file StackArCheck.java.
  3. Add/remove/edit method preconditions, method postconditions, and class invariants so that the plugin reports no errors or warnings for the StackAr project. Re-run the plugin as many (or as few) times as you’d like.

    There are 3 important things you should not do:

    We have included conditions in StackAr.java that were inferred using an automated tool. Feel free to remove/edit these invariants or to retain (some of) them, whatever you find most useful.

    NOTE: your job is to write verify the library class against the client code, not to create the most detailed specification possible.

Please do not take any breaks when working on the main project; if you need to take a break, record the start time and length of the break.

While we will answer tool / interface questions during the main project, we will not answer questions such as "why can’t the plugin verify this postcondition?"

6  General Hints

The Eclipse plugin is a modular checker: it reasons about code by examining one method at a time. Therefore, the plugin both checks and depends on annotations. For instance, suppose method A calls method B. If you have not written properties describing the return value of B, VeriWeb may not be able to prove a property about method A.

When writing @ensures and @exsures clauses, any mention of an argument x refers to \old(x).

When writing @ensures and @exsures clauses, instead of calling a boolean predicate (e.g., isEmpty()) try writing the condition captured by the predicate explicitly.

7  Frequently Asked Questions

7.1  Do I have to verify all of the included conditions?

No! The included conditions are automatically generated suggestions, as such, they might (1) be false, or (2) be unnecessary to verify the library class with respect to the client. Remember: your job is to verify the source code given to you, not to write the most detailed specification possible.

7.2  When using Eclipse, I get the error: "Could not invoke Simplify"

There appears to be a bug in our Eclipse setup that causes the plugin’s configuration to sometimes be cleared. To reconfigure the plugin, follow these steps:

Windows > Preferences > Prover Editor > Simplify

Windows > Preferences > Java > ESC/Java2

After setting these options, you may need to close Eclipse (log out) and log back in for the changes to take effect.