OpenJML / Джесси для Android - PullRequest
Новая
       63

OpenJML / Джесси для Android

0 голосов
/ 17 декабря 2018

Я пытаюсь статически проверить 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?Может быть, Джесси / Кракатау это удастся сделать?

1 Ответ

0 голосов
/ 05 января 2019

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

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

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

...