maggicl/soft-an03
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

report done

Browse source
This commit is contained in:
Claudio Maggioni 2023-05-01 14:35:01 +02:00
parent 6f1444e751
commit 38ca002687
2 changed files with 47 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
report.pdf
View file

Binary file not shown.

56
report.tex
View file

@ -390,23 +390,61 @@ void translateWhole(final @MinLen(1) CharSequence input, final Writer writer) th
final String quoteless = input.subSequence(1, lastIndex).toString();
\end{minted}
This assertion is one good example of CheckerFramework's limitations in
verifying transitively true properties due to the lack of deductive verification
capabilities. All assertions added in the project are trivial in this way to
some degree.
\section{Conclusions}
As evidenced by the Apache Common Text test suite and the previous section of
this report, no changes in the implementation behaviour are introduced in the
this report, no changes in the implementation behaviour were introduced in the
code by the refactor. Only extended type annotations and assertions (that hold
when executing the test suite) are added to the code.
when executing the test suite) were added to the code.
{\color{red}
Did using the checker help you find any bugs or other questionable design and implementation choices?
No implementaton-derived bugs were discovered during refactoring, altough the
introduction of additional method preconditions via extended type annotations
was sometimes needed. Some questionable design choices were found in the
library, namely the \textit{CharSequenceTranslator} template method hierarchy
with \mintinline{java}{public} implementors and the inversion of abstration by
refused bequest in the \textit{SinglePassTranslator} partial implementation,
however I managed to introduce correct extended types without drastic
alterations (which may have broken clients of the library).
> no bugs found, couple of design choices
It was quite easy to introduce the CheckerFramework index checker to the Maven
build toolchain of the project. However, compiling the project after this was
significantly slower than before and lots of spurious warnings (i.e. false
positives) were produced by the tool due to its lack of deductive verification
capabilities. Some benefits were gained by using the tool, namely being able to
better refine the precondition of the methods in the library by documenting them
in an automatedly parsable fashion. However, the sheer number of trivially true
assertions introduced to silence some warnings is a significant downside to
consider when using the index checker.
How complex was it to apply the checker, and what benefits did you gain in return?
The CheckerFramework extended type checker has a cost and complexity of usage
greater than the Infer static analysis tool and lower than the Dafny deductive
verifier. However, with respect to my experience with all the tools in carrying
out the assignment, this is the tool that has shown to be the less useful.
> not so complex, lots of false positives
The less powerful Infer static analyzer, even with a great number of false
positives, was able to highlight some bugs in the project I have chosen for that
assignment (Apache Commons Lang). As all Apache Commons libraries are quite
mature and well-maintained it is expected that both tools find relatively few
things to flag in them. However, no noteworthy errors were found by
CheckerFramework in this project other than some small imprecisions in the
precondition specification of some methods.
Compare the checker’s trade-off between complexity of usage and analysis power to that of other software analysis techniques you’re familiar with (in particular, those used in previous assignments).
}
When compared to Dafny and deductive verifiers in general, clearly both Infer
and CheckerFramework pale in comparison in terms of capabilities. However, the
increased cost of adoption and of the tool's execution make it suitable only to
critical portions of project codebases.
Finally, I would like to mention the
\href{https://github.com/JetBrains/java-annotations}{Jetbrains Java Annotations}
as a much less powerful but effective extended type checking mechanism to handle
nullable an non-null values in plain Java. Even if its scope of analysis is
rather narrow and warnings an the type checking process is proprietary (as only
Jetbrains IDEs interpret the annotations) I have found it an effective
development aid in my university and work experience.
\end{document}