Models

A model is a stand-in for a class or method that the engine analyzes in place of the real thing. The Key Concepts cover why: turning a whole class verbatim into a formula is often too big to solve, so heavy or external code is either replaced by a small model or havoc’d to a nondet result.

bmc4j ships models for the parts of the JDK and Kotlin stdlib that proofs reach often, so most code just works. This page is about writing, checking, and skipping your own.

Writing a model

Put a class under src/bmcModel with the same fully qualified name as the class it replaces. It shadows the real one on the analysis classpath, so any proof that reaches that class sees your version instead. A model is normal code; it just gives the engine a smaller, easier-to-solve definition.

Checking a model against the real thing

A model is only worth trusting if it behaves like the class it stands in for. @ConformProofsAgainstModel(Target::class) checks that for one proof: it runs the proof twice, once with the model and once against the real class, and both runs must reach the expected verdict.

@BmcProof
@ConformProofsAgainstModel(NoCollisionMap::class)
fun `put then get returns the value`() { ... }

If the model lets the proof pass while the real class would refute it, the real run fails and the gap is surfaced. It is opt-in and scoped to the proof, so passing it means the model agrees with the real class on what this proof exercises, not that the model is sound everywhere. Conform the proofs whose real runs are tractable, and lean on the model for the rest. Goes on a method or a class.

Using the real class instead

Models are global, so every proof sees them. To run one proof against the real class instead, list the models to skip with @ExcludeModels:

@BmcProof
@ExcludeModels(acme.RingBuffer::class, acme.Slot::class)
fun `ring buffer invariant holds against the real class`() { ... }

The real class is always more faithful than a model, so excluding one can only make a proof slower or Unknown, never a false pass. Method-level and class-level exclusions add together.