Specware 4.0.5

Release Notes

New Features

• Several new top-level commands were added to Specware:

  :sw-help		Print list of processing commands
  :dir		List files in current folder
  :swll spec-unit-id		Incrementally generate and load Lisp
  :sw-spec spec-unit-id		Set context for :swe command
  :swe expr		Evaluate and print Metaslang expression

• Improvements in Lisp code generation include consistency of the order in which functions are generated and a new function naming scheme for curried/uncurried & n-argument/1-argument versions.

• The prover interface to Snark has been enhanced.

• Improvements were made to the Base libraries.

• Quick Reference guide has been added to the documentation.

Bug Fixes

• One-field record descriptors and subsorts are now handled correctly by the Lisp code generator.
• The equivalence relation of quotient types has been fixed.
• The parser semantics for the project construct has been corrected.
• Memory usage by the system has been improved when processing large specs.
• The number of error messages printed has been reduced.

Changes to Syntax

• Commas are now required by the proof-term when listing more than one claim in the optional using {claim,…} sequence.
• Double-quotes are no longer required around the argument to the :swpath command.

Changes to Documentation

• The Libraries section of the Language Manual reflects changes to the Base Libraries.
• The Code Generation section of the User Manual reflects changes to Lisp code generation.
• The new top-level commands are documented in the User Manual.