1

I am trying to statically check Java my code. The only problem is that it uses android sdk and OpenJML cannot identify android classes. For instance this is part of logs I get:

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;

Is there a way to "link" OpenJML with android SDK? Or maybe is there some other tools that is compatible with android? Maybe Jessie/Krakatoa can do it?

alagris
  • 1,838
  • 16
  • 31

1 Answers1

1

After some time I come to the conclusion that there is no way to formally verify Android SDK fro 2 reasons:

  • OpenJML doesn't support concurrency, while Android heavily relies on async calls.
  • Judging by OpenJML repo (https://github.com/OpenJML/OpenJML), it seems that OpenJML is primarily made with OpenJDK, while Android uses their own implementation of Java along with Dalvik VM. For this reason supporting Android might be even more difficult for OpenJML

But there is a solution! What I personally made was to create abstraction over Android. Just make a bunch of interfaces that are modelled with JML, prove main logic based on them, and then implement all those interfaces with Android code (hoping that the implementation is correct).

alagris
  • 1,838
  • 16
  • 31