2009-04-04: Updated Assertion Language Manual
Version 6.3 of the
Bound-T Assertion Language Manual (pdf) was
published today on the Bound-T website.
This is a significant update of the assertion language.
New features introduced include:
- The ability to identify program parts by source-code
position. When you write an assertion for a loop
or a call, you can now identify the loop or call by its
place in the source code, either directly by using the
line number of a source-code line, or indirectly by using
the name of a mark embedded at this point in the source
code.
- The ability to assert bounds on the number of starts
of a loop. This sets bounds on the number of times the
flow of execution reaches the loop at all. For example,
asserting that a loop starts zero times means that
the loop is never reached (is infeasible).
The use of marks in source-code files is helped by a
new auxiliary program find_marks that Tidorum has
announced.