Spec# 1.0.6003 for Microsoft Visual Studio 2005 Beta 2 Release Notes

Installing Simplify

See Installing Simplify.

Changes since last release

1. The compiler now enforces that all method calls used in assert/assume statements are marked as pure (Pure, Confined, or StateIndependent). This had already been the case for pre- and postconditions and object invariants.
2. In Boogie, the abstract interpretation now runs by default and infers loop invariants for "for-loops". This means that Boogie should no longer complain about array indices possibly being out of bounds in a for-loop.
3. Many bug fixes...