debugging
(true iff you're in debug assertion mode) can't you write something like
assert debugging ==> (youngest >= 0);
or at least you could if you also had a shortcut implication operator. Which you don't but you could switch to the inverse variable, running
and write
assert running || (youngest >= 0);
which isn't quite as nice but would work. Perhaps release
is a better name than running
.
requires
preconditions will be omitted if the analysis doesn't require the; while recommends
preconditions will always be dynamically checked. See: "Specifying the Boundary Between Unverified and Verified Code." David R. Cok & K. Rustan M. Leino in LNC13360.
https://link.springer.com/chapter/10.1007/978-3-031-08166-8_6