Mungo comparison
João Mota edited this page Jun 23, 2023
·
3 revisions
This table compares the checking capabilities between Mungo and our tool. Each line is justified by some tests, which include a README.md file with the results each tool outputs. On each test, the correct output is characterized by no errors being reported in Ok.java files and errors being reported in NotOk.java files.
| Features | Mungo Toolset | Java Typestate Checker | Tests |
|---|---|---|---|
| Basic checking | ✔️ | ✔️ | basic-checking |
| Decisions on enumeration values | ✔️ | ✔️ | basic-checking |
| Decisions on boolean values | ✔️ | boolean-decision | |
@Requires @Ensures
|
✔️ | state-refinement | |
| Nullness checking | 🟨 [1] | ✔️ | nullness-checking |
| Linearity checking | 🟨 [2, 3] | ✔️ | linearity-checking, linearity-checking-corner-cases |
| Force protocol completion | 🟨 [4] | ✔️ | protocol-completion, protocol-completion-corner-cases |
| Class analysis | ✔️ | class-analysis | |
| Protocol definitions for libraries | ✔️ | iterator-attempt1 | |
| Droppable objects | ✔️ | droppable-objects | |
| Generics | generics | ||
| Collections | auction | ||
| Improved flow analysis Recognition of decisions with equality checks |
✔️ [5] | iterator-attempt[2, 3, 4, 5, 6, 7] original-mungo-flow-issue-1 original-mungo-flow-issue-2 |
- Some errors are reported but they are a bit cryptic and
obj != nullrefinement does not exist. - Some errors are reported but they are a bit cryptic.
- Some corner cases are not handled, namely, if an object is moved to a lambda.
- Some corner cases are not handled, namely, if an object without protocol holds a reference to an object with protocol, the protocol completion of the second one if not ensured.
- We recognize, for example, that
while(true)is an infinite loop. This is useful for recognition of code that might have been automatically generated by a toolchain, like StMungo.