SE-2832 Introduction to Software Verification

Dr. Mark Sebern -- Spring quarter 2013-2014

Lab 2

Revised: 19 March 2014


This lab was developed by Dr. Walt Schilling; all errors in its adaptation are the responsibility of the instructor.


In this lab, you will use EclEmma to collect code coverage metrics that may provide some insight into the effectiveness of tests written for a target application.

Tool installation

Install the EclEmma Eclipse plugin:

  1. From the Eclipse Help menu, select Install New Software....
  2. Click on Add... to add a new repository site.
  3. Enter "EclEmma" in the Name field and "" in the Location field, and click OK.
  4. Select "EclEmma" in the list of available software and click Next >.
  5. Complete the rest of the usual Eclipse plugin installation steps, including accepting the license.

Normal unit test execution

Next, download two versions of the lab project code:

Now, unZIP the first (non-alternate) version of the project code and make an Eclipse project incorporating it, adding the JUnit4 library to the build path. Then run the JUnit tests in, to make sure they are set up correctly.

Initial coverage testing

In Eclipse, open the following files so they are displayed in the source code tabs:

In the Eclipse Package Explorer, right-click on the JUnit test tile ( and select Coverage As->JUnit Test. The coverage summary should appear in the Coverage window (located in the console area). You can expand the items in the Element column to see which methods have been tested and their level of coverage. You can also double-click on a filename in the Coverage window, to bring it up in a source code window, where lines should be marked with the following colors to show execution coverage:

To export a copy of the coverage report in HTML:

Alternate coverage testing

Next, repeat the coverage testing process with a second project incorporating the "alternate version" files. This ZIP file contains only the program source code, so you'll have to copy over the tests from the first project.

Re-run the coverage analysis for the tests and compare the results with the original version.

Test case improvement

Based on the coverage results, write new test cases to improve the code coverage. See whether you can reach 100% coverage for both implementations, and reflect on the reasons why you were successful (or not) in doing so.

Assignment submission (due by 11:59PM CDT, Monday, March 24)

Prepare a PDF report (named "SE2832-username-Lab2.pdf", where "username" is your MSOE email username) on your lab experience, including:

Put this report in the top-level directory of your first ("non-alternate") project.

Submit that projects (i.e., your Eclipse project trees, including your report in the first one) using git to your personal Bitbucket repository (""), committing them to branches "lab2" and "lab2alt" (not "master"); if you are not sure how to do this, ask the instructor for assistance in lab. Note that your MSOE username and Bitbucket username may differ, but the repository path incorporates your MSOE username (even though you may need to log in to Bitbucket with a different username). DO NOT submit your bin (class files) directory tree! Use .gitignore to skip the .class files.

Appendix: Tax Law

This information courtesy of Dr. Schilling.

Taxes are complex, but for this assignment, they have been simplified.

Filing Status and Obligation to File

The first thing of importance is the person’s filing status and whether he or she is required to file a return at all. A return may indicate that a person is:

While you will not need to check the conditions that would quality a person to file using one of these categories, you will need to use the categories to test your program.

Depending on the filing status, a person is required to file an income tax return with the IRS if the criteria of Table 1 are met.

Table 1. 2008 Filing Requirements Chart for Most Taxpayers (From IRS Publication 501)

IF your filing status is... AND at the end of 2008 you were... THEN file a return if your gross income was at least...
Single Under 65 $8950
65 or older $10300
Head of household Under 65 $11500
65 or older $12850
Married, filing jointly Under 65 (both spouses) $17900
65 or older (one spouse) $18950
65 or older (both spouses) $20000
Married, filing separately Any age $3500
Qualifying widow(er) Under 65 $14400
65 or older $15450

The constructors for the Tax Calculator are responsible for accepting the name of the filer, the type of filer, and the filer’s age, along with the spouse’s age if the filing status is married (separate or joint filing).

Taxable Income

Income tax is based upon the taxable income of the filer. The taxable income is determined by taking the gross income and subtracting the standard deduction from this amount. The standard deduction amount depends on the filing status and the age of the filer. This information is provided in Table 2.

Table 2. Standard Deduction

Filing Status Base Standard Deduction
Single $5450
Married, filing separately $5450
Head of household $8000
Married, filing jointly $10900
Qualifying widow(er) $10900

In addition to the base standard deductions, the standard deductions are increased by $1050 for each person on the return who is age 65 or older. For example, a couple who is filing jointly and has the ages of 72 and 71 would have a standard deduction of $13000. The amount of tax is calculated based upon a sliding scale. For example, a single person making less than 8025 would simply pay 10% on their income. However, if they made more than $32550, they would pay 10% on the first $8025, 15% on the amount between $8025 and $32550, and 25% on the remaining income.


Jill, age 19, is in college and works part time as a waitress. Each year, she makes a total of $7500.00. Because her income is so low, she is not required by law to file a return. Her taxable income, if she did file, would be $2050.00, and she would be responsible for a total of $205.00 in taxes. While she is not required to file a return, it may be advantageous since, if more than $205.00 has been withheld from her paychecks, she may be able to receive a refund.

Jill’s boyfriend Mark, also 19, works as a pizza delivery driver. Each year, he makes a total of $11,000.00. He must file a return, as his income is greater than $8950.00. His standard deduction is $5450.00, making his taxable income $11,000.00-$5450.00=$5550.00. His tax due is 10% of his taxable income, yielding a net tax rate of 5.045%.

Oil tycoon, age 95, John D. Rockerfeller earns 5,000,000.00 a year and is single. He must file a return. Because of his age, his standard deduction is $6500.00, yielding taxable income of $4,993,500.00. On his income, he pays a total tax of $1,726,321.75, yielding a net tax rate of 34.526%.