The translation of executable specs to Lisp code is straightforward for the most part as Lisp is a higher-order functional language. Functional expressions go to lambda expressions and most Specware types are implemented as Lisp lists and vectors apart from the strings, numbers, characters and booleans which are implemented by the corresponding Lisp datatypes. This guide is meant primarily to help the user in calling and debugging the functions generated from a spec, so we concentrate on the translation of op names to Lisp names and the implementation of types. The implementation details of procedural constructs such as pattern-matching are omitted. The interested user is free to examine the Lisp code itself, which is simple but verbose for pattern-matching constructs.
Specware ops are implemented using Lisp defuns if they are functions, defparameters otherwise. Their names are upper-cased and put in the package with the same name as the qualifier, or SW-USER if unqualified. However, if the name is that of a built-in Lisp symbol, the name is prepended with the character "!" and not upper-cased. If the qualifier of the op is the same as a built-in Lisp package then "-SPEC" is appended to the spec name to get the package name. For example, the Lisp code for the spec:
Z qualifying spec
def two: Nat = 2
def add1(x:Nat): Nat = x + 1
endspec |
is
(DEFPACKAGE "Z") (IN-PACKAGE "Z") (DEFPARAMETER TWO 2) (DEFUN ADD1 (X) (INTEGER-SPEC::+-2 X 1)) |