bmc4j - v0.6.0 bmc4j is a formal verification too...

# feed

[Courtney May]

bmc4j - v0.6.0

bmc4j is a formal verification tool for kotlin/java (using bounded model checking) that lets you write/run code proofs as JUnit tests.

Example:

@JvmInline
value class Score(val value: Int) { init { require(value in 1..101) } } // a bug - should be 1..100

fun gradeBand(score: Score): String {
    val labels = arrayOf("F", "E", "D", "C-", "C", "C+", "B", "B+", "A-", "A")
    return labels[(score.value - 1) / 10]
}

class GradeBandProofs {
    @BmcProof
    fun `gradeBand never throws for any valid Score`() {
        val score = assumeValid { Score(anyInt()) } // require(...) gets folded into the domain
        gradeBand(score)                            // we want to prove that gradeBand never throws for any valid score
        // refuted! ArrayIndexOutOfBoundsException, counterexample: score = 101
    }
}

We are pre-1.0.0 so actively looking for people to try it out and provide feedback/report issues!

https://bmc4j.github.io/docs/
https://github.com/bmc4j/bmc4j

[Bernd Prünster]

Sounds awesome! Does it work on the JVM targets of KMP projects or does it have to be the kotlin jvm-only gradle plugin?

[Courtney May]

Yep! it works on JVM targets of KMP