OpenJML/ Джесси для 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;

Есть ли способ "связать" OpenJML с Android SDK? Или, может быть, есть какие-то другие инструменты, которые совместимы с Android? Может, Джесси / Кракатау это сделать?

Answer 1

Через некоторое время я прихожу к выводу, что нет никакой возможности официально проверить Android SDK по двум причинам:

• OpenJML не поддерживает параллелизм, в то время как Android сильно зависит от асинхронных вызовов.
• Судя по репозиторию OpenJML ( https://github.com/OpenJML/OpenJML), кажется, что OpenJML в основном сделан с OpenJDK, в то время как Android использует собственную реализацию Java вместе с Dalvik VM. По этой причине поддержка Android может быть еще сложнее для OpenJML

Но есть решение! Я лично создал абстракцию над Android. Просто создайте несколько интерфейсов, которые смоделированы с помощью JML, подтвердите основную логику на их основе, а затем реализуйте все эти интерфейсы с помощью кода Android (надеясь, что реализация верна).