Your First Proofs

Lets write a proof! below is our function we want to prove:

fun foo(x: Int, y: Int): Int {
    return if (y % 2 == 0) {
        x/y
    } else {
        y*2
    }
}

Our first step should be to write a proof that checks nothing:

@BmcProof
fun `my foo is sound`() {
    val x = anyInt()
    val y = anyInt()
    foo(x, y)
}

As a test, not having any asserts would be strange and a code smell, but here it makes perfect sense. Any exception, error, or assertion failure will come back as refuation of this proof.

So if you ran this proof, you would get:

JBMC refuted proofs.FooProof.my foo is sound
  ✗ assertion
    counterexample: x = 0, y = 0

So it breaks at y = 0 (division by 0). Lets fix it!

fun foo(x: Int, y: Int): Int {
    if (y == 0) return 0
    return if (y % 2 == 0) {
        x/y
    } else {
        y*2
    }
}

Now lets write another proof, lets prove that when y is odd, foo is always an even number:

@BmcProof
fun `my foo is never odd when y is odd`() {
    val x = anyInt()
    val y = anyInt()
    assume(y % 2 == 1)
    check((foo(x, y) % 2) == 0)
}

If we run it, we should get a verified result!

Lets also write the opposite of this check to be sure:

@BmcProof(expect = Verdict.REFUTED)
fun `my foo is never odd when y is odd - refuted`() {
    val x = anyInt()
    val y = anyInt()
    assume(y % 2 == 1)
    check((foo(x, y) % 2) == 1)
}