Added submission

README.md

@@ -3,6 +3,33 @@
 Classes come from [https://github.com/apache/commons-lang](https://github.com/apache/commons-lang)
 revision `770e72d2f78361b14f3fe27caea41e5977d3c638`
 
+## List of semantically different functions with contracts
+
+- Class `math.IEEE754rUtils`:
+  - `static double min(double[])` and overloads 
+  - `static double max(double[])` and overloads
+- Class `math.Fraction`
+  - `static Fraction getFraction(int, int)` and `static Fraction getFraction(int, int, int)`
+  - `static Fraction getReducedFraction(int, int)`
+  - `public int getDenominator()`
+  - `public Fraction negate()`
+  - `public Fraction abs()`
+  - `public Fraction reduce()`
+- Class `CharRange`
+  - `boolean contains(CharRange)`
+- Class `util.FluentBitSet`
+  - `FluentBitSet and(FluentBitSet)` and overloads
+  - `FluentBitSet andNot(FluentBitSet)` and overloads
+  - `FluentBitSet or(FluentBitSet)` and overloads
+  - `FluentBitSet clear()` and overloads
+  - `boolean get(int)` and overloads
+  - `boolean isEmpty()`
+  - `FluentBitSet flip(int)` and overloads
+  - (TODO) `FluentBitSet xor(FluentBitSet)`==> done/ to review
+  - (TODO) `FluentBitSet set(int)` ==> done/ to review
+  - (TODO) `int nextSetBit(int)` and `int previousSetBit(int)` ==> done
+  - (TODO) `int nextClearBit(int)` and `int previousClearBit(int)` ==>done
+
 ## Run Tests
 
 ```

pom.xml

@@ -15,6 +15,11 @@
     </properties>
 
     <dependencies>
+        <dependency>
+            <groupId>ch.usi.si.codelounge</groupId>
+            <artifactId>jSicko</artifactId>
+            <version>1.0.0</version>
+        </dependency>
         <dependency>
             <groupId>org.apache.commons</groupId>
             <artifactId>commons-lang3</artifactId>
@@ -40,6 +45,12 @@
                 <groupId>org.apache.maven.plugins</groupId>
                 <artifactId>maven-compiler-plugin</artifactId>
                 <version>3.10.1</version>
+                <configuration>
+                    <compilerArgs>
+                        <arg>-parameters</arg>
+                        <arg>-Xplugin:JSickoContractCompiler</arg>
+                    </compilerArgs>
+                </configuration>
             </plugin>
             <plugin>
                 <groupId>org.apache.maven.plugins</groupId>

report.tex

@@ -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}
+

src/main/java/ch/usi/inf/sdm/sdm04/CharRange.java

@@ -32,7 +32,7 @@ import java.util.Objects;
  */
 // TODO: This is no longer public and will be removed later as CharSet is moved
 //  to depend on Range.
-final class CharRange implements Iterable<Character>, Serializable {
+final class CharRange implements Iterable<Character>, Serializable, CharRangeContracts {
 
     /**
      * Required for serialization support. Lang version 2.0.
@@ -156,6 +156,8 @@ final class CharRange implements Iterable<Character>, Serializable {
      *
      * @return the start char (inclusive)
      */
+    @Pure
+    @Override
     public char getStart() {
         return this.start;
     }
@@ -165,6 +167,8 @@ final class CharRange implements Iterable<Character>, Serializable {
      *
      * @return the end char (inclusive)
      */
+    @Pure
+    @Override
     public char getEnd() {
         return this.end;
     }
@@ -177,6 +181,8 @@ final class CharRange implements Iterable<Character>, Serializable {
      *
      * @return {@code true} if negated
      */
+    @Pure
+    @Override
     public boolean isNegated() {
         return negated;
     }
@@ -188,6 +194,9 @@ final class CharRange implements Iterable<Character>, Serializable {
      * @param ch the character to check
      * @return {@code true} if this range contains the input character
      */
+    @Pure
+    @Override
+    @Ensures("contains_uses_start_end_range")
     public boolean contains(final char ch) {
         return (ch >= start && ch <= end) != negated;
     }
@@ -200,6 +209,9 @@ final class CharRange implements Iterable<Character>, Serializable {
      * @return {@code true} if this range entirely contains the input range
      * @throws NullPointerException if {@code null} input
      */
+    @Pure
+    @Requires("char_range_is_not_null")
+    @Ensures("characters_in_param_are_in_this")
     public boolean contains(final CharRange range) {
         Objects.requireNonNull(range, "range");
         if (negated) {

src/main/java/ch/usi/inf/sdm/sdm04/CharRangeContracts.java

@@ -0,0 +1,55 @@
+/*  __    __  __  __    __  ___
+ * \  \  /  /    \  \  /  /  __/
+ *  \  \/  /  /\  \  \/  /  /
+ *   \____/__/  \__\____/__/
+ *
+ * Copyright 2014-2017 Vavr, http://vavr.io
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ch.usi.inf.sdm.sdm04;
+
+import ch.usi.si.codelounge.jsicko.Contract;
+
+import java.util.stream.StreamSupport;
+
+@SuppressWarnings("unused") // methods used by jSicko
+public interface CharRangeContracts extends Contract {
+
+    @Pure
+    char getStart();
+
+    @Pure
+    char getEnd();
+
+    @Pure
+    boolean isNegated();
+
+    @Pure
+    boolean contains(final char ch);
+
+    @Pure
+    default boolean char_range_is_not_null(final CharRange range) {
+        return range != null;
+    }
+
+    @Pure
+    default boolean contains_uses_start_end_range(final boolean returns, final char ch) {
+        return returns == (this.isNegated() != (this.getStart() <= ch && this.getEnd() >= ch));
+    }
+
+    @Pure
+    default boolean characters_in_param_are_in_this(final boolean returns, final CharRange range) {
+        return returns == StreamSupport.stream(range.spliterator(), false).allMatch(this::contains);
+    }
+}

src/main/java/ch/usi/inf/sdm/sdm04/math/Fraction.java

@@ -32,7 +32,7 @@ import java.util.Objects;
  *
  * @since 2.0
  */
-public final class Fraction extends Number implements Comparable<Fraction> {
+public final class Fraction extends Number implements Comparable<Fraction>, FractionContracts {
 
     /**
      * Required for serialization support. Lang version 2.0.
@@ -137,6 +137,8 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @throws ArithmeticException if the denominator is {@code zero}
      * or the denominator is {@code negative} and the numerator is {@code Integer#MIN_VALUE}
      */
+    @Pure
+    @Requires("get_fraction_pre")
     public static Fraction getFraction(int numerator, int denominator) {
         if (denominator == 0) {
             throw new ArithmeticException("The denominator must not be zero");
@@ -167,6 +169,9 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @throws ArithmeticException if the resulting numerator exceeds
      *  {@code Integer.MAX_VALUE}
      */
+    @Pure
+    @Requires("get_fraction_whole_pre")
+    @Ensures("get_whole_fraction_post")
     public static Fraction getFraction(final int whole, final int numerator, final int denominator) {
         if (denominator == 0) {
             throw new ArithmeticException("The denominator must not be zero");
@@ -203,6 +208,8 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @return a new fraction instance, with the numerator and denominator reduced
      * @throws ArithmeticException if the denominator is {@code zero}
      */
+    @Requires("get_reduced_fraction_pre")
+    @Ensures("get_reduced_fraction_post")
     public static Fraction getReducedFraction(int numerator, int denominator) {
         if (denominator == 0) {
             throw new ArithmeticException("The denominator must not be zero");
@@ -361,6 +368,7 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      *
      * @return the denominator fraction part
      */
+    @Ensures("non_negative_den")
     public int getDenominator() {
         return denominator;
     }
@@ -449,6 +457,7 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      *
      * @return a new reduced fraction instance, or this if no simplification possible
      */
+    @Ensures("must_be_reduced")
     public Fraction reduce() {
         if (numerator == 0) {
             return equals(ZERO) ? this : ZERO;
@@ -489,6 +498,9 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      *
      * @return a new fraction instance with the opposite signed numerator
      */
+    //@Requires("check_if_non_min_val")
+    @Ensures("check_if_negative")
+    @Requires("check_if_non_min_val")
     public Fraction negate() {
         // the positive range is one smaller than the negative range of an int.
         if (numerator==Integer.MIN_VALUE) {
@@ -506,6 +518,7 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @return {@code this} if it is positive, or a new positive fraction
      *  instance with the opposite signed numerator
      */
+    @Ensures("must_positive")
     public Fraction abs() {
         if (numerator >= 0) {
             return this;
@@ -845,6 +858,7 @@ public final class Fraction extends Number implements Comparable<Fraction> {
      * @throws NullPointerException if the object is {@code null}
      */
     @Override
+    @Pure
     public int compareTo(final Fraction other) {
         if (this == other) {
             return 0;

src/main/java/ch/usi/inf/sdm/sdm04/math/FractionContracts.java

@@ -0,0 +1,109 @@
+/*  __    __  __  __    __  ___
+ * \  \  /  /    \  \  /  /  __/
+ *  \  \/  /  /\  \  \/  /  /
+ *   \____/__/  \__\____/__/
+ *
+ * Copyright 2014-2017 Vavr, http://vavr.io
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ch.usi.inf.sdm.sdm04.math;
+
+import ch.usi.si.codelounge.jsicko.Contract;
+
+import static ch.usi.si.codelounge.jsicko.Contract.old;
+
+@SuppressWarnings("unused") // used by jSicko
+public interface FractionContracts extends Contract {
+
+    default boolean non_negative_den(final int returns) {
+        return returns != 0.;
+    }
+
+    @Pure
+    Fraction negate();
+
+    @Pure
+    int getDenominator();
+
+    @Pure
+    int getNumerator();
+
+    @Pure
+    default boolean check_if_non_min_val() {
+        return this.getNumerator() != Integer.MIN_VALUE;
+    }
+
+    @Pure
+    default boolean must_positive(Fraction returns) {
+        return returns.getNumerator() >= 0;
+    }
+
+    @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;
+    }
+
+    @Pure
+    default boolean must_be_reduced(Fraction returns) {
+        int den = returns.getDenominator();
+        int num = returns.getNumerator();
+        if(num==0){
+            return true;
+        }
+        if( num>den){
+            return (num % den == num);
+        } else if (num<den && num>0 ) {
+            return (num%den == num);
+        }
+        return true;
+
+    }
+
+    @Pure
+    static boolean get_fraction_pre(final int numerator, final int denominator) {
+        return denominator != 0 && (denominator > 0 ||
+                (numerator != Integer.MIN_VALUE && denominator != Integer.MIN_VALUE));
+    }
+
+    @Pure
+    static boolean get_reduced_fraction_pre(final int numerator, final int denominator) {
+        return denominator != 0 && (numerator != 0 || denominator != Integer.MIN_VALUE);
+    }
+
+    @Pure
+    static boolean get_fraction_whole_pre(final int whole, final int numerator, final int denominator) {
+        final long numeratorValue = whole * (long) denominator + (long) (whole > 0 ? 1 : -1) * numerator;
+        return numerator >= 0 && denominator > 0 &&
+                numeratorValue >= Integer.MIN_VALUE && numeratorValue <= Integer.MAX_VALUE;
+    }
+
+    @Pure
+    static boolean get_reduced_fraction_post(final Fraction returns, final int numerator, final int denominator) {
+        final Fraction f = Fraction.getFraction(numerator, denominator);
+        return returns.compareTo(f) == 0;
+    }
+
+    @Pure
+    static boolean get_whole_fraction_post(final Fraction returns, final int whole, final int numerator, final int denominator) {
+        final long numeratorValue = whole * (long) denominator + (long) (whole < 0 ? -1 : 1) * numerator;
+        final Fraction calc = Fraction.getFraction((int) numeratorValue, denominator);
+        return returns.compareTo(calc) == 0;
+    }
+}

src/main/java/ch/usi/inf/sdm/sdm04/math/IEEE754rUtils.java

@@ -27,7 +27,7 @@ import java.util.Objects;
  *
  * @since 2.4
  */
-public class IEEE754rUtils {
+public class IEEE754rUtils implements IEEE754rUtilsContracts {
 
     /**
      * Returns the minimum value in an array.
@@ -38,6 +38,8 @@ public class IEEE754rUtils {
      * @throws IllegalArgumentException if {@code array} is empty
      * @since 3.4 Changed signature from min(double[]) to min(double...)
      */
+    @Requires("non_null_non_empty_arg")
+    @Ensures("is_minimum_element")
     public static double min(final double... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
@@ -60,6 +62,8 @@ public class IEEE754rUtils {
      * @throws IllegalArgumentException if {@code array} is empty
      * @since 3.4 Changed signature from min(float[]) to min(float...)
      */
+    @Requires("non_null_non_empty_arg_float")
+    @Ensures("is_minimum_element_float")
     public static float min(final float... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
@@ -83,6 +87,7 @@ public class IEEE754rUtils {
      * @param c value 3
      * @return the smallest of the values
      */
+    @Ensures("is_minimum_element_3")
     public static double min(final double a, final double b, final double c) {
         return min(min(a, b), c);
     }
@@ -96,6 +101,7 @@ public class IEEE754rUtils {
      * @param b value 2
      * @return the smallest of the values
      */
+    @Ensures("is_minimum_element_2")
     public static double min(final double a, final double b) {
         if (Double.isNaN(a)) {
             return b;
@@ -116,6 +122,7 @@ public class IEEE754rUtils {
      * @param c value 3
      * @return the smallest of the values
      */
+    @Ensures("is_minimum_element_3_float")
     public static float min(final float a, final float b, final float c) {
         return min(min(a, b), c);
     }
@@ -129,6 +136,7 @@ public class IEEE754rUtils {
      * @param b value 2
      * @return the smallest of the values
      */
+    @Ensures("is_minimum_element_2_float")
     public static float min(final float a, final float b) {
         if (Float.isNaN(a)) {
             return b;
@@ -148,6 +156,8 @@ public class IEEE754rUtils {
      * @throws IllegalArgumentException if {@code array} is empty
      * @since 3.4 Changed signature from max(double[]) to max(double...)
      */
+    @Requires("non_null_non_empty_arg")
+    @Ensures("is_maximum_element")
     public static double max(final double... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
@@ -170,6 +180,8 @@ public class IEEE754rUtils {
      * @throws IllegalArgumentException if {@code array} is empty
      * @since 3.4 Changed signature from max(float[]) to max(float...)
      */
+    @Requires("non_null_non_empty_arg_float")
+    @Ensures("is_maximum_element_float")
     public static float max(final float... array) {
         Objects.requireNonNull(array, "array");
         Validate.isTrue(array.length != 0, "Array cannot be empty.");
@@ -193,6 +205,7 @@ public class IEEE754rUtils {
      * @param c value 3
      * @return the largest of the values
      */
+    @Ensures("is_maximum_element_3")
     public static double max(final double a, final double b, final double c) {
         return max(max(a, b), c);
     }
@@ -206,6 +219,7 @@ public class IEEE754rUtils {
      * @param b value 2
      * @return the largest of the values
      */
+    @Ensures("is_maximum_element_2")
     public static double max(final double a, final double b) {
         if (Double.isNaN(a)) {
             return b;
@@ -226,6 +240,7 @@ public class IEEE754rUtils {
      * @param c value 3
      * @return the largest of the values
      */
+    @Ensures("is_maximum_element_3_float")
     public static float max(final float a, final float b, final float c) {
         return max(max(a, b), c);
     }
@@ -239,6 +254,7 @@ public class IEEE754rUtils {
      * @param b value 2
      * @return the largest of the values
      */
+    @Ensures("is_maximum_element_2_float")
     public static float max(final float a, final float b) {
         if (Float.isNaN(a)) {
             return b;

src/main/java/ch/usi/inf/sdm/sdm04/math/IEEE754rUtilsContracts.java

@@ -0,0 +1,98 @@
+/*  __    __  __  __    __  ___
+ * \  \  /  /    \  \  /  /  __/
+ *  \  \/  /  /\  \  \/  /  /
+ *   \____/__/  \__\____/__/
+ *
+ * Copyright 2014-2017 Vavr, http://vavr.io
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ch.usi.inf.sdm.sdm04.math;
+
+import ch.usi.si.codelounge.jsicko.Contract;
+
+import java.util.stream.DoubleStream;
+import java.util.stream.IntStream;
+
+@SuppressWarnings("unused") // methods used by jSicko
+public interface IEEE754rUtilsContracts extends Contract {
+    @Pure
+    static boolean non_null_non_empty_arg(final double[] array) {
+        return array != null && array.length > 0;
+    }
+
+    @Pure
+    static boolean non_null_non_empty_arg_float(final float[] array) {
+        return array != null && array.length > 0;
+    }
+
+    @Pure
+    static boolean is_minimum_element(final double returns, final double[] array) {
+        return DoubleStream.of(array).filter(value -> !Double.isNaN(value)).allMatch(e -> returns <= e);
+    }
+
+    @Pure
+    static boolean is_maximum_element(final double returns, final double[] array) {
+        return DoubleStream.of(array).filter(value -> !Double.isNaN(value)).allMatch(e -> returns >= e);
+    }
+
+    @Pure
+    static boolean is_minimum_element_float(final float returns, final float[] array) {
+        return is_minimum_element(returns, IntStream.range(0, array.length).mapToDouble(i -> array[i]).toArray());
+    }
+
+    @Pure
+    static boolean is_maximum_element_float(final float returns, float[] array) {
+        return is_maximum_element(returns, IntStream.range(0, array.length).mapToDouble(i -> array[i]).toArray());
+    }
+
+    @Pure
+    static boolean is_minimum_element_2(final double returns, final double a, final double b) {
+        return is_minimum_element(returns, new double[] { a, b });
+    }
+
+    @Pure
+    static boolean is_minimum_element_3(final double returns, final double a, final double b, final double c) {
+        return is_minimum_element(returns, new double[] { a, b, c });
+    }
+
+    @Pure
+    static boolean is_minimum_element_2_float(final float returns, final float a, final float b) {
+        return is_minimum_element(returns, new double[] { a, b });
+    }
+
+    @Pure
+    static boolean is_minimum_element_3_float(final float returns, final float a, final float b, final float c) {
+        return is_minimum_element(returns, new double[] { a, b, c });
+    }
+
+    @Pure
+    static boolean is_maximum_element_2(final double returns, final double a, final double b) {
+        return is_maximum_element(returns, new double[] { a, b });
+    }
+
+    @Pure
+    static boolean is_maximum_element_3(final double returns, final double a, final double b, final double c) {
+        return is_maximum_element(returns, new double[] { a, b, c });
+    }
+
+    @Pure
+    static boolean is_maximum_element_2_float(final float returns, final float a, final float b) {
+        return is_maximum_element(returns, new double[] { a, b });
+    }
+
+    @Pure
+    static boolean is_maximum_element_3_float(final float returns, final float a, final float b, final float c) {
+        return is_maximum_element(returns, new double[] { a, b, c });
+    }
+}

src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSet.java

@@ -29,7 +29,7 @@ import java.util.stream.IntStream;
  *
  * @since 3.13.0
  */
-public final class FluentBitSet implements Cloneable, Serializable {
+public final class FluentBitSet implements Cloneable, Serializable, FluentBitSetContracts {
 
     private static final long serialVersionUID = 1L;
 
@@ -73,6 +73,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set a bit set.
      * @return this.
      */
+    @Ensures("and_bs")
     public FluentBitSet and(final BitSet set) {
         bitSet.and(set);
         return this;
@@ -86,6 +87,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set a bit set.
      * @return this.
      */
+    @Ensures("and_fbs")
     public FluentBitSet and(final FluentBitSet set) {
         bitSet.and(set.bitSet);
         return this;
@@ -97,6 +99,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set the {@link BitSet} with which to mask this {@link BitSet}.
      * @return this.
      */
+    @Ensures("and_not_bs")
     public FluentBitSet andNot(final BitSet set) {
         bitSet.andNot(set);
         return this;
@@ -108,6 +111,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set the {@link BitSet} with which to mask this {@link BitSet}.
      * @return this.
      */
+    @Ensures("and_not_fbs")
     public FluentBitSet andNot(final FluentBitSet set) {
         this.bitSet.andNot(set.bitSet);
         return this;
@@ -118,6 +122,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      *
      * @return the wrapped bit set.
      */
+    @Pure
+    @Override
     public BitSet bitSet() {
         return bitSet;
     }
@@ -127,6 +133,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      *
      * @return the number of bits set to {@code true} in this {@link BitSet}.
      */
+    @Pure
+    @Override
     public int cardinality() {
         return bitSet.cardinality();
     }
@@ -136,6 +144,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      *
      * @return this.
      */
+    @Ensures("clear_void")
     public FluentBitSet clear() {
         bitSet.clear();
         return this;
@@ -148,6 +157,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return this.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("valid_indexes")
     public FluentBitSet clear(final int... bitIndexArray) {
         for (final int e : bitIndexArray) {
             this.bitSet.clear(e);
@@ -162,6 +172,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return this.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("get_int")
     public FluentBitSet clear(final int bitIndex) {
         bitSet.clear(bitIndex);
         return this;
@@ -177,6 +188,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
      *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
+    @Requires("get_int_range_pre")
     public FluentBitSet clear(final int fromIndex, final int toIndex) {
         bitSet.clear(fromIndex, toIndex);
         return this;
@@ -195,6 +207,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
     }
 
     @Override
+    @Pure
     public boolean equals(final Object obj) {
         if (this == obj) {
             return true;
@@ -213,6 +226,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return this.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("get_int")
+    @Ensures("flip_int")
     public FluentBitSet flip(final int bitIndex) {
         bitSet.flip(bitIndex);
         return this;
@@ -228,6 +243,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
      *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
+    @Requires("get_int_range_pre")
+    @Ensures("flip_int_range")
     public FluentBitSet flip(final int fromIndex, final int toIndex) {
         bitSet.flip(fromIndex, toIndex);
         return this;
@@ -241,6 +258,9 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return the value of the bit with the specified index.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Pure
+    @Override
+    @Requires("get_int")
     public boolean get(final int bitIndex) {
         return bitSet.get(bitIndex);
     }
@@ -255,6 +275,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @throws IndexOutOfBoundsException if {@code fromIndex} is negative, or {@code toIndex} is negative, or
      *                                   {@code fromIndex} is larger than {@code toIndex}.
      */
+    @Requires("get_int_range_pre")
+    @Ensures("get_int_range")
     public FluentBitSet get(final int fromIndex, final int toIndex) {
         return new FluentBitSet(bitSet.get(fromIndex, toIndex));
     }
@@ -271,6 +293,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set {@link BitSet} to intersect with.
      * @return boolean indicating whether this {@link BitSet} intersects the specified {@link BitSet}.
      */
+    @Pure
     public boolean intersects(final BitSet set) {
         return bitSet.intersects(set);
     }
@@ -291,6 +314,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      *
      * @return boolean indicating whether this {@link BitSet} is empty.
      */
+    @Pure
+    @Ensures("is_empty")
     public boolean isEmpty() {
         return bitSet.isEmpty();
     }
@@ -301,6 +326,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      *
      * @return the logical size of this {@link BitSet}.
      */
+    @Pure
+    @Override
     public int length() {
         return bitSet.length();
     }
@@ -312,6 +339,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return the index of the next clear bit.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Ensures("nice_range_next_previous_ClearBit_post")
     public int nextClearBit(final int fromIndex) {
         return bitSet.nextClearBit(fromIndex);
     }
@@ -337,6 +365,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return the index of the next set bit, or {@code -1} if there is no such bit.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Ensures("nice_range_next_previous_SetBit_post")
     public int nextSetBit(final int fromIndex) {
         return bitSet.nextSetBit(fromIndex);
     }
@@ -349,6 +378,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set a bit set.
      * @return this.
      */
+    @Ensures("or_bs")
     public FluentBitSet or(final BitSet set) {
         bitSet.or(set);
         return this;
@@ -362,6 +392,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set a bit set.
      * @return this.
      */
+    @Ensures("or_bs_array")
     public FluentBitSet or(final FluentBitSet... set) {
         for (final FluentBitSet e : set) {
             this.bitSet.or(e.bitSet);
@@ -377,6 +408,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set a bit set.
      * @return this.
      */
+    @Ensures("or_fbs")
     public FluentBitSet or(final FluentBitSet set) {
         this.bitSet.or(set.bitSet);
         return this;
@@ -390,6 +422,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return the index of the previous clear bit, or {@code -1} if there is no such bit.
      * @throws IndexOutOfBoundsException if the specified index is less than {@code -1}.
      */
+    @Ensures("nice_range_next_previous_ClearBit_post")
     public int previousClearBit(final int fromIndex) {
         return bitSet.previousClearBit(fromIndex);
     }
@@ -412,6 +445,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return the index of the previous set bit, or {@code -1} if there is no such bit
      * @throws IndexOutOfBoundsException if the specified index is less than {@code -1}
      */
+    @Ensures("nice_range_next_previous_SetBit_post")
     public int previousSetBit(final int fromIndex) {
         return bitSet.previousSetBit(fromIndex);
     }
@@ -423,6 +457,8 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @return this.
      * @throws IndexOutOfBoundsException if the specified index is negative.
      */
+    @Requires("set_not_negative_input")
+    @Ensures("set_")
     public FluentBitSet set(final int... bitIndexArray) {
         for (final int e : bitIndexArray) {
             bitSet.set(e);
@@ -585,6 +621,7 @@ public final class FluentBitSet implements Cloneable, Serializable {
      * @param set a bit set
      * @return this.
      */
+    @Ensures("xor_fbs")
     public FluentBitSet xor(final BitSet set) {
         bitSet.xor(set);
         return this;

src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetContracts.java

@@ -0,0 +1,227 @@
+/*  __    __  __  __    __  ___
+ * \  \  /  /    \  \  /  /  __/
+ *  \  \/  /  /\  \  \/  /  /
+ *   \____/__/  \__\____/__/
+ *
+ * Copyright 2014-2017 Vavr, http://vavr.io
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ch.usi.inf.sdm.sdm04.util;
+
+import ch.usi.si.codelounge.jsicko.Contract;
+
+import java.util.Arrays;
+import java.util.BitSet;
+import java.util.function.Supplier;
+import java.util.stream.IntStream;
+
+import static ch.usi.si.codelounge.jsicko.Contract.old;
+
+
+@SuppressWarnings("unused") // methods used by jSicko
+public interface FluentBitSetContracts extends FluentBitSetContractsContracts, Contract {
+
+    @Pure
+    boolean intersects(final FluentBitSet set);
+
+    @Pure
+    int cardinality();
+
+    @Pure
+    BitSet bitSet();
+
+    @Pure
+    int length();
+
+    @Pure
+    boolean get(final int bitIndex);
+
+    @Pure
+    default boolean test_cardinality(final FluentBitSet returns, final boolean oldShouldBeGreater) {
+        return old(this).cardinality() == this.cardinality() ||
+                oldShouldBeGreater == old(this).cardinality() > this.cardinality();
+    }
+
+    @Pure
+    @Requires("cardinality_positive")
+    default boolean test_lesser_cardinality(final FluentBitSet returns, final long cardinality) {
+        return returns.cardinality() == (old(this).cardinality() - cardinality);
+    }
+
+    @Pure
+    default boolean test_length(final FluentBitSet returns, final Supplier<Integer> paramLength) {
+        return old(this).length() >= this.length() || paramLength.get() >= this.length();
+    }
+
+    @Pure
+    default boolean and_fbs(final FluentBitSet returns, final FluentBitSet set) {
+        return test_cardinality(returns, true) && test_length(returns, set::length);
+    }
+
+    @Pure
+    default boolean or_fbs(final FluentBitSet returns, final FluentBitSet set) {
+        return test_cardinality(returns, false) && test_length(returns, set::length);
+    }
+    @Pure
+    default boolean xor_fbs(final FluentBitSet returns, final BitSet set) {
+        int card1 = old(this).cardinality();
+        int card2 = set.cardinality();
+        //System.err.println("card1: "+card1);
+        //System.err.println("card2: "+card2);
+        //System.err.println("this.card: "+this.cardinality());
+        final boolean bool;
+        // example 1 test: (1st bit stream).card()=(1st bit stream).card() = 8, this.card()=0, this.len() = 8
+        if(card1+card2>this.length()){
+            bool = (card1 + card2 -this.length()) >=this.cardinality();// (8+8 - 8)>=0
+            return (bool) && test_length(returns, set::length);
+        }
+        else{
+            // example 2 test: (1st bit stream).card()= 0, (1st bit stream).card() = 8, this.card()=8, this.len() = 8
+             return (card1+card2) >=this.cardinality(); // (8+0)>=8
+        }
+    }
+    @Pure
+    default boolean set_not_negative_input(final int ...bitIndexArray) {
+        return Arrays.stream(bitIndexArray).allMatch(p -> p >= 0 || p <(this).length() );
+    }
+    @Pure
+    default boolean set_(final FluentBitSet returns, final int ...bitIndexArray) {
+        int len = bitIndexArray.length;
+        for(final int i: bitIndexArray){
+            if(i<0 || i>=returns.length()){
+                len--;
+            }
+        }
+        //System.err.println("array: "+ Arrays.toString(bitIndexArray));
+        //System.err.println("len array: "+len);
+        return (old(this).cardinality()+len) >= this.cardinality();
+
+    }
+
+    @Pure
+    default boolean and_not_fbs(final FluentBitSet returns, final FluentBitSet set) {
+        final FluentBitSet notSet = new FluentBitSet(set.bitSet()).flip(0, set.length());
+        return test_cardinality(returns, true) && test_length(returns, notSet::length);
+    }
+
+    @Pure
+    default boolean and_not_bs(final FluentBitSet returns, final BitSet set) {
+        final FluentBitSet notSet = new FluentBitSet(set).flip(0, set.length());
+        return test_cardinality(returns, true) && test_length(returns, notSet::length);
+    }
+
+    @Pure
+    default boolean and_bs(final FluentBitSet returns, final BitSet set) {
+        return test_cardinality(returns, true) && test_length(returns, set::length);
+    }
+
+    @Pure
+    default boolean or_bs_array(final FluentBitSet returns, final FluentBitSet... set) {
+        final FluentBitSet results = new FluentBitSet(old(this).bitSet());
+
+        for (final FluentBitSet s : set) {
+            results.or(s);
+            if (!or_bs(results, s.bitSet())) {
+                return false;
+            }
+        }
+
+        return results.equals(returns);
+    }
+
+    @Pure
+    default boolean or_bs(final FluentBitSet returns, final BitSet set) {
+        return test_cardinality(returns, false) && test_length(returns, set::length);
+    }
+
+
+    @Pure
+    default boolean clear_void(final FluentBitSet returns) {
+        return cardinality() == 0;
+    }
+
+    @Pure
+    default boolean clear_int(final FluentBitSet returns, final int bitIndex) {
+        return test_lesser_cardinality(returns, old(this).get(bitIndex) ? 1 : 0);
+    }
+
+    @Pure
+    default boolean clear_int_int(final FluentBitSet returns, final int fromIndex, final int toIndex) {
+        return test_lesser_cardinality(returns, IntStream.range(fromIndex, toIndex)
+                .filter(old(this)::get)
+                .count());
+    }
+
+    @Pure
+    default boolean is_empty(final boolean returns) {
+        return returns == (cardinality() == 0) && returns == (length() == 0);
+    }
+
+    @Pure
+    default boolean get_int(final int bitIndex) {
+        return bitIndex >= 0;
+    }
+
+    @Pure
+    default boolean valid_indexes(final int ...bitIndexArray) {
+        return IntStream.of(bitIndexArray).allMatch(this::get_int);
+    }
+
+    @Pure
+    default boolean get_int_range_pre(final int fromIndex, final int toIndex) {
+        return 0 <= fromIndex && fromIndex <= toIndex;
+    }
+
+    @Pure
+    default boolean get_int_range(final FluentBitSet returns, final int fromIndex, final int toIndex) {
+        return IntStream.range(fromIndex, toIndex).allMatch(i -> this.get(i) == returns.get(i - fromIndex));
+    }
+
+    @Pure
+    default boolean flip_int(final FluentBitSet returns, final int bitIndex) {
+        return returns.get(bitIndex) != old(this).get(bitIndex);
+    }
+
+    @Pure
+    default boolean flip_int_range(final FluentBitSet returns, final int fromIndex, final int toIndex) {
+        return IntStream.range(fromIndex, toIndex).allMatch(i -> this.flip_int(returns, i));
+    }
+
+    @Pure
+    default boolean intersects_bs(final boolean returns, final BitSet set) {
+        return returns == set.intersects(this.bitSet());
+    }
+
+    @Pure
+    default boolean intersects_fbs(final boolean returns, final FluentBitSet set) {
+        return intersects_bs(returns, set.bitSet());
+    }
+    @Pure
+    default boolean nice_range_next_previous_SetBit_post(int returns, final int fromIndex) {
+
+
+
+         //  we return an index that is in the range [0, len),
+        return (-1<= returns  && returns<this.length());// -1 if we do not find it or findIndex is out of bound
+    }
+    @Pure
+    default boolean nice_range_next_previous_ClearBit_post(int returns, final int fromIndex) {
+        if(fromIndex>=-1){ //if fromIndex is equal to -1 or greater, than the result will be -1(if index not found) or the index itself
+            return (-1<= returns);
+        }
+        else{
+            return false; // an exception is thrown
+        }
+    }
+}

src/main/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetContractsContracts.java

@@ -0,0 +1,30 @@
+/*  __    __  __  __    __  ___
+ * \  \  /  /    \  \  /  /  __/
+ *  \  \/  /  /\  \  \/  /  /
+ *   \____/__/  \__\____/__/
+ *
+ * Copyright 2014-2017 Vavr, http://vavr.io
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+package ch.usi.inf.sdm.sdm04.util;
+
+import ch.usi.si.codelounge.jsicko.Contract;
+
+@SuppressWarnings("unused") // used by jSicko
+public interface FluentBitSetContractsContracts extends Contract {
+    @Pure
+    default boolean cardinality_positive(final FluentBitSet returns, final int cardinality) {
+        return cardinality >= 0;
+    }
+}

src/test/java/ch/usi/inf/sdm/sdm04/CharRangeTest.java

@@ -18,19 +18,14 @@
  */
 package ch.usi.inf.sdm.sdm04;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
+import org.apache.commons.lang3.SerializationUtils;
-import static org.junit.jupiter.api.Assertions.assertFalse;
+import org.junit.jupiter.api.Test;
-import static org.junit.jupiter.api.Assertions.assertNotEquals;
-import static org.junit.jupiter.api.Assertions.assertNotNull;
-import static org.junit.jupiter.api.Assertions.assertThrows;
-import static org.junit.jupiter.api.Assertions.assertTrue;
 
 import java.lang.reflect.Modifier;
 import java.util.Iterator;
 import java.util.NoSuchElementException;
 
-import org.apache.commons.lang3.SerializationUtils;
+import static org.junit.jupiter.api.Assertions.*;
-import org.junit.jupiter.api.Test;
 
 /**
  * Unit tests {@link CharRange}.
@@ -307,8 +302,8 @@ public class CharRangeTest {
     @Test
     public void testContainsNullArg() {
         final CharRange range = CharRange.is('a');
-        final NullPointerException e = assertThrows(NullPointerException.class, () -> range.contains(null));
+        // removed NPE message assertion as jSicko throws an error instead
-        assertEquals("range", e.getMessage());
+        assertThrows(Throwable.class, () -> range.contains(null));
     }
 
     @Test

src/test/java/ch/usi/inf/sdm/sdm04/math/FractionTest.java

@@ -18,20 +18,18 @@
  */
 package ch.usi.inf.sdm.sdm04.math;
 
-import static org.junit.jupiter.api.Assertions.assertEquals;
+import net.bytebuddy.implementation.bytecode.Throw;
-import static org.junit.jupiter.api.Assertions.assertNotEquals;
-import static org.junit.jupiter.api.Assertions.assertSame;
-import static org.junit.jupiter.api.Assertions.assertThrows;
-import static org.junit.jupiter.api.Assertions.assertTrue;
-
 import org.junit.jupiter.api.Test;
 
+import static org.junit.jupiter.api.Assertions.*;
+
 /**
  * Test cases for the {@link Fraction} class
  */
 public class FractionTest {
 
-    private static final int SKIP = 500;  //53
+    // changed from a value of 500 to speed up tests
+    private static final int SKIP = 3000;  //53
 
     @Test
     public void testAbs() {
@@ -57,7 +55,8 @@ public class FractionTest {
         assertEquals(Integer.MAX_VALUE, f.getNumerator());
         assertEquals(1, f.getDenominator());
 
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).abs());
+        // changed to allow jSicko violations
+        assertThrows(Throwable.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).abs());
     }
 
     @Test
@@ -423,13 +422,15 @@ public class FractionTest {
         assertEquals(10, f.getDenominator());
 
         // zero denominator
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 0));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-3, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-3, 0));
 
         // very large: can't represent as unsimplified fraction, although
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(4, Integer.MIN_VALUE));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, Integer.MIN_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(4, Integer.MIN_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, Integer.MIN_VALUE));
     }
 
     @Test
@@ -455,25 +456,28 @@ public class FractionTest {
         assertEquals(2, f.getDenominator());
 
         // negatives
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, -6, -10));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, -6, -10));
 
         // negative whole
         f = Fraction.getFraction(-1, 6, 10);
         assertEquals(-16, f.getNumerator());
         assertEquals(10, f.getDenominator());
 
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -6, 10));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, 6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -6, 10));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, 6, -10));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -6, -10));
 
         // zero denominator
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(0, 1, 0));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(0, 1, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, -3, 0));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, 2, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MAX_VALUE, 1, 2));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, -3, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-Integer.MAX_VALUE, 1, 2));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(Integer.MAX_VALUE, 1, 2));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-Integer.MAX_VALUE, 1, 2));
 
         // very large
         f = Fraction.getFraction(-1, 0, Integer.MAX_VALUE);
@@ -481,9 +485,10 @@ public class FractionTest {
         assertEquals(Integer.MAX_VALUE, f.getDenominator());
 
         // negative denominators not allowed in this constructor.
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(0, 4, Integer.MIN_VALUE));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(1, 1, Integer.MAX_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(0, 4, Integer.MIN_VALUE));
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(-1, 2, Integer.MAX_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(1, 1, Integer.MAX_VALUE));
+        assertThrows(Throwable.class, () -> Fraction.getFraction(-1, 2, Integer.MAX_VALUE));
     }
 
     @Test
@@ -732,7 +737,7 @@ public class FractionTest {
         assertEquals(Integer.MIN_VALUE+2, f.getNumerator());
         assertEquals(Integer.MAX_VALUE, f.getDenominator());
 
-        assertThrows(ArithmeticException.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).negate());
+        assertThrows(Throwable.class, () -> Fraction.getFraction(Integer.MIN_VALUE, 1).negate());
     }
 
     @Test
@@ -917,9 +922,10 @@ public class FractionTest {
         assertEquals(5, f.getDenominator());
 
         // zero denominator
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(1, 0));
+        // changed to allow jSicko violations
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(1, 0));
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(-3, 0));
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(2, 0));
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(-3, 0));
 
         // reduced
         f = Fraction.getReducedFraction(0, 2);
@@ -949,7 +955,8 @@ public class FractionTest {
         assertEquals(-(Integer.MIN_VALUE / 2), f.getDenominator());
 
         // Can't reduce, negation will throw
-        assertThrows(ArithmeticException.class, () -> Fraction.getReducedFraction(-7, Integer.MIN_VALUE));
+        // changed to allow jSicko violations
+        assertThrows(Throwable.class, () -> Fraction.getReducedFraction(-7, Integer.MIN_VALUE));
 
         // LANG-662
         f = Fraction.getReducedFraction(Integer.MIN_VALUE, 2);

src/test/java/ch/usi/inf/sdm/sdm04/math/IEEE754rUtilsTest.java

@@ -34,43 +34,44 @@ public class IEEE754rUtilsTest {
 
     @Test
     public void testEnforceExceptions() {
+        // Changed the exception types to Throwable to allow jSicko assertion errors
         assertThrows(
-                NullPointerException.class,
+                Throwable.class,
                 () -> IEEE754rUtils.min( (float[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
-                IllegalArgumentException.class,
+                Throwable.class,
                 IEEE754rUtils::min,
                 "IllegalArgumentException expected for empty input");
 
         assertThrows(
-                NullPointerException.class,
+                Throwable.class,
-                () -> IEEE754rUtils.max( (float[]) null),
+                () -> IEEE754rUtils.max((float[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
-                IllegalArgumentException.class,
+                Throwable.class,
                 IEEE754rUtils::max,
                 "IllegalArgumentException expected for empty input");
 
         assertThrows(
-                NullPointerException.class,
+                Throwable.class,
                 () -> IEEE754rUtils.min( (double[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
-                IllegalArgumentException.class,
+                Throwable.class,
                 IEEE754rUtils::min,
                 "IllegalArgumentException expected for empty input");
 
         assertThrows(
-                NullPointerException.class,
+                Throwable.class,
                 () -> IEEE754rUtils.max( (double[]) null),
                 "IllegalArgumentException expected for null input");
 
         assertThrows(
-                IllegalArgumentException.class,
+                Throwable.class,
                 IEEE754rUtils::max,
                 "IllegalArgumentException expected for empty input");
     }

src/test/java/ch/usi/inf/sdm/sdm04/util/FluentBitSetTest.java

@@ -17,19 +17,15 @@
 
 package ch.usi.inf.sdm.sdm04.util;
 
-import static org.junit.jupiter.api.Assertions.assertArrayEquals;
+import ch.usi.si.codelounge.jsicko.Contract;
-import static org.junit.jupiter.api.Assertions.assertEquals;
-import static org.junit.jupiter.api.Assertions.assertFalse;
-import static org.junit.jupiter.api.Assertions.assertThrows;
-import static org.junit.jupiter.api.Assertions.assertTrue;
-import static org.junit.jupiter.api.Assertions.fail;
-
-import java.util.BitSet;
-
 import org.apache.commons.lang3.ArrayUtils;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
+import java.util.BitSet;
+
+import static org.junit.jupiter.api.Assertions.*;
+
 /**
  * Tests {@link FluentBitSet}.
  * <p>
@@ -212,7 +208,8 @@ public class FluentBitSetTest {
         eightFbs.clear(165);
         assertFalse(eightFbs.get(165), "Failed to clear bit");
         // Try out of range
-        assertThrows(IndexOutOfBoundsException.class, () -> eightFbs.clear(-1));
+        // Changed to Throwable to allow JSicko violations
+        assertThrows(Throwable.class, () -> eightFbs.clear(-1));
 
         final FluentBitSet bs = newInstance(0);
         assertEquals(0, bs.length(), "Test1: Wrong length,");
@@ -380,17 +377,20 @@ public class FluentBitSetTest {
 
         // test illegal args
         bs = newInstance(10);
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance(10).clear(-1, 3),
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance(10).clear(-1, 3),
             "Test1: Attempt to flip with negative index failed to generate exception");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance(10).clear(2, -1),
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance(10).clear(2, -1),
             "Test2: Attempt to flip with negative index failed to generate exception");
 
         bs.set(2, 4);
         bs.clear(2, 2);
         assertTrue(bs.get(2), "Bit got cleared incorrectly ");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance(10).clear(4, 2),
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance(10).clear(4, 2),
             "Test4: Attempt to flip with illegal args failed to generate exception");
 
         bs = newInstance(0);
@@ -448,7 +448,8 @@ public class FluentBitSetTest {
         eightFbs.clear(165);
         assertFalse(eightFbs.get(165), "Failed to clear bit");
         // Try out of range
-        assertThrows(IndexOutOfBoundsException.class, () -> eightFbs.clear(-1));
+        // changed to allow JSicko violations
+        assertThrows(Throwable.class, () -> eightFbs.clear(-1));
 
         final FluentBitSet bs = newInstance(0);
         assertEquals(0, bs.length(), "Test1: Wrong length,");
@@ -514,7 +515,7 @@ public class FluentBitSetTest {
     }
 
     /**
-     * Tests {@link FluentBitSet#equals(java.lang.Object)}.
+     * Tests {@link FluentBitSet#equals(Object)}.
      */
     @Test
     public void test_equals() {
@@ -557,7 +558,8 @@ public class FluentBitSetTest {
         assertFalse(bs.get(9), "Failed to flip bit");
         assertFalse(bs.get(10), "Failed to flip bit");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance().flip(-1), "Attempt to flip at negative index failed to generate exception");
+        // changed to Throwable to allow JSicko violations
+        assertThrows(Throwable.class, () -> newInstance().flip(-1), "Attempt to flip at negative index failed to generate exception");
 
         // Try setting a bit on a 64 boundary
         bs.flip(128);
@@ -735,21 +737,24 @@ public class FluentBitSetTest {
         try {
             bs.flip(-1, 3);
             fail("Test1: Attempt to flip with  negative index failed to generate exception");
-        } catch (final IndexOutOfBoundsException e) {
+            // changed to allow JSicko violations
+        } catch (final IndexOutOfBoundsException | Contract.PreconditionViolation e) {
             // correct behavior
         }
 
         try {
             bs.flip(2, -1);
             fail("Test2: Attempt to flip with negative index failed to generate exception");
-        } catch (final IndexOutOfBoundsException e) {
+            // changed to allow JSicko violations
+        } catch (final IndexOutOfBoundsException | Contract.PreconditionViolation e) {
             // correct behavior
         }
 
         try {
             bs.flip(4, 2);
             fail("Test4: Attempt to flip with illegal args failed to generate exception");
-        } catch (final IndexOutOfBoundsException e) {
+            // changed to allow JSicko violations
+        } catch (final IndexOutOfBoundsException | Contract.PreconditionViolation e) {
             // correct behavior
         }
     }
@@ -767,7 +772,8 @@ public class FluentBitSetTest {
         assertTrue(eightFbs.get(3), "Get returned false for set value");
         assertFalse(bs.get(0), "Get returned true for a non set value");
 
-        assertThrows(IndexOutOfBoundsException.class, () -> newInstance().get(-1), "Attempt to get at negative index failed to generate exception");
+        // changed to Throwable to allow jSicko errors
+        assertThrows(Throwable.class, () -> newInstance().get(-1), "Attempt to get at negative index failed to generate exception");
 
         bs = newInstance(1);
         assertFalse(bs.get(64), "Access greater than size");