diff --git a/report.pdf b/report.pdf index fa98978..7c74fe8 100644 Binary files a/report.pdf and b/report.pdf differ diff --git a/report.tex b/report.tex index 95f4238..826555c 100644 --- a/report.tex +++ b/report.tex @@ -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}