Specware Logo

Home | Releases | Documentation | Support

Specware 4.1

Release Notes

New Features

  • The Specware shell is now independent from Lisp. It has its own prompt and commands. The syntax of some existing commands has been slightly changed. Several commands have been added. See the User Manual for details.

  • Besides Lisp, Specware can now generate Java code and C code. See the Language Manual for the extensions to the syntax of target-code-terms and the User Manual for usage details.

  • A built-in operator for record update has been added. See the Language Manual for details.

  • Claims (i.e. axioms, theorems, and conjectures) can now have qualified names, not only simple names, just like types and ops. See the Language Manual.

  • The term "sort" has been replaced with "type", both in the documentation and in the syntax (see the Language Manual). The old syntax is still allowed as equivalent to the new syntax, but it is deprecated and will be eventually made illegal. See the Language Manual.

  • The syntax for polymorphic op-declarations, op-definitions, and claim definitions has been made more terse and less confusing. For instance, instead of op f : fa(a) List a -> List a the syntax is now op f : [a] List a -> List a, which is terser and avoids any possible confusion with the quantifier faused in expressions. The old syntax is still allowed as equivalent to the new syntax, but it is deprecated and will be eventually made illegal. See the Language Manual for details.

  • The type Boolean and the ops for logical connectives and inequality, which were previously declared in the spec Boolean in the base libraries, are now built-in, in the sense that they are automatically available in every spec, independently on whether the spec is part of the base libraries or not. In particular, the spec Boolean is no longer in the base libraries. See the Language Manual.

  • The syntax of the logical connectives for conjunction and disjunction has changed from "&" and "or" to "&&" and "||", which is more consistent. The old syntax is still allowed as equivalent to the new syntax, but it is deprecated and will be eventually made illegal. See the Language Manual.

  • The specs in the base libraries have been extended to include complete axiomatizations for all the types and ops declared in them, most notably integer and natural numbers. Previously, some types and ops, listed in the spec Primitive in the base libraries, were assumed to have a fixed interpretation. Now, aside from the built-in boolean type and ops, there is no such assumption for any other type or op in the base libraries. In particular, the spec Primitive is no longer in the base libraries. See the base library specs in the distribution as well as Appendix B of the Language Manual for details.

  • The Prover Base Library has been restructured to parallel the structure of the Base Library. The properties that make up /Library/ProverBase/Top.sw is used as further hypothesis for each proof.

  • The Specware/Snark interface handles a larger subset of the MetaSlang type system. In particular axioms for Co-Product and Product types are generated and sent to Snark. The axioms associated with a Type T , are names T_def , and can be referred to in the using clause of a proof unit.

  • A simple linear inequality decision procedure has been added as a prover option. By default the inequality decision procedure attempts to discharge the conclusion of a proof unit. If that fails then Snark is invoked as usual. The user can also specify a specific prover to use. See the User Guide.