JML Tutorial - Time and Error Limits
This page describes how to limit the time spent on proof attempts.
Timeouts
You can set a timeout for a proof attempt with the --timeout
option.
The value given is an integer number of seconds. A limit of a few minutes
(e.g. 180) is reasonable. A shorter limit will let fast proofs be reported
while not taking up too much time on longer proofs.
Limiting errors
By default, each method is a single, individual proof attempt. OpenJML looks for a verification failure in the method. If one is found, it is reported and the tool goes on to find a next one. (The order in which assertion violations are found is non-deterministic.) The proof attempt quits when the tool cannot find any more failures.
However, the last step – where no more assertion violations are found –
can be time-consuming. So sometimes it is useful to stop after just one verification failure (or a small fixed number) is reported.
The number of errors reported for each method can be limited using the
--escMaxWarnings
option. By default it is set to a very large number,
but it is a reasonable working style to set it to 1.
Note that there will be no proof attempts for any methods in a file if there are parsing or type-checking errors in the source or specification files.