适用于 Android 的 OpenJML/Jessie答案

【问题标题】：OpenJML/Jessie for android适用于 Android 的 OpenJML/Jessie
【发布时间】：2019-05-18 02:04:11
【问题描述】：

我正在尝试静态检查 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;

有没有办法将 OpenJML 与 android SDK “链接”？或者也许还有其他一些与android兼容的工具？也许 Jessie/Krakatoa 可以做到？

【问题讨论】：

标签： android formal-verification openjml

【解决方案1】：

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

OpenJML 不支持并发，而 Android 严重依赖异步调用。
从 OpenJML repo (https://github.com/OpenJML/OpenJML) 来看，OpenJML 似乎主要是用 OpenJDK 制作的，而 Android 使用他们自己的 Java 实现以及 Dalvik VM。因此，对于 OpenJML 来说，支持 Android 可能会更加困难

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

【讨论】：