-
Notifications
You must be signed in to change notification settings - Fork 27
Hackeython Working Group: Library Functions
Shepard: Wolfram
One of the most frequently asked questions on the mailing list is, why KeY does not find Java library methods such as "System.out.println()" or "Arrays.toString()". When writing code for testing a small implementation that should be verified with KeY, it is also very annoying that you always have to remove these method calls, imports etc. from your code before loading the file with KeY.
In principle, there is the solution to provide a custom Java library with the \bootclasspath option in .key files (see also the https://keyproject.github.io/key-docs/user/FAQ/ and https://keyproject.github.io/key-docs/user/Classpath/). This way, it is possible to provide the missing classes and methods. However, this is not trivial at all, since you have to be very careful to provide all the correct dependencies (there are for example some classes/fields/methods that KeY needs) and also have to remove features of Java that KeY does not support (e.g., Generics). Furthermore, since KeY does not bring them by default, you have to do it again and again.
The idea of this working group is to extend JavaRedux (the fragment of the Java Class Library shipped with KeY) in such a way that the most commonly needed classes are present. In addition to the Java method signatures, this may also include contracts. However, it is an open task to decide how exactly these contracts should look like: For example, for "System.out.println()" full functional specification will not be possible, but we need to come up with an abstraction (which might even be "unsound", e.g. state assignable \nothing in this case).
- Which classes/fields/methods do we want to support?
- What to do with imports (from the Java library)? Shall we dynamically generate contracts (as long as javac can parse the file, i.e., the syntax element stems from JCL)?
- Should there be several modes? E.g., sound default contracts (
assignable \everything), "unsound" contracts¹ that allow us to "easily skip" debug method calls during verification (assignable \(strictly_)nothing). - What shall be error/warning messages?
¹) Maybe, they are not really unsound, but introduce additional assumptions, such as that the state of the console is not part of the state of the program.