OpenJML/Jessie for android

Question

我正在尝试静态地检查Java我的代码。唯一的问题是它使用了android，而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“链接”？或者，还有其他与android兼容的工具吗？也许杰茜/克拉卡托能做到？

Answer 1

过了一段时间，我得出这样的结论:没有办法正式验证Android，原因有2：

• OpenJML不支持并发性，而Android则严重依赖异步调用。
• 从OpenJML回购(https://github.com/OpenJML/OpenJML)判断，OpenJML似乎主要是用OpenJDK制作的，而安卓则使用自己的Java实现和Dalvik。由于这个原因，对OpenJML来说支持Android可能更加困难。

但有个解决办法！我个人创造的是对Android的抽象。只需制作一堆用JML建模的接口，证明基于JML的主要逻辑，然后用Android代码实现所有这些接口(希望实现是正确的)。