Specware 4.2

Release Notes

We now use Steel Bank Common Lisp (SBCL) as the host system for Specware on Linux and Mac OS X. This improves Specware’s speed and supports Specware for Mac OS X on Intel.

Miscellaneous bug fixes.

New language features (Specware Language Manual section in parentheses)

• Guarded patterns (2.7.2)

• Special syntax for monads (2.6.16)

• Underscore (_) is a wild card in qualifications in translations (2.3.2.3)

• Sum and Quotient types are only allowed at the top-level, i.e., on the right-hand side of type definitions (2.4.3)

• New combined op and def syntax to facilitate sub-type definition (2.4.4). E.g.,

   op [a] nth (l : List a, i : Nat | i < length l) : List a = ...
  

• Allow switch between word and non-word style in names at underscore (2.2.1). E.g.,

   +_2
  

• Hexadecimal literals (2.2.1)

• Use of X-Symbol package to support non-ascii symbols (2.2.2)

• Also see Chapter 9 of the Specware User manual.

New Libraries (under Library/General).

Experimental support for using Isabelle/HOL to prove proof obligations. See Specware-Isabelle Interface manual.