Spec# 1.0.7301 for Microsoft Visual Studio 2005 Release Notes

Installing Simplify

See Installing Simplify.

Changes since last release

  1. Documentation on how to write Spec# code!!
  2. A new Boogie option has been added (although currently it is not in the help screen): /concat will treat multiple input BPL files as a single file, but all error messages will be relative to the file.
  3. Quantifiers: Added new quantifiers: sum, product, max, min. Added support for these quantifiers, as well as count and exists unique, to Boogie. Also added Boogie support for using these on displays in specifications (for example, max{x,y}).
  4. More contracts on the out-of-band specifications, especially all GetEnumerator methods.
  5. Relaxed delayed type checking: can now read from delayed references, but get possibly null references with unknown delay.
  6. Added attributes and context checks for [Inside], [Additive], [Captured], [Rep], and [Peer]. Marked [Owned] as obsolete.
  7. Fixes for applying out-of-band contracts.
  8. Modifies: Allow “e.0” for expressions “e” in modifies clauses. It means that the method modifies nothing. Modifies clauses have no restriction on the visibility of referenced members. (More use will be made of these in a future release of Boogie.)
  9. Allow “e.**” for expressions “e” in modifies clauses. It means that all fields of all peers of “e” may be modified.
  10. Non-null checking: unnecessary coercions to non-null are removed and warnings about explicit unnecessary coercions are now given. Many other fixes to the non-null checking.
  11. The message in exceptions thrown at runtime when a contract is violated has changed: it now contains the source text of the condition.
  12. For debugging, the name of “old” locals is now “old(…)” where “…” is the source text of the old expression.
  13. For Boogie, all contracts are split into their top-level conjuncts so that error messages will know exactly which part of the contract failed.
  14. The visibility rules have changed for postconditions. They may now mention things that are not as visible as the method itself, but the members mentioned must be visible to all implementations of the method.
  15. Better purity checking: no update operators (assignment) can appear in a contract.
  16. [NoDefaultContract] can appear on parameters, but only on reference-type parameters.
  17. Runtime checking: non-null checking happens in only in Debug builds.
  18. Improved handling of value arrays and exact arrays types.
  19. Implemented more Boogie support for struct types.
  20. Additional information about string values and string equality.
  21. Fixed handling of ref/out parameters.
  22. New and much faster algorithm in one of the VC generation phases.
  23. Boogie now knows as much about [StrictReadonly] fields (their type, allocation status, etc.) as it does about other fields.
  24. More support for the use of [StateIndependent] methods.
  25. Boogie output now shows number of errors, number of methods verified, and number of inconclusive verifications.
  26. Several improvements in the modifies-clause checking.
  27. Changes in various axioms, with the effect to big performance improvements.
  28. Better handling of IntPtr and UIntPtr instructions in Boogie, and some more knowledge of extreme integer values.
  29. Fixes in the interaction of deferred constructors and pack operations.
  30. Improved and corrected support for various integer conversions.
  31. BoogiePL change: In order for constants to be considered distinct, they must be declared with “const unique”. This works for constants of any type. (Previously, all constants of type “name” were distinct, and constants of other types were not.)
  32. Improved handling of some type parameters.
  33. Changed the way owners were automatically assigned for peer fields, resulting in a marginally stricter discipline, but reaping huge gains in prover performance.
  34. Added more comments in BoogiePL code generated from compiled Spec#.
  35. By default with /level:1, Boogie now assumes that loops respect the method’s modifies clause. With /level:2, Boogie checks this property. This behavior can be customized with the enhanced /modifiesOnLoop switch.
  36. Expanded VC generation pipeline: Various improvements in the availability and selection of choices that affect VC generation. In particular, the /vc, /vcAst, and /prover flags work better together. Added /proverLogAppend switch, which uses the /proverLog file in append mode. Added /proverWarnings to control where prover warnings go. Added support for the Z3 theorem prover (this prover is not yet available publicly, but a plan calls for such a release later this year).
  37. Fixed omitted BoogiePL where-clause assumptions.
  38. Fixed BoogiePL type check bug, which previously had restricted the use of “any”-typed variables as actual out parameters.
  39. Added axioms to support the implementation of pure interface methods.
  40. Improvements in receiving Simplify output messages, including: Produce better Boogie warning if it encounter’s Simplify’s “triggerless quantifier body” message.
  41. If there is a problem with running the Boogie plug-in from within Visual Studio, a message is printed in the Visual Studio Output window.