Proof annotations

A proof is a method marked @BmcProof. It is discovered and run like a JUnit 5 test, so it shows up in your IDE and test reports, but instead of executing the body the engine verifies it. With no attributes you get the common case: prove the property for every input, with the loop bound found for you.

@BmcProof

Attribute	Default	What it does
unwind	AUTO	Loop and recursion bound. AUTO finds the smallest bound that decides; a positive N pins it. See Unwinding.
unwindMax	build cap (16)	Lets AUTO climb higher without pinning a bound.
maxStringLength	build default (16)	Bound on symbolic string length.
unwindingAssertions	true	Return Unknown if the bound is too small, rather than trust a half-explored loop.
solver	built-in MiniSat	Use a different SAT or SMT backend. See External solver.
timeoutSeconds	none	Wall-clock budget. Over it the proof is killed and reported Unknown.
removeExceptionMessages	AUTO	Drop construction of an unread exception message so it can’t slow a proof. AUTO, ON, or OFF.
stringMode	REFINEMENT	How String is modelled. See String modes.
expect	VERIFIED	The verdict the test should get. Set it to REFUTED for a fail-on-purpose proof.
allowStubs	none	Methods you knowingly let run as havoc’d stubs, to silence their footnote.
acknowledgeUnmodelled	none	JDK members bmc4j can’t model that you accept as havoc instead of Unknown.

expect takes a Verdict: VERIFIED, REFUTED, UNKNOWN, TIMEOUT, or VACUOUS.

Project-wide defaults for most of these live in the plugin config; a value on @BmcProof always wins.

Companions

On the same method, unless noted:

• @LoopUnwind(loop, bound) pins one specific loop’s bound. Repeatable. See Unwinding.
• @Shard(n) pins a proof, or a whole class, to a CI shard. @ShardSlices spreads a split proof’s slices across shards. See Sharding.
• @BmcProfile prints where the engine spent its time. See Profiling.
• @JbmcOptions("...") passes raw flags straight to the engine.

Contracts

To prove a method against another’s contract instead of inlining its body, see Contracts.