Handout P8

Contents:

Introduction

As always, please read the entire handout before you start work.

Programmers hate to do by hand anything that can be automated. This includes formal verification: it is an important and useful way to ensure that your program is correct, but it can be tedious to do by hand, and especially if it has to be redone every time that your program changes.

In this assignment, you will get experience with automated program verification, in which you write a specification and the ESC/Java2 system performs a proof of correctness for you. This experience should help to solidify your understanding of the basics of reasoning about programs. It will also help you to understand a new technology that, though not widespread today, is increasingly being used in software development where correctness is important.

Your job in this problem set is to verify the correctness of 3 small programs using ESC/Java2, the Extended Static Checker for Java. You will use both the Eclipse and the VeriWeb interfaces demoed in class, using one interface for the first two problems and the other for the third. The order that you will complete the assignment in has been determined randomly — you will receive an email containing this order.

Each program consists of two classes — an abstract data type (ADT) and a client class that calls it. You will create and/or edit annotations in the source code of the ADT. You will not write write annotations in the client code. Your goal is to enable ESC/Java to verify that neither the ADT nor the calling code may ever terminate with a runtime exception. That is, when ESC/Java produces no warnings or errors on both the ADT and the calling code, your task is complete.

For each program, please allocate 1 hour of uninterrupted time to complete the verification task. (Some tasks may take less time; for others, you may not be finished when the hour runs out). Feel free to take breaks in between tasks, but please do not read email, etc. while you are working on a program. In total, you will spend around 5 hours on this assignment.

You are not permitted to collaborate with other students on this problem set. This problem set will help us understand the usability of program verification tools for CSE331 students; we are interested in your ability to use the interfaces, not your ability to collaborate!

The Extended Static Checker for Java

ESC/Java is a tool that statically checks certain program properties. Users express the properties via source comments, similar to assertions or Java annotations. ESC reads the source code (and annotations) and warns about annotations that might not be universally true. ESC also warns about potential runtime exceptions such as null dereferences and array bounds errors.

ESC annotations are written in the Java Modeling Language (JML). In general, ESC supports annotations anywhere in the source code. However, in this problem set, you will only use annotations that specify properties of an abstract data type. Specifically, you will write a representation invariant (also known as an object invariant) and method specifications (preconditions and postconditions).

ESC is a modular checker: it reasons about code by examining one method at a time. Therefore, ESC both checks and depends on annotations. For instance, if an annotation describing the return value of an observer method is missing, ESC may not be able to prove a result about a method that calls that observer. This is exactly the same as other modular verification tools, such as type-checkers including the Nullness Checker. It is also the way a human performs an inductive proof of correctness for a data structure.

Setup

No setup is required. You will use Eclipse and its ESC/Java2 plugin via remote desktop. You will use VeriWeb from a web browser. As usual, you will submit the assessments by committing the files to your SVN repository.

By now you should have received an email at your @cs account containing:

If you have not received an email with this information, please contact the course staff immediately.

Grading

We do not expect that everybody will complete all the tasks within the given time bounds — the tasks are (intentionally) of varying difficulties. As such, your grade on this assignment will not be determined by whether or not you complete the verification tasks. Rather, we will determine your grade by (1) whether or not you attempted the tasks and (2) your written response for the assessments.

Using Eclipse and its ESC/Java plugin

Running Eclipse via Remote Desktop

  1. Remote Desktop into the server specified in the staff email:

    On Windows

    1. Go to Start → All Programs → Accessories → Remote Desktop Connection
    2. Enter the host IP that was emailed to you and click connect

    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., CSE331-PS8) and the host IP that was emailed to you. Click OK
    4. Double click on the connection icon in the list
  2. Login using your @cs username and the password provided in the email; Eclipse will automatically load. Closing Eclipse will close your session, so don't do that until you are done with the project.
  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".

Configuring the ESC/Java2 plugin

We have setup the ESC/Java2 plugin for you. However, before beginning the assignment, please confirm the following configuration (performing the steps as needed):

Windows → Preferences → Prover Editor → Simplify

  1. Select "Custom"
  2. Enter C:\Program Files\Simplify\Simplify-1.5.4.exe for the path

Windows → Preferences → Java → ESC/Java2

  1. Check "no semicolon warnings"
  2. Check "enables output of counterexample information"
  3. Check "enables output of suggestion information

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

Verifying a file or package

To run ESC/Java2 on a project, package, or file:

  1. Select the project, package, or file in the Package Explorer. For example:

  2. Click the green check-mark in the toolbar to run ESC/Java2 on the selected project, package, or file; clicking the red X will remove ESC/Java2 warnings from the selected object.

    Note: if you run ESC/Java2 on a single file, only that file is passed to the checker — types and methods from other files will not be found. For example, running the checker on StackArCheck.java will result in an error that ESC/Java2 cannot find type StackAr.

  3. ESC/Java's output is shown in the console; additionally, errors are marked and underlined in the source files (just like compilation errors and warning). 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.

NOTE: There is a known bug in the ESC/Java2 Eclipse plugin that causes the following error / 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 error.

Using VeriWeb

VeriWeb works best in Chrome and Firefox. Do not use another browser (e.g., Internet Explorer) because the interface may not function properly.

  1. Browse to http://schillerlabs.com:8080/VeriWeb/start.html
  2. Enter your @cs username and select the project to verify. Click "OK"
  3. If at any point you believe that the tool has stopped working (e.g., drag and drop doesn't work), try reloading the page. If the problem persists, please contact the course staff.

Usage Basics

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 invariants in the drag and drop interface, move the vertical slider to the right.

Just about the only case where ESC/Java and VeriWeb can provide human-readable feedback about why a clause failed to verify is when the clause in syntactically incorrect or has a type error.

The only way to leave a precondition problem is to either eliminate all of the ESC/Java2 warnings for the method or to signal that the specs for a method that it calls are deficient.

If the user interface becomes unresponsive, reload the page.

Verification in Eclipse (33 points)

This section contains the instructions for the Eclipse user interface. If the email you received states that you should use the VeriWeb interface first, follow the instructions for VeriWeb first and return to this section later.

Warm-up

Before using the Eclipse interface on the main projects, familiarize yourself with the interface by verifying the warm-up project FixedSizeSet, an ADT representing a mutable set of integers drawn from the range [0..7].

Follow the instructions in the next section for the FixedSizeSet project, taking as much time as you need. If you get stuck, you can "cheat" by referring to the included project FixedSizeSet-Solved, which contains a set of annotations that permit ESC to verify the ADT 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. Most students won't need to look at the solutions, but if you do, make it a learning experience.

Don't hesitate to ask the course staff questions about the tool / verification during the warm-up.

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

Main Instructions

Follow these instructions for each project that you are instructed to verify with the Eclipse interface.

  1. Familiarize yourself with the Eclipse assessment questions
  2. Load the Eclipse environment.
  3. Record the project name and your starting time for the project in a file named eclipse.txt in your answers/ directory. This is in your regular CSE331 SVN checkout, not in the environment you access via remote desktop.

  4. Spend at most 1 hour adding/removing/editing method preconditions, method postconditions, and representation invariants so that ESC/Java2 reports no errors or warnings. Re-run ESC/Java as many (or as few) times as you'd like. Do not modify any Java statements or expressions in the source code. Also, do not add/edit the annotations in the client file.

    For the main projects — i.e., not the warmup — we have included invariants in the ADT file that were inferred with the Daikon tool. Feel free to remove/edit these invariants or to retain (some of) them, whatever you find most useful.

  5. Record your ending time for the project in eclipse.txt.

Guidelines

Assessment of the Eclipse user interface

Please answer the following questions in a file named eclipse.txt in your answers/ directory. There are no wrong or right answers, but we expect your answers to be thoughtful.

  1. Did you write all your annotations first, then check them, or incrementally add annotations and check? (Essentially, describe your mode of operation while performing this task). How much time did you spend before first running the checker?
  2. If you used the Eclipse interface to verify 2 projects: Was your approach the same for both projects, and if not, how did it differ?
  3. In what general order did you write annotations? (For example, starting at the top of a source file and working your way to the bottom of the source file, or in the order that ESC/Java produced warnings, or some other order (be specific).) Why did you choose that order?
  4. Describe the most difficult ESC/Java2 warning that you eliminated (be concrete — class and method). What information did you not know or understand, or what fact were you unable to express, that made the warning difficult to eliminate?
  5. Describe the most difficult ESC/Java2 warning that you could not eliminate, if any (be concrete — class and method). What information did you not know or understand, or what fact were you unable to express, that made the warning difficult to eliminate?
  6. What did you find especially hard (or especially easy)?
  7. Do you have any suggestions for improving the way the tool works? (What did you expect or want to see that you didn't?)
  8. The provided source code contained some properties that had been inferred by Daikon. In what way(s) were the supplied conditions helpful? In what way(s) were the supplied invariants not helpful, or a hindrance? On balance, did you find the supplied conditions helpful?

Verification with VeriWeb (33 points)

This section contains the instructions for the VeriWeb user interface. If the email you received states that you should use the Eclipse interface first, follow the instructions for Eclipse first and return to this section later.

Warm-up

Before using the VeriWeb interface on the main projects, familiarize yourself with the interface by verifying the warm-up project FixedSizeSet, an ADT representing a mutable set of integers drawn from the range [0..7].

Follow the instructions in the next section for the FixedSizeSet project, taking as much time as you need. Follow the instruction in the next section for the FixedSizeSet project. If you get stuck, you can "cheat" by referring to FixedSizeSet.java, a file that contains a set of annotations that enable ESC to verify the ADT and the client. This is only one possible solution among many; your solution might include more / different annotations.

Don't hesitate to ask the course staff questions about the tool / verification during the warm-up.

When finished, compare your solution to the one provided in FixedSizeSet.java.

Main Instructions

Follow these instructions for each project that you are instructed to verify with the VeriWeb interface.

  1. Familiarize yourself with the VeriWeb assessment questions
  2. Open the project in the VeriWeb environment (See Section Running VeriWeb).
  3. Record the project name and your starting time for the project in a file named veriweb.txt in your answers/ directory.

  4. Spend at most 1 hour using the tool so that ESC/Java2 reports no errors or warnings. You are finished verifying a project when the tool presents you with a solution key.

  5. Record your ending time for the project in veriweb.txt.

Assessment of the VeriWeb user interface

Please answer the following questions in a file named veriweb.txt in your answers/ directory. There are no wrong or right answers, but we expect your answers to be thoughtful.

  1. Describe the most difficult ESC/Java2 warning that you eliminated (be concrete — class and method). What information did you not know or understand, or what fact were you unable to express, that made the warning difficult to eliminate?
  2. Describe the most difficult ESC/Java2 warning that you could not eliminate, if any (be concrete — class and method). What information did you not know or understand, or what fact were you unable to express, that made the warning difficult to eliminate?
  3. What did you find especially hard (or especially easy)?
  4. Do you have any suggestions for improving the way the tool works? (What did you expect or want to see which you didn't?)
  5. The provided source code contained some properties that had been inferred by Daikon. In what way(s) were the supplied conditions helpful? In what way(s) were the supplied invariants not helpful, or a hindrance? On balance, did you find the supplied conditions helpful?

Assessment of program verification (33 points)

Like any tool, ESC/Java2 and its two user interfaces you tried have their own strengths and weaknesses, and should only be used in appropriate ways and situations.

Please answer the following questions in a file named assessment.txt in your answers/ directory. There are no wrong or right answers, but we expect your answers to be thoughtful.

  1. Which verification projects did you performs, and in what order? Each project consists of a program name and a user interface (Eclipse or VeriWeb).
  2. When performing the Eclipse warmup, did you refer to the FixedSizeSet-Solved project for hints before completing your own solution?
  3. When performing the VeriWeb warmup, did you refer to the FixedSizeSet.java file for hints before completing your own solution?
  4. The classes you were given were not documented. (That's terrible style; amazingly, these were taken verbatim from a textbook!) During the process of creating verifiably-correct specifications, did you discover any facts about the code that was different than what you had assumed, based on your intuition or on your initial examination of the program? Be specific.
  5. Which user interface was easier for you to learn? Why?
  6. If you had used the interfaces in the opposite order, would your answer to the previous question likely be different? If so, why?
  7. Which user interface did you you prefer? Why?
  8. Use the principles discussed in lecture to critique the two user interfaces. For each user interface, state and discuss (in 1-2 sentences each) two positive and two negative aspects of the user interface design.

Collaboration

You are not permitted to collaborate with other students on this problem set. This problem set will help us understand the usability of program verification tools for CSE331 students; we are interested in your ability to use the interfaces, not your ability to collaborate!

Reflection (1 point)

Please answer the following questions in a file named reflection.txt in your answers/ directory.

  1. How many hours did you spend on each problem of this problem set? (Only include time when you are completely focused on CSE 331. For example, if you worked an hour in your noisy dorm lounge, or you were periodically reading email or IMs, don't count that hour. But, that shouldn't have happened for this problem set!)
  2. In retrospect, what could you have done better to reduce the time you spent solving this problem set?
  3. What could the CSE 331 staff have done better to improve your learning experience in this problem set?
  4. What do you know now that you wish you had known before beginning the problem set?

What to turn in

The following files should be checked into SVN before you run ant validate:

Hints

ESC is a modular checker: it reasons about code by examining one method at a time. Therefore, ESC both checks and depends on annotations. For instance, if an annotation describing the return value of an observer method is missing, ESC may not be able to prove a result about a method which calls that observer.

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

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

Exceptional postconditions are not throws clauses — an Exceptional postcondition states what is true when the exception is thrown, whereas a Java throws clause describes what conditions cause an exception to be thrown. Though there is often some overlap between the two, they are not the same.

Errata

March 5, 2011: Added section on Reconfiguring the ESC/Java2 plugin for Eclipse, and related Q & A.

March 6, 2011: Clarified what happens when ESC/Java2 is run a single file in Eclipse instructions.

Q & A

This section will list clarifications and answers to common questions about problem sets. We'll try to keep it as up-to-date as possible, so this should be the first place to look (after carefully re-reading the problem set handout) when you have a problem.

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

There appears to be a bug in our Eclipse setup that causes the ESC/Java plugin's configuration to be cleared. To reconfigure the plugin, follow these steps.

When using Eclipse, I get missing semicolon errors

Be default, ESC/Java2 requires that each clause it terminated with a semicolon. Ironically, for ease of use, we turned of this requirement in the configuration. There appears to be a bug in our Eclipse setup that causes the ESC/Java plugin's configuration to be cleared. To reconfigure the plugin, follow these steps.