Exercise 1: Static Code Analysis

In this lab, students will run a static code analysis tool on an existing codebase and analyze the results. Static code analysis tools are designed to conduct automated inspections on a given codebase  and  detect  potential  defects.  Static  code  analysis  is  an  advanced  bug-finding technique in the industry and there are open-source and commercial tools for this purpose. Students will execute an analysis tool on an existing project and interpret its output.

Tool Setup

1.   Launch Eclipse

2.   Install the SpotBugs Eclipse plugin. You can drag and drop the “Install” icon in the Eclipse marketplace to start the installation.

We are going to use the same JFreeChart project that we cloned from GitHub from the previous lab. So open the project that is cloned from the repo like the last exercise.

Instructions

To become familiar with SpotBugs, we will simply ask it to analyze JFreeChart.

1.   Right-click on the JFreeChart project in the package explorer

2.   Select “SpotBugs > Find Bugs” from the context menu.

3.  Wait for SpotBugs to complete.

4.   Once SpotBugs has been completed, you can see the number of warnings in parentheses in the package explorer

5.   Open new windows for SpotBugs (bug explorer and bug info)

a.   Click Window on the drop-down menu

b.   Select show view

c.   Click Other

d.   Find SpotBugs

e.   Open both Bug Explorer and Info

6.  You can explore different bug warnings with different severity from bug explorer.

a.   Expand any warning like the figure below.

b.   Double-click any warning to navigate to the location.

 

7.   If the warned file is open

a.   Switch the bug info View on like the figure below.

b.  This will show the specific information about the warning

i.      Navigation of the method calls.

ii.      Bug: explanation of the potential bug.

iii.      Rank: shows the severity and its confidence level.

iv.      Pattern: name of the pattern that is used to detect potential bugs.

v.     Type and category

vi.     And the XML output of the tool for later use

 

Analyzing an issue

Let us now examine the issue “EC: Call to equals() comparing different types

(EC_UNRELATED_TYPES)

”

1.   Inspect the issue by clicking on the occurrence or by viewing the description on the

SpotBugs website:

https://spotbugs.readthedocs.io/en/latest/bugDescriptions.html.

2.   SpotBugs tells us that:

This method calls equals(Object) on two references of different class types and     analysis suggests they will be to objects of different classes at runtime. Further,    examination of the equals methods that would be invoked suggests that either this call will always return false, or else the equals method is not symmetric (which is a property required by the contract for equals in class Object).

3.   It is easy to see that SpotBugs is correct in indicating that this code looks suspicious,    however before confirming that this is indeed a bug, we should examine all possibilities.

4.  The first thing that we must consider is that SpotBugs may be incorrect in understanding the requirements of this method. We should consider that there is a possibility that this   could be a correct use of CategoryToPieDataset::equals()which perhaps deviates from  the norm of most Object::equals()methods. We have to refer to the implementation of     both DefaultCategoryDataset and CategoryToPieDataset.

5.  The second thing we must consider is the context: is there any possibility that this misuse is the intended implementation? On another quick examination of the above   code, we can see that the suspect code is part of a method testEquals(). Above the    method declaration, on line 180, there is code documentation simply stating: “For datasets, the equals() method just checks keys and values.” which clearly indicates to us that this method exists as a test. If the intention is to test the

SimpleDateFormat::equals() method then this could be the intended implementation, if not then this may again indicate an error.

6.   In this particular example, we could see that this code may in fact be erroneous or maybe the intended implementation. This leads us to believe that making the determination ourselves would be impossible without contacting the developers, which is impracticable for this example. Choosing one of these three possibilities is up to you. However, using tools such as SpotBugs in your own development projects may be helpful.

Exercise 2: Design by Contract (DbC) using Java Modeling Language (JML)

In this lab, you will work on completing the contracts of a simple Library system, which involves two classes, i.e., Library and Book. An object of a Library contains a list of books. A library can add new books, delete existing books, find the books by given title, etc. The project we provided has been implemented completely, your task is to write appropriate contracts using    JML.

The resource for this exercise:

●   JML command-line tool:V-0.8.51

●    Contracts examples:http://www.openjml.org/examples/

●   The java file we will be using today:Library.javaor copy from the bottom.

Preparation

1.  You need to use java 8 for this tool.

a.   Installjava 8 if you don’t have it.

b.  You can swap the default java using this command:

sudo update-alternatives --config java

2.   Download openjml-0.8.51-20210102.zip from:V-0.8.51

a.   Unzip to use openjml.jar inside.

3.   Run the tool by the following command via CLI:

a.  java -jar [path_of_openjml]/openjml.jar [options] [cur_path]/Library.java

b.  -esc : option for static checking

c.   -rac : option for runtime checking

d.   Note: your path shouldn’t have white spaces.

Syntax examples

1.   requires

a.   Specifies a precondition that should be met.

b.  e.g. @ requires newBook != null;

2.  ensures

a.   Specifies a postcondition that should be met.

b.  e.g. @ ensures holdings.contains(newBook);

3.  \result

a.   Keyword used to state the return value of the method.

b.  e.g. @ ensures \result == a;

4.  \old()

a.   Keyword used to state the values before the execution of the method.

b.  e.g. \old(holdings.size())); // size of holding before the execution.

5.   ==>

a.   Implications // A ==> B; // A implies B

b.  e.g. holdings.contains(newBook) ==> \result == true

6.  \forall

a.   Universal quatifier expression.

b.  e.g. \forall int i; 0 <= i < a.length; a[i] == 2*i

c.   \\ states the property that each (that is, all) of the elements of the array have a value equal to twice the index of the element.

Instructions:

1.   Fill in the JML part in Library.java file (TODO parts)

2.   Check if JML executes without error (both with static and runtime options).

a.   If you see warnings pointing to the contracts that you have written, something is wrong with them!

b.  You may ignore the warnings pointing to the actual code.

Library.java

import java.util.LinkedList;

class Library {

LinkedList<Book> holdings = new LinkedList<Book>();

// constructor

Library() {}

//* The following contracts are designed for function 'addBook'*/

//TODO pre-condition: the 'newBook' should not be null

//@ requires

//TODO post-condition: the newBook should be in the holdings after executing this function //@ ensures

//TODO post-condition: the size of holdings is increased by 1

//@ ensures

Library addBook(Book newBook) { // add a new book to the library (assuming there are no duplicate

books)

holdings.add(newBook);

return this;

}

//* The following contracts are designed for function 'removeBook'*/

//TODO pre-condition: the newBook should not be null

//@ requires

//TODO post-condition: if this method returns true, the newBook should be in old holdings (i.e.,

before executing this method)

//@ ensures

//TODO post-condition: if this method returns false, the newBook should not be in old holdings //@ ensures

//TODO post-condition: the size of holdings is reduced by 1 if return true

//@ ensures

boolean removeBook(Book newBook) { // remove a new book to the library

for (int i = 0; i < holdings.size(); i++) {

if (holdings.get(i).equals(newBook)) {

holdings.remove(i);

return true;

}

}

return false;

}

/* The following contracts are designed for function 'hasBook'*/

//TODO pre-condition: the newBook should not be null

//@ requires

//TODO post-condition: the size of holdings is the same before and after executing this method //@ ensures

//TODO post-condition: each element in holdings should be the same before and after executing this method

//@ ensures

boolean hasBook(Book newBook) {

for (int i = 0; i < holdings.size(); i++) {

if (holdings.get(i).equals(newBook)) {

return true;

}

}

return false;

}

/* The following contracts are designed for function 'findByTitle'*/

//TODO post-condition: the size of holdings is the same before and after executing this method //@ ensures

//TODO post-condition: each element in holdings should be the same before and after executing this method

//@ ensures

Book findByTitle(String atitle) { // find a book by its title

for (Book item : holdings) {

if (item.title.equals(atitle)) {

return item;

}

}

// If the book isn't found, return null;

return null;

}

}

// A class for books in a library

class Book {

String title;

String callNum;

int timesOut = 0;

boolean isAvailable = true;

// constructor

Book(String title, String callNum) {

this.title = title;

this.callNum = callNum;

}

// mark a book as checked out of the library

public Book checkOut() {

this.isAvailable = false;

this.timesOut = this.timesOut + 1;

return this;

}

// mark a book as checked in at the library

public Book checkIn() {

this.isAvailable = true;

return this;

}

@Override

public boolean equals(Object obj) {

if (this == obj) return true;

if (obj == null) return false;

if (getClass() != obj.getClass()) return false;

Book other = (Book) obj;

if (callNum == null) {

if (other.callNum != null) return false;

} else if (!callNum.equals(other.callNum)) return false;

if (isAvailable != other.isAvailable) return false;

if (timesOut != other.timesOut) return false;

if (title == null) {

if (other.title != null) return false;