VeriWeb Project Instructions |
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 use a web interface called VeriWeb. VeriWeb lets you write method specifications in a Java-like language, then it tells you whether the specifications you wrote are correct and sufficient.
The job has the following steps:
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.
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.
A method specification consists of three parts:
You will write specifications using the Java Modeling Language (JML). We now give some examples.
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;
}
x is not null”.
(Otherwise, it fails by throwing a NullPointerException.)
Thus, the precondition is:
@requires x != null
When reasoning about preconditions, it is often helpful to reason "backward" from the place where an error may occur; this helps you determine what must be true in order for the exception not to occur.
null”, and that
“x is not negative”, because the method returned without an exception.More
interestingly, we also know that “the return value of the method is equal to
the value of x plus 5”.
Thus, the postconditions are:
@ensures \result != null @ensures \result = x + 5 @ensures x >= 0
A postcondition describes what must be true when the method exits, including facts about class member variables and return values.
IllegalArgumentException is
thrown, we know that “x is negative”. Therefore the exceptional
postcondition is:@exsures (IllegalArgumentException) x < 0
An exceptional postcondition states what is true at the moment the exception is thrown. This may not be the same as the conditions when the method was called that caused the exception to be thrown later. There is often some overlap between the two, but they are not the same.
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.
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.
You will use the web interface to write these, instead of inserting
them directly in the source code.
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++;
}
...
}
Here is table that describes the JML expressions you will need to know for your task:
| Expression | Type | Meaning |
| a && b | boolean | just like in Java |
| a || b | boolean | just like in Java |
| !a | boolean | just like in Java |
| a ==> b | boolean | if a is true, then b is true; equivalent to (!a) || b |
| \forall decl; pred; expr | boolean | used to express that expr holds over the range of values for which pred holds (Section 2.4.2) |
| \result | same as the method’s return type | the return value of the method (can only be used in the method’s postcondition) |
| \old(expr) | same as the type of expr | refers to the value of expr at the entry of a method (can only be used in a postcondition) |
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.
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]);
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.
VeriWeb is a web interface that checks the program properties that the user writes as method pre- and postconditions. VeriWeb reads the source code (and properties) and warns about properties that might not be always true. VeriWeb also warns about potential runtime exceptions.
VeriWeb is a modular checker: it reasons about code by
examining the body of one method at a time. Therefore, VeriWeb 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.
VeriWeb is a web interface that checks the program properties that the user writes as method pre- and postconditions. VeriWeb reads the source code (and properties) and warns about properties that might not be always true. VeriWeb also warns about potential runtime exceptions.
VeriWeb is a modular checker: it reasons about code by
examining the body of one method at a time. Therefore, VeriWeb 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.
VeriWeb works best in Chrome and Firefox. Do not use another browser (e.g., Internet Explorer) because the interface may not function properly.
FixedSizeSet. Click
"OK"
To begin this project, VeriWeb will ask you to write postconditions
for the method FixedSizeSet(). The interface consists of 3
main panels:
A postcondition problem asks you to write expressions that are true when the method returns. Expressions you try are shown in the bottom left of the interface. VeriWeb also tries some postconditions automatically for you. In this case, the tool has guessed a couple postconditions. The conditions are correct, so they are shown in green:
You can move the split bars to change the size of the three main information regions. For example, to give yourself more space to see long conditions listed in the lower left, click and drag the vertical slider to the right.
In the source code view, hover your mouse over the FixedSetSet
method name underlined in blue. The information panel will show the
documentation for the method. As we’ll see later in the walkthrough,
the method’s conditions will be also be displayed in the information
panel when you hover your mouse over the method in the source code
view.
Even though VeriWeb guesses postconditions, you should also think of
other properties that might be true. In this case, the fact that
bits is not null when the method returns seems
important. Let’s use the drag-and-drop interface to write the
condition.
The drag and drop interface lets you assemble conditions by combining condition fragments. The interface consists of three main parts: the condition fragment palette, the scratch pad, and the condition entry box.
The fragment palette contains JML specification fragments
with holes that you can fill with other fragments. To use a new
fragment, click and drag it from the palette. Try dragging the
forall int i fragment to the scratch pad:
Fragments can be dropped onto the scratch pad, or the hole of another fragment:
The scratch pad can contain as many fragments as you want. Use the scratch pad to build up complex fragments, for example:
To remove a subfragment from a fragment (and move it elsewhere), hover your mouse over the fragment,
then click and drag the fragment to another location, such as an open hole in a another fragment.
To delete a fragment, click and drag the fragment, dropping it onto the "Delete Fragment" area that appears:
Try deleting all the fragments on the scratch pad.
Now that we’ve learned to use the interface, let’s write the condition
bits != null:
!=null fragment to the condition box.
this.bits fragment and drop it into the hole
on the !=null fragment to form the condition
this.bits != null.
Click “Next Problem” to move onto the next problem.
Next, VeriWeb will ask you to select required preconditions from a
list of guessed preconditions for the add method, since the
method might crash with an exception. To see the warnings, hover your
mouse over the source code underlined in red. In this case, 3 warnings
will show in the information panel:
Since the “Array index possibly too large” warning would be
eliminated if n < bits.length was true, click the checkbox next
to the precondition to activate it. After VeriWeb has finished
thinking, when you hover your mouse over the underlined source code,
you will see that the warning is no longer present.
The other possible precondition, bits.length == 8, is not
necessary. Do not activate it. Be careful to not make the
preconditions too strict! If you write a precondition that is not
true, it might eliminate the warning in the method body, but you will
have to change it later when you are working on another part of the
code that calls this method.
The set of possible preconditions VeriWeb knows about is not
sufficient to eliminate the other two warnings, so we let VeriWeb know
about them. Click the “Condition Not Listed” button. In the window
that appears, write a short description of the preconditions needed to
eliminate the warnings, i.e., that n should be non-negative,
and bits should not be null. Click “OK.”
Next, VeriWeb will have you write preconditions for the method. Note that in the information bar, VeriWeb is notifying you that “There are messages.” By clicking this link, you can see the messages for the problem. In this case, your message from the previous problem will appear.
Whenever you indicate that a problem cannot be solved, or that an existing specification is incorrect, the VeriWeb interface will ask you to write a short message describing the problem. These messages are made available to you when VeriWeb asks you to fix the problem.
If there are multiple message, VeriWeb will show you a list of source methods. Click on the source method to view to associated message thread.
The interface has two interfaces for entering conditions: (1) drag and drop, and (2) textual. You can switch between the two modes using the radio buttons:
Type and submit the following two preconditions.
bits != null
n >= 0
We suggest that you start with the drag and drop interface because it helps you write syntactically valid conditions. When you are confident you can write conditions on your own, you can switch to textual input. You can always switch back if you want.
When VeriWeb is done thinking, click the “Next Problem Button”.
Next, VeriWeb will ask you to write postconditions for the method
add. In the source code view, you will see the preconditions
that are assumed — the precondition that you activated and the two
preconditions you just wrote.
For this problem, VeriWeb automatically checks 2 postconditions:
VeriWeb displays the condition bits.length == 8 in red since it
is not guaranteed to be true given the assumed preconditions. You can
hide the condition by clicking the red “X” to the left of the
condition. The condition bits[n] == true turns green since it
is guaranteed to be true.
Click “Next Problem”.
Next, VeriWeb will ask you to select preconditions for the method
union. Notice that there are 2 areas of the source code
underlined in red. Hover your mouse over each to view the
warnings. Based on the warnings, it should be clear that both
suggested preconditions should be activated. But, as before, these
aren’t sufficient, since it also must be true that both
other.bits and this.bits are not null, and
other.bits.length >= bits.length.
Click the “Condition not listed” button, and write a short textual description of the missing preconditions.
Next, VeriWeb will ask you to write preconditions for the same method
union. Submit the conditions other.bits != null and
this.bits != null.
Next, let’s submit a slightly incorrect precondition. If VeriWeb cannot prove a condition, then there are three possibilities: (1) the condition is false and you should not have written/selected it, (2) the condition is true but you have not yet provided enough other information (such as method pre- or postconditions on this or another method) to permit VeriWeb to prove it, or (3) VeriWeb is not powerful enough to prove the property, no matter how much other information you provide.
Enter the condition other.bits.length > bits.length (note the
strict inequality). The condition will turn red:
Hover your mouse over the blue information box 
to view the condition
failure information in the information panel. By expanding the nodes
in the tree, you can see that the method can be called with both
arrays having the same size. Also, you can hover your mouse over the
subexpressions of the condition to see their values:
When you are solving postcondition problems, the table will also show the values when the method exits.
Non-null values are described by a unique id of the form
ref@.... If two ids are the same, the references point to the
same object.
Submit the correct condition other.bits.length >= bits.length,
and click “Next Problem” when VeriWeb has finished thinking.
Next, VeriWeb will ask you to write postconditions for
union. In this case, VeriWeb again automatically tries a couple
postconditions. But, we note the second conditions isn’t general
enough: the property should hold for each element of the array. To
express this, we use a \forall statement (see
Section 2.4.2):
(\forall int i; 0 <= i && i < bits.length; bits[i] == (\old(bits[i]) || other.bits[i]))
Note the use of the \old(...) expression to refer to the bits
array when the method is called.
Click “Next Problem”.
Next, VeriWeb will ask you to select preconditions for the method
similar. From the code, you can see that the required
postconditions are the same as for union, but that
other != null is not required since the method is since the
method has declared it throws a RuntimeException in its throws
clause.
Therefore, the following conditions should hold:
(other != null) ==> other.bits != null
(other != null) ==> other.bits.length >= bits.length
Indicating that the properties only must hold when
other != null. To enter these, click the “Precondition Not
Listed” button, and enter a short description of the necessary
preconditions. VeriWeb will then ask you to submit those
preconditions.
VeriWeb will now ask you to write the similar methods regular
postconditions, i.e., what is true when the exception is not
thrown. The postcondition should say that the method returns
true if, and only if, the elements are equal:
\result == (\forall int i; 0 <= i && i < bits.length; bits[i] == other.bits[i])
HINT: When answering postcondition questions, any mention of an
argument x refers to \old(x), the value of x when
the method was called.
VeriWeb will now ask you to write the exceptional
postconditions for RuntimeException, i.e., what is true when
the exception is thrown in the similar(...) method. The top of the
problem panel will say “Write post-conditions for RuntimeException”.
REMEMBER: An exceptional postcondition states what is true when the exception is thrown. This may not be the same as the conditions when the method was called that caused the exception to be thrown later.
In this case, we know that other == null. Submit this
condition.
HINT: When answering postcondition questions, any mention of an
argument x refers to \old(x), the value of x when
the method was called.
This concludes the walkthrough; complete the task by using the VeriWeb tool until it informs you that you are finished.
VeriWeb provides two ways to learn about the methods called by the current method:
In the example below, the user has toggled the inline specifications
for FixedSizeSet and contains:
Notice that the precondition bits != null is not met for the
method contains, and is therefore shown in red. By looking at
the postconditions FixedSizeSet, you can see that the method
needs a postcondition that bits != null.
To tell VeriWeb that this postcondition is needed, bring up the
specification for FixedSizeSet by hovering your mouse over the
method. Then click “Add Postcondition”.
Alternatively, if you thought the precondition for contains was
too strong, you would bring up the specification for contains
and then click the “Bad” button next to the bits != null condition:
If you get stuck, you can "cheat" by referring to the file FixedSizeSet.java, which contains a set of annotations that are sufficient to verify the library and the client. 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 warm-up quickly.
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.
StackAr project in the VeriWeb environment (see
Section 3.1).
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 VeriWeb verify this postcondition?"
VeriWeb is a modular checker: it reasons about code by examining one
method at a time. Therefore, VeriWeb 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 answering postcondition questions, instead of calling a boolean
predicate (e.g., isEmpty()) write the property (the method’s
body) explicitly.