Added report
This commit is contained in:
parent
abdcf30572
commit
4568a07f93
3 changed files with 364 additions and 2 deletions
|
@ -11,7 +11,6 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
|
||||||
- Class `math.Fraction`
|
- Class `math.Fraction`
|
||||||
- `static Fraction getFraction(int, int)` and `static Fraction getFraction(int, int, int)`
|
- `static Fraction getFraction(int, int)` and `static Fraction getFraction(int, int, int)`
|
||||||
- `static Fraction getReducedFraction(int, int)`
|
- `static Fraction getReducedFraction(int, int)`
|
||||||
- (TODO PICK OTHER 3 FROM HERE)
|
|
||||||
- `public int getDenominator()`
|
- `public int getDenominator()`
|
||||||
- `public Fraction negate()`
|
- `public Fraction negate()`
|
||||||
- `public Fraction abs()`
|
- `public Fraction abs()`
|
||||||
|
@ -27,7 +26,6 @@ revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
|
||||||
- `boolean isEmpty()`
|
- `boolean isEmpty()`
|
||||||
- `FluentBitSet flip(int)` and overloads
|
- `FluentBitSet flip(int)` and overloads
|
||||||
- (TODO) `FluentBitSet xor(FluentBitSet)`==> done/ to review
|
- (TODO) `FluentBitSet xor(FluentBitSet)`==> done/ to review
|
||||||
- (TODO) `byte[] toByteArray()` and `byte[] toLongArray()`
|
|
||||||
- (TODO) `FluentBitSet set(int)` ==> done/ to review
|
- (TODO) `FluentBitSet set(int)` ==> done/ to review
|
||||||
- (TODO) `int nextSetBit(int)` and `int previousSetBit(int)` ==> done
|
- (TODO) `int nextSetBit(int)` and `int previousSetBit(int)` ==> done
|
||||||
- (TODO) `int nextClearBit(int)` and `int previousClearBit(int)` ==>done
|
- (TODO) `int nextClearBit(int)` and `int previousClearBit(int)` ==>done
|
||||||
|
|
BIN
report.pdf
Normal file
BIN
report.pdf
Normal file
Binary file not shown.
364
report.tex
Normal file
364
report.tex
Normal file
|
@ -0,0 +1,364 @@
|
||||||
|
\documentclass[11pt,a4paper]{scrartcl}
|
||||||
|
\usepackage[utf8]{inputenc}
|
||||||
|
\usepackage[margin=2.25cm]{geometry}
|
||||||
|
\usepackage{hyperref}
|
||||||
|
\usepackage{listings}
|
||||||
|
\usepackage{xcolor}
|
||||||
|
\usepackage{lmodern}
|
||||||
|
\usepackage{booktabs}
|
||||||
|
\usepackage{graphicx}
|
||||||
|
\usepackage{float}
|
||||||
|
\usepackage{tikz}
|
||||||
|
\usepackage{listings}
|
||||||
|
\usepackage{pgfplots}
|
||||||
|
\usepackage{subcaption}
|
||||||
|
\setlength{\parindent}{0cm}
|
||||||
|
\setlength{\parskip}{0.3em}
|
||||||
|
\hypersetup{pdfborder={0 0 0}}
|
||||||
|
\usepackage[nomessages]{fp}
|
||||||
|
|
||||||
|
\definecolor{codegreen}{rgb}{0,0.6,0}
|
||||||
|
\definecolor{codegray}{rgb}{0.5,0.5,0.5}
|
||||||
|
\definecolor{codepurple}{rgb}{0.58,0,0.82}
|
||||||
|
\definecolor{backcolour}{rgb}{0.95,0.95,0.92}
|
||||||
|
|
||||||
|
\lstdefinestyle{mystyle}{
|
||||||
|
backgroundcolor=\color{backcolour},
|
||||||
|
commentstyle=\color{codegreen},
|
||||||
|
keywordstyle=\color{magenta},
|
||||||
|
keywordstyle=[2]{\color{olive}},
|
||||||
|
numberstyle=\tiny\color{codegray},
|
||||||
|
stringstyle=\color{codepurple},
|
||||||
|
basicstyle=\ttfamily\footnotesize,
|
||||||
|
breakatwhitespace=false,
|
||||||
|
breaklines=true,
|
||||||
|
captionpos=b,
|
||||||
|
keepspaces=true,
|
||||||
|
numbers=left,
|
||||||
|
numbersep=5pt,
|
||||||
|
showspaces=false,
|
||||||
|
showstringspaces=false,
|
||||||
|
showtabs=false,
|
||||||
|
tabsize=2,
|
||||||
|
aboveskip=0.8em,
|
||||||
|
belowcaptionskip=0.8em
|
||||||
|
}
|
||||||
|
\lstset{style=mystyle}
|
||||||
|
|
||||||
|
\geometry{left=2cm,right=2cm,top=2cm,bottom=3cm} % se serve spazio
|
||||||
|
\title{
|
||||||
|
\vspace{-5ex} % se serve spazio
|
||||||
|
Assignment 4 -- Software Design and Modelling \\\vspace{0.5cm}
|
||||||
|
\Large Applying Design by Contract to an Existing Project
|
||||||
|
\vspace{-1ex} % se serve spazio
|
||||||
|
}
|
||||||
|
\author{Filippo Casari \and Claudio Maggioni}
|
||||||
|
\date{\vspace{-3ex}} % se serve spazio
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
\maketitle
|
||||||
|
\tableofcontents
|
||||||
|
|
||||||
|
\section{Project Selection}
|
||||||
|
|
||||||
|
The aim of this project is to apply Design by Contract principle to a part of or a complete application by not altering the application behaviour. No restrictions are placed on the size or type of project, other than being hosted on GitHub or otherwise on a public website. \marginpar[right
|
||||||
|
text]{\color{white}\url{https://youtu.be/rdnpdJXgV0Q}}
|
||||||
|
|
||||||
|
|
||||||
|
We first consider the \href{https://github.com/vavr-io/vavr}{\textbf{vavr-io/vavr}} GitHub project,
|
||||||
|
a Java library containing some data structures useful for functional programming (e.g. ``maybe'' and ``either'' types). However, due to peculiar design choices in the library codebase allowing for concise client code, the interfaces provided have an insufficient number of query methods to effectively writed contracts, and therefore we discard the project.
|
||||||
|
|
||||||
|
We instead choose the \textit{Apache Commons Lang} library (\textbf{\href{https://github.com/apache/commons-lang}{\textbf{apache/commons-lang}}} on GitHub), an Apache Software Foundation\footnote{\url{https://apache.org}} sponsored support library for Java. We choose this project mainly for the support role it fulfills, as many classes implement data structures and collections that are independent from each other and implementing an easy to understand interface. Additionally, the library is written with classical Java software design principles allowing for a richer set of query methods to potentially use in contracts.
|
||||||
|
|
||||||
|
\subsection {The Apache Commons Lang Project}
|
||||||
|
According to GitHub, the project has 179 contributors as of October 30th, 2022.
|
||||||
|
|
||||||
|
All the source and test classes are contained within in the package \textit{org.apache.commons.lang3} or in a sub-package of that package. For the sake of brevity, this
|
||||||
|
prefix is omitted from now on when mentioning packages and classes in the project.
|
||||||
|
|
||||||
|
We choose to analyze the code at the \textit{git} revision \texttt{770e72d2f78361b14f3fe27caea41e5977d3c638} of the library.
|
||||||
|
|
||||||
|
According to GitHub, the project has more than 2,400 stars, more than 1,500 forks, 222 open issues on the Apache Commons JIRA instance\footnote{\url{https://issues.apache.org/jira/projects/LANG/}, as of
|
||||||
|
2022-12-06 (ISO 8601 date)}. We analyze some line of code metrics of the project by using the \textit{cloc} tool, which returns what shown in Table \ref{tab:cloc}.
|
||||||
|
|
||||||
|
\begin{table}[t]
|
||||||
|
\centering
|
||||||
|
\begin{tabular}{lllll}
|
||||||
|
\toprule
|
||||||
|
\textbf{Files} & Language & Blank & Comment & Code \\ \midrule
|
||||||
|
\textbf{464} & Java & 16792 & 63093 & 89748 \\
|
||||||
|
\textbf{30} & Text & 1852 & 0 & 11972 \\
|
||||||
|
\textbf{26} & XML & 408 & 530 & 3958 \\
|
||||||
|
\textbf{1} & Maven & 29 & 39 & 967 \\
|
||||||
|
\textbf{4} & Markdown & 40 & 0 & 271 \\
|
||||||
|
\textbf{1} & HTML & 13 & 16 & 236 \\
|
||||||
|
\textbf{5} & YAML & 37 & 96 & 152 \\
|
||||||
|
\textbf{1} & Velocity Template Language & 23 & 31 & 90 \\
|
||||||
|
\textbf{1} & Groovy & 12 & 22 & 81 \\
|
||||||
|
\textbf{1} & CSV & 1 & 0 & 16 \\
|
||||||
|
\textbf{1} & Properties & 3 & 19 & 3 \\
|
||||||
|
\textbf{1} & Bourne Shell & 0 & 2 & 2 \\ \midrule
|
||||||
|
\textbf{536} & SUM & 19210 & 63848 & 107496 \\ \bottomrule
|
||||||
|
\end{tabular}
|
||||||
|
\caption{\textit{cloc} output for the Apache Commons Lang project repository at revision \texttt{770e72d2f78361b14f3fe27caea41e5977d3c638}.}
|
||||||
|
\label{tab:cloc}
|
||||||
|
\end{table}
|
||||||
|
|
||||||
|
\subsection{Scope of Contract Implementation}
|
||||||
|
|
||||||
|
As the Apache Commons Lang project ostensibly provides utility classes and collections, the unit of functionality is often a single class. We therefore decide to select 4 classes on which to design contracts. For sake of brevity from here onward the prefix \textit{org.apache.commons.lang3} is omitted from each class name. The classes we choose are.
|
||||||
|
|
||||||
|
\begin{description}
|
||||||
|
\item[math.IEEE754rUtils] a utility class able to efficiently sort floating point arrays;
|
||||||
|
\item[math.Fraction] a class representing a fraction with an integer numerator and denominator;
|
||||||
|
\item[CharRange] a memory efficient implementation of a set of \texttt{char}s within a contiguous range;
|
||||||
|
\item[util.FluentBitSet] a memory efficient implementation of ordered list of bits supporting bitwise operations and fast random access.
|
||||||
|
\end{description}
|
||||||
|
|
||||||
|
We choose these classes as we feel they are a significant sample of the API the Apache Commons Lang offers, as it is mainly composed by utility classes and implementations of data structures that client developers may use to support their client code.
|
||||||
|
|
||||||
|
As the Commons Lang project has a rather complicated build system targeting different Java versions
|
||||||
|
and dividing sources and tests in different compilation modules, we decide to create a new project copying the sources of the aforementioned classes and the relevant tests. However, we have to make minor edits on the tests sources. This is because all test classes extend a generic setup class \textit{AbstractLangTest}, which performs some global tear down operations that are irrelevant in the scope of this assignment. Therefore, in our copy we remove the \texttt{extends} clause from all the tests. Additionally, part of both the source and test code performs some validation operations which depend on other utility classes in Commons Lang. We therefore include Commons Lang as a dependency to our project to allow this code to be compiled.
|
||||||
|
|
||||||
|
The resulting project can then be found in the branch \texttt{main} of the repository
|
||||||
|
|
||||||
|
\begin{center}
|
||||||
|
{\small\href{https://gitlab.com/usi-si-teaching/msde/2022-2023/software-design-and-modeling/assignment-4-dbc/group-1/}{usi-si-teaching/msde/2022-2023/software-design-and-modeling/assignment-4-dbc/group-1}}
|
||||||
|
\end{center}
|
||||||
|
|
||||||
|
on \textit{gitlab.com}.
|
||||||
|
|
||||||
|
We then run the \textit{cloc} tool again on these sources to provide a baseline for further analysis of the annotated code. The line of code metrics can be found in Table \ref{tab:before}.
|
||||||
|
|
||||||
|
\begin{table}[t]
|
||||||
|
\centering
|
||||||
|
\begin{tabular}{lllll}
|
||||||
|
\toprule
|
||||||
|
Files & Language & Blank & Comment & Code \\ \midrule
|
||||||
|
8 & Java & 706 & 1541 & 3342 \\
|
||||||
|
15 & XML & 0 & 0 & 1067 \\
|
||||||
|
6 & Text & 6 & 0 & 149 \\
|
||||||
|
1 & Maven & 4 & 0 & 54 \\
|
||||||
|
1 & Markdown & 3 & 0 & 7 \\ \midrule
|
||||||
|
31 & SUM & 719 & 1541 & 4619 \\ \bottomrule
|
||||||
|
\end{tabular}
|
||||||
|
\caption{\textit{cloc} output for the \textit{main} (not annotated) branch of the contracts project.}
|
||||||
|
\label{tab:before}
|
||||||
|
\end{table}
|
||||||
|
|
||||||
|
\begin{table}[t]
|
||||||
|
\centering
|
||||||
|
\begin{tabular}{lllll}
|
||||||
|
\toprule
|
||||||
|
Files & Language & Blank & Comment & Code \\ \midrule
|
||||||
|
13 & Java & 793 & 1667 & 3736 \\
|
||||||
|
15 & XML & 0 & 0 & 1058 \\
|
||||||
|
6 & Text & 6 & 0 & 149 \\
|
||||||
|
1 & Maven & 4 & 0 & 65 \\
|
||||||
|
1 & Markdown & 5 & 0 & 34 \\ \midrule
|
||||||
|
36 & SUM & 808 & 1667 & 5042 \\ \bottomrule
|
||||||
|
\end{tabular}
|
||||||
|
\caption{\textit{cloc} output for the \textit{annotated} branch of the contracts project.}
|
||||||
|
\label{tab:after}
|
||||||
|
\end{table}
|
||||||
|
|
||||||
|
\section{Approach to Contract Design}
|
||||||
|
|
||||||
|
Writing contracts for the classes we choose is quite easy, as documentation, tests and pre-existing exception-based argument checking paints a clear picture of how each public interface behaves. Therefore our approach is relatively straightforward.
|
||||||
|
|
||||||
|
To define a method contract, we first look at the aforementioned resources to understand the behaviour of class. If needed, we the precondition clause, considering both the existing sources in the method body and additional constraints on parameter values specified in the method documentation (though in our experience with these classes we can say the Commons Lang developers are quite thorough in their in-code assertions). We then define a postcondition clause when needed, taking count of the class's behaviour and the domain of return values.
|
||||||
|
|
||||||
|
To check if a contract is potentially defined in a wrong way we run the relevant test suite. With the exception of assertions relating to precondition violations (an issue discussed in Section \ref{sec:test}), the unit tests are as effective with the original code as they are with the asserted code. This allows to check that our changes do not alter the intended behaviour of each class and additionally gives \textit{jSicko} many opportunities to evaluate preconditions and postconditions with test data.
|
||||||
|
|
||||||
|
All the contracts we implement do not rely on any change on the original source code other than \textit{jSicko} clause definitions and adding \texttt{@Pure} annotations to query methods.
|
||||||
|
|
||||||
|
\section{Contract Implementation}
|
||||||
|
|
||||||
|
In order to implement design by contract, we use version 1.0.0 of the \href{https://gitlab.com/usi-si-oss/codelounge/jSicko}{\textbf{jSicko}} contract checking library written by Dr.\ Andrea Mocci. The library allows definitions of preconditions and postconditions in \texttt{default} methods of interfaces which contracted class reference. We define a total of 18 preconditions and 38 postconditions. We define contracts for both command methods and query methods, using the latter ones to define a more detailed domain of the values returned and to describe inter-dependencies between queries. With the exception of \textit{math.IEEE754rUtilsContracts}, the contracts we define are not complete as they do not span all the side effects caused by the command methods and all the inter-dependencies between the query methods.
|
||||||
|
|
||||||
|
The resulting code after contract implementation can then be found in the \texttt{annotated} branch of the repository
|
||||||
|
|
||||||
|
\begin{center}
|
||||||
|
{\small\href{https://gitlab.com/usi-si-teaching/msde/2022-2023/software-design-and-modeling/assignment-4-dbc/group-1/}{usi-si-teaching/msde/2022-2023/software-design-and-modeling/assignment-4-dbc/group-1}}
|
||||||
|
\end{center}
|
||||||
|
|
||||||
|
on \textit{gitlab.com}. We now specify the methods our contracts apply to and in which interfaces the matching contracts can be found.
|
||||||
|
|
||||||
|
The interface \textit{math.IEEE754rUtilsContracts} implements a complete set of contracts for the methods of class \\\textit{math.IEEE754rUtils}, namely:
|
||||||
|
\begin{itemize}
|
||||||
|
\item \texttt{static double min(double[])} and overloads;
|
||||||
|
\item \texttt{static double max(double[])} and overloads.
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
The interface \textit{CharRangeContracts} implements the contract of method \texttt{boolean\ contains(CharRange)} of class \textit{CharRange}.
|
||||||
|
|
||||||
|
The interface \textit{math.IEEE754rUtilsContracts} implements contracts for some methods of class\\ \textit{math.Fraction}, namely:
|
||||||
|
\begin{itemize}
|
||||||
|
\item
|
||||||
|
\texttt{static\ Fraction\ getFraction(int,\ int)} and\\
|
||||||
|
\texttt{static\ Fraction\ getFraction(int,\ int,\ int)};
|
||||||
|
\item
|
||||||
|
\texttt{static\ Fraction\ getReducedFraction(int,\ int)};
|
||||||
|
\item
|
||||||
|
\texttt{public\ int\ getDenominator()};
|
||||||
|
\item
|
||||||
|
\texttt{public\ Fraction\ negate()};
|
||||||
|
\item
|
||||||
|
\texttt{public\ Fraction\ abs()};
|
||||||
|
\item
|
||||||
|
\texttt{public\ Fraction\ reduce()}.
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
Finally, the interface \textit{util.FluentBitSet} implements contracts for some methods in the \textit{util.FluentBitSet} class, namely:
|
||||||
|
\begin{itemize}
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ and(FluentBitSet)} and overloads;
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ andNot(FluentBitSet)} and overloads;
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ or(FluentBitSet)} and overloads;
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ clear()} and overloads;
|
||||||
|
\item
|
||||||
|
\texttt{boolean\ get(int)} and overloads;
|
||||||
|
\item
|
||||||
|
\texttt{boolean\ isEmpty()};
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ flip(int)} and overloads;
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ xor(FluentBitSet)};
|
||||||
|
\item
|
||||||
|
\texttt{FluentBitSet\ set(int)};
|
||||||
|
\item
|
||||||
|
\texttt{int\ nextSetBit(int)} and
|
||||||
|
\texttt{int\ previousSetBit(int)};
|
||||||
|
\item
|
||||||
|
\texttt{int\ nextClearBit(int)} and
|
||||||
|
\texttt{int\ previousClearBit(int)} .
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
After implementing the aforementioned contracts we run the \textit{cloc} tool again to understand
|
||||||
|
the impact of contract code on source code metrics. Results are shown in Table \ref{tab:after}.
|
||||||
|
|
||||||
|
The following sections go in further detail on the implementation of some contracts, providing additional insight on the strategies we use for defining them.
|
||||||
|
|
||||||
|
\subsection{Bitwise Operations and the \textit{FluentBitSet}}
|
||||||
|
|
||||||
|
We worked on the class \textit{util.FluentBitSet}, which is an alternative implementation of class \textit{java.util.BitSet} providing some additional operations.
|
||||||
|
|
||||||
|
The original \textit{BitSet} class implements a bit vector that expands as necessary. Bits are represented as \texttt{boolean} values, while non-negative integers serve as indexes for accessing them. The class allows to inspect, set, or clear certain indexed bits. Various bitwise logical operations can be applied to a \textit{BitSet} to change its contents without changing the contents of another \textit{BitSet}.
|
||||||
|
|
||||||
|
The \textit{util.FluentBitSet} class varies from \textit{BitSet} as it allows its command methods to return \texttt{this} to allow more succinct client code. This style of command methods is called ``fluent'', hence the name of the class.
|
||||||
|
|
||||||
|
\subsubsection{The \textit{xor} Command Method}
|
||||||
|
|
||||||
|
\begin{lstlisting}[caption=Postcondition declaration for the \textit{xor} command method in the \textit{util.FluentBitSet} class., language=java, label=lst:post_xor]
|
||||||
|
@Ensures("xor_fbs")
|
||||||
|
public FluentBitSet xor(final BitSet set)
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
\begin{lstlisting}[caption=Matching postcondition clause for the \textit{xor} command method in the \textit{util.FluentBitSet} class.,language=java,label=lst:xorfbs]
|
||||||
|
@Pure
|
||||||
|
default boolean xor_fbs(final FluentBitSet returns, final BitSet set) {
|
||||||
|
int card1 = old(this).cardinality();
|
||||||
|
int card2 = set.cardinality();
|
||||||
|
final boolean bool;
|
||||||
|
if (card1 + card2 > this.length()) {
|
||||||
|
bool = (card1 + card2 - this.length()) >= this.cardinality();
|
||||||
|
return bool && test_length(returns, set::length);
|
||||||
|
} else {
|
||||||
|
return (card1 + card2) >= this.cardinality();
|
||||||
|
}
|
||||||
|
}
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
In order to write clauses for this method we use the \texttt{int cardinality()} query method. The cardinality of a \textit{FluentBitSet} is the total number of bits set to 1. We additionally use the \texttt{int length()} query method, returning the position of the most significant bit set to 1 in the set.
|
||||||
|
|
||||||
|
The \texttt{FluentBitSet xor(FluentBitSet)} is a command method in \textit{FluentBitSet} performing an in-place bitwise exclusive-or operation with another set instance, and returning this instance.
|
||||||
|
|
||||||
|
In the contract (shown in Listing \ref{lst:xorfbs}) we say that when the sum of the cardinalities of the old \textit{FluentBitSet} state and the argument are greater than the returned length, the cardinality of the returned object must be less than the sum of the cardinalities of the old state and the argument minus the length of the new state.
|
||||||
|
|
||||||
|
For instance, let us consider:
|
||||||
|
|
||||||
|
\texttt{old(this).cardinality() = set.cardinality() = 8}, \texttt{this.cardinality() = 0},\\ and \texttt{this.length() = 8}
|
||||||
|
|
||||||
|
then $(8 + 8 - 8)$ is greater or equal to $0$, where $0$ is the cardinality of the new state. In contrary, if the sum is not greater than the length of the \textit{FluentBitSet} we have:
|
||||||
|
|
||||||
|
\texttt{old(this).cardinality() = 0}, \texttt{set.cardinality() = 8}, \texttt{this.cardinality() = 8},\\ and \texttt{this.length() = 8}
|
||||||
|
|
||||||
|
then $(8 + 0 - 8)$ is greater or equal to $0$, where 0 is the cardinality of the result of the \textit{xor} operation.
|
||||||
|
|
||||||
|
\subsubsection{The \textit{isEmpty} Query Method}
|
||||||
|
|
||||||
|
\begin{lstlisting}[label=lst:empty_method, language=java, caption=Postcondition declaration for the \textit{isEmpty} query method in the \textit{util.FluentBitSet} class.]
|
||||||
|
@Pure
|
||||||
|
@Ensures("is_empty")
|
||||||
|
public boolean isEmpty()
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
\begin{lstlisting}[caption=Matching postcondition clause for the \textit{isEmpty} query method in the \textit{util.FluentBitSet} class.,language=java,label=lst:xorfbs, label=lst:empty, language=java]
|
||||||
|
@Pure
|
||||||
|
default boolean is_empty(final boolean returns) {
|
||||||
|
return returns == (cardinality() == 0) && returns == (length() == 0);
|
||||||
|
}
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
We additionally define a postcondition clause for the \texttt{boolean isEmpty()} query method, returning \texttt{true} when all bits in the sets are 0. This condition trivially is true if and only if its \textit{length} is also 0, and our contract indeed checks this fact.
|
||||||
|
|
||||||
|
\subsection{Fraction Arithmetic and the \textit{Fraction} Class}
|
||||||
|
|
||||||
|
Our contracts for the \textit{math.Fraction} class are defined in the interface \textit{math.FractionContracts}. \textit{Fraction} is a class that extends \textit{Number} and implements an arithmetic fraction compose of an integer numerator and denominator. This class is immutable, inter-operates with most methods that accept a \textit{Number} instance. We report below the methods on which we implemented contracts.
|
||||||
|
|
||||||
|
\subsubsection{The \textit{Negate} Query Method}
|
||||||
|
|
||||||
|
\begin{lstlisting}[label=lst:negate, language=java, caption=Postcondition declaration for the \textit{negate} query method in \textit{math.Fraction}.]
|
||||||
|
@Pure
|
||||||
|
@Ensures("check_if_negative")
|
||||||
|
// [clause omitted]
|
||||||
|
public Fraction negate()
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
\begin{lstlisting}[label=lst:negate_post, language=java, caption=Matching postcondition clause for the \textit{negate} query method in \textit{math.Fraction}.]
|
||||||
|
@Pure
|
||||||
|
default boolean check_if_negative(final Fraction returns) {
|
||||||
|
if ((this.getNumerator() > 0 && this.getDenominator() > 0) ||
|
||||||
|
(this.getNumerator() < 0 && this.getDenominator() < 0)) {
|
||||||
|
return returns.getNumerator() < 0;
|
||||||
|
}
|
||||||
|
return returns.getNumerator() > 0;
|
||||||
|
}
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
Here we want to make sure that the returned \textit{Fraction} instance will be positive if the starting fraction was negative, and vice versa. Consequently, we adopt the clause shown in Listing \ref{lst:negate_post} as a postcondition of the method negate (shown in Listing \ref{lst:negate}). This an instance of the aforementioned inter-dependencies between query method behaviours.
|
||||||
|
|
||||||
|
\subsubsection{The \textit{getDenominator} Query Method}
|
||||||
|
|
||||||
|
\begin{lstlisting}[label=lst:get_den, language=java, caption=Postcondition declaration for the \textit{getDenominator} query method in \textit{math.Fraction}.]
|
||||||
|
@Ensures("non_zero_den")
|
||||||
|
public int getDenominator()
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
\begin{lstlisting}[label=lst:non_zero, language=java, caption=Matching postcondition clause for the \textit{getDenominator} query method in \textit{math.Fraction}.]
|
||||||
|
default boolean non_zero_den(final int returns) {
|
||||||
|
return returns != 0;
|
||||||
|
}
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
Here we introduce a simple postcondition checking a property that any fraction denominator has, namely that it is different from $0$. This is an instance of a contract used to restrict the domain of the return value further than its type definition is able to capture.
|
||||||
|
|
||||||
|
\section{Unit Tests and Code Contracts}
|
||||||
|
\label{sec:test}
|
||||||
|
|
||||||
|
The only issue we find in implementing contracts has to do with test checking operations that result in precondition violations. As some preconditions are defensively checked by the original Commons Lang code, some tests check the thrown exception type to be exactly the one thrown in the check. As \textit{jSicko} checks preconditions before method entry, and \textit{jSicko} throws a special exception (namely a child of \textit{AssertionError}) when preconditions are violated, the assertions for the original source code fail as the thrown exception type is does not match the expected one.
|
||||||
|
|
||||||
|
To solve this error, we simply modify to all these assertions to allow for \textit{AssertionError}s. For JUnit \texttt{assertThrows(...)} assertions we change the expected thrown type to be \textit{Throwable}, as there is no more specific type that is both an \textit{Error} and a \textit{RuntimeException}. These alterations and \textit{jSicko} contract code are the only changes we perform on the source code from Apache Commons Lang.
|
||||||
|
|
||||||
|
\section{Conclusions}
|
||||||
|
|
||||||
|
Apache Commons Lang is a Java project using well-established traditional design best practices. This is quite handy as its implementation can be easily understood and the project is well documented. The project also implements a variety of design patterns, making this contract implementation quite diverse as different classes are implemented in different ways beside domain-specific logic. For instance, the utility class \textit{math.IEEE754rUtils} allows us to test \textit{jSicko}'s ability to contract check static methods, and we can say it does that effectively from the experience we gathered.
|
||||||
|
|
||||||
|
The process used to write contracts in this assignment can be applied to other projects similar to Apache Commons Lang with respect to documentation availability and the set of Java programming language features use. However, we speculate the approach would need to be changed for projects with
|
||||||
|
inadequate documentation or using newer or more advanced features of the Java language (like proxies), which may be able to break the internal abstractions used by \textit{jSicko}.
|
||||||
|
|
||||||
|
\end{document}
|
||||||
|
|
Reference in a new issue