OpenJML/Jessie 对于 android

Question

我正在尝试静态检查 Java 我的代码。唯一的问题是它使用android sdk 并且OpenJML 无法识别android 类。例如，这是我得到的日志的一部分：

app/src/main/java/rup/ino/catornot/MainActivity.java:3: error: package android.graphics does not exist
import android.graphics.Bitmap;
                   ^
app/src/main/java/rup/ino/catornot/MainActivity.java:4: error: package android.graphics does not exist
import android.graphics.BitmapFactory;
                   ^
app/src/main/java/rup/ino/catornot/MainActivity.java:5: error: package android.graphics does not exist
import android.graphics.Canvas;
                   ^
app/src/main/java/rup/ino/catornot/MainActivity.java:6: error: package android.hardware does not exist
import android.hardware.Camera;

有没有办法 "link" OpenJML 与 android SDK？或者是否有其他一些与 android 兼容的工具？也许Jessie/Krakatoa可以做到？

Answer 1

一段时间后，我得出结论，无法正式验证 Android SDK，原因有两个：

OpenJML 不支持并发，而 Android 严重依赖异步调用。
根据 OpenJML 存储库 (https://github.com/OpenJML/OpenJML) 判断，OpenJML 似乎主要是用 OpenJDK 制作的，而 Android 使用他们自己的 Java 实现以及 Dalvik VM。因此，支持 Android 对 OpenJML

但是有一个解决办法！我个人所做的是在 Android 上创建抽象。做一堆用JML建模的接口，根据它们证明主要逻辑，然后用Android代码实现所有这些接口（希望实现正确）。

OpenJML/Jessie 对于 android

OpenJML/Jessie for android

android

formal-verification

openjml