Automatic Soundness and Completeness Warnings in ESC/Java3
Note: Some initial work on this project was done as a 2005-2006 Final Year Project by Barry Denby (report). The prototype is integrated into ESC/Java2.
- Supervisor Dr. Joseph Kiniry
- Subject Area Software Engineering with Applied Theoretical Computer Science
- Pre-requisites Strong knowledge of Java and reasonably strong mathematical background
- Co-requisites (things you must learn along the way) Programming language semantics, formal specification, extended static checking, logic
- Subject Coverage Semantics, Extended Static Checking
- Project Type Design and Implementation
- Hardware/Software Machine running anything but Windows
Description
ESC/Java2 is an extended static checker for Java: it automatically proves that a Java program fulfills (parts of) its specification, written in the Java Modeling Language.
Concessions must be made to make ESC/Java2 automatic and easy to use, some of which are formal and some of which are practical. In particular, ESC/Java2 is neither a sound nor a complete verification system. In other words, it generates false positives, false negatives, and it completely misses some errors. All of these problems are due to the fact that its built-in semantics of Java and JML are intentionally incomplete (they do not cover the full language) and that the modular reasoning framework used is intentionally unsound (by design and because of the current theorem prover used).
Therefore, when ESC/Java2 detects a problem, it signals a warning, not and error, because we just cannot be certain that what has been checked is actually true.
This situation is unsatisfactory, but an obvious solution exists to this dilemma. Because we understand ESC/Java2's logics and can characterise them precisely, and because we have a rich context when reasoning about a given method, we know when the user is trying to verify programs in "dangerous waters".
For example, if you use floating point arithmetic, all bets are off. If you try to reason about specification with certain kinds of invariants that have universally quantified subexpressions, Danger Will Robinson!
The purpose of this project is to characterise these "danger areas" and extend ESC/Java2's functionality to automatically warn the user when they are attempting to perform verifications about programs and/or specifications that are possibly confounded by the soundness and completeness problems of the tool.
Mandatory Goals
- Learn the ESC/Java2 object logics and their soundness and completeness issues and annotate the booklet "The Logics and Calculi of ESC/Java2" for clarity.
- Learn the ESC/Java2 calculi and their soundness and completeness issues and annotate the above booklet for clarity.
- Write a short survey on the soundness and completeness issues with modern object-oriented modular checking techniques.
- Itemise full list of soundness and completeness issues from the three above stages in a distilled document.
- Design and implement a contextually-aware soundness and completeness warning system for ESC/Java3.
Discretionary Goals
- Coauthor, submit, and publish a paper on this work.