Contents:

Introduction

In this assignment, you will verify the code you wrote for all previous homeworks. You will prove that your code never throws a NullPointerException.

You will use an automated tool, called the Nullness Checker. You will write specifications in a form that the Nullness Checker understands, and you will fix bugs that it identifies. The Nullness Checker issues warnings if:

Use of a verification tool such as the Nullness Checker complements or obviates some assertions and calls to checkRep.

Problem 1: Learn about Nullness Checker specifications

Read chapters 1, 2, 3, and 4. of the Checker Framework Manual. You can skip the installation instructions, because Gradle will automatically download the Checker Framework for you. You may also find the FAQ and the Troubleshooting guide helpful if you have questions. The reading will save you time in the long run, because you will use the Nullness Checker on every subsequent assignment. Feel free to ask the staff questions if you don't find your question answered in the documentation.

Also read the Nullness Checker handout.

Problem 2: Specify your code

Write Nullness Checker specifications for your code from all previous homeworks. That is, write Nullness Checker annotations that express your code's specifications. This includes specifying all of the staff-provided code from previous homework (except for hw2/PolyGraph.java and hw2/CalculatorFrame.java). You can only express — and the Nullness Checker will only verify — the nullness, initialization, and map key properties of your code, not every fact in your specifications. You will not run the Nullness Checker in this problem.

For example, suppose that you had a Graph whose representation is 

    // maps from each node to all of its children
    Map<Node, Set<Node>> edges;

and your rep invariant is:

All of these properties are expressible as annotations. Because @NonNull is the default, the following annotation can express this entire invariant! Then, the Nullness Checker will warn if your code violates the rep invariant. 

    Map<Node, Set<@KeyFor("edges") Node>> edges;

Likewise, you should express other invariants of your implementations as annotations. Whenever there is an invariant that you cannot express as an annotation, you might later need to suppress some false positive warnings.

The staff provided you a few annotations in commments. Uncomment them, for example by changing /*@Nullable*/ to @Nullable.

You do not need to worry about annotating the past JUnit tests. Take this code for example: 

/** @throws IllegalArgumentException if x == null */
public void foo(Integer x) {
  if (x == null) {
    throw new IllegalArgumentException();
  }
  // ...
}
Note that x == null is defined behavior for foo. However, it is also exceptional behavior, and we would prefer to let the Nullness Checker help us prevent clients from causing this exceptional behavior. For this reason, we do not annotate the argument x to the method foo with @Nullable. On the other hand, we would like to be able to test this behavior, since it is specified. So it is not necessary to annotate your tests, as we will not be running the Nullness Checker on them.

Avoid the temptation to run the Nullness Checker while writing the specification. When the Nullness Checker issues a warning, that might or might not be the best place for a fix. If you run the Nullness Checker and then just try to add annotations or change code in places where it issues a warning, you can get yourself in a mess. It is quicker to write all the specifications before running the tool.

Now commit and push your code, and tag the commit with the tag hw5-part1-final. That will show the graders what was done before and after the specification phase.

We will not grade you on whether all your annotatations were perfect as of the hw5-part1-final tag, nor whether your code passes the Nullness Checker. However, we want to see what work you did before and after starting to run the Nullness Checker.

Problem 3: Learn about running the Nullness Checker

Tutorial

Here is a quick tutorial demonstrating a type of warning the Nullness Checker will throw and how to resolve the underlying problem.
  1. Begin by viewing NullnessExample.java. It is a simple Java program with an easily-debugged null pointer exception. 
    public class NullnessExample {
    public static void main(String[] args) {
        Object myObject = null;
        System.out.println(myObject.toString());
    }
}
  2. Run ./gradlew assemble -PnullnessExample1 from the command line to see how the Nullness Checker warns you about this error at compile time.

    The following error will be produced. 

    [dereference.of.nullable] dereference of possibly-null reference myObject
        System.out.println(myObject.toString());
                           ^
  3. Edit the code to initialize the myObject variable to some non-null value, thus correcting the error. 
    public class NullnessExample {
    public static void main(String[] args) {
        Object myObject = new Object();
        System.out.println(myObject.toString());
    }
}
    Now, ./gradlew assemble -PnullnessExample1 should not issue any warnings.
  4. Run ./gradlew assemble -PnullnessExample2 to try the next example: debugging AnotherNullnessExample.java, NullFilledLinkedList.java, and LinkedListNode.java. You might have to fix code and/or specifications.

As part of the assignment, you must submit the fixed NullnessExample.java, AnotherNullnessExample.java, NullFilledLinkedList.java, and LinkedListNode.java files.

Answer the following question in hw5/answers.txt:
How did you change the code provided in AnotherNullnessExample.java, NullFilledLinkedList.java, and LinkedListNode.java to account for problems discovered by the NullnessChecker? For each change, also state why the change needed to be made.

Problem 4: Verify your code

Run the Nullness Checker to check your code against its specifications.

To run the Nullness Checker, simply run ./gradlew build or run the build Gradle task through IntelliJ. The Nullness Checker manual also contains instructions for running a checker within IntelliJ, but using those instructions is optional.

Answer the following questions in hw5/answers.txt:
  1. Did the Nullness Checker indicate any problems with your specifications or code? If so, what were they?
  2. How did you change your specification or code to account for problems discovered by the Nullness Checker? For each change, also state why the change needed to be made.

Collaboration

Please answer the following questions in a file named hw5/collaboration.txt. The standard collaboration policy applies to this assignment. State whether or not you collaborated with other students. If you did collaborate with other students, state their names and a brief description of how you collaborated.

Feedback on the assignment

Complete the Canvas Quiz associated with this assignment. You will receive full credit for this section if you complete the quiz. Your answers will be anonymous to the instructors. This quiz is due 24 hours after the assignment due date. You cannot use late days for this quiz.

What to Turn In

You should add, commit, and push the following files to your CSE 331 GitLab repository:

Please tag the commit of your finished homework with the tag hw5-final.

When you have committed and pushed all of your changes and are done with the assignment, you should create a git tag in your repository and push that tag to your repository. Once you have committed and pushed that tag, your assignment has been submitted and the staff will grade the files in your repository that are labeled with that tag.

Refer to the assignment submission handout for complete turnin instructions.