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.