Code Generation: Issues and Designs

Slang ATL Specs for Lisp

Release Notes for code generation

See the release notes for details on the code generation process.

Other Lisp Specs and Slang to Lisp Morphisms

Code Generation

Primeval (builtin) Specs

See the SpecWeb page for primeval specs.
Note: each primeval spec and each ATL spec in Specware has an interpretation into Lisp and C++. See the below and the release notes for details. For the primeval specs the translations are in the builtin map for empty to slang-base.

BOOLEAN

Spec: boolean.re

NAT

Spec: nat.re

CHAR

Spec: char.re

String

Spec: string.re

ATL Specs

ATL for Common Lisp

See the SpecWeb page for ATL specs.
Note: each primeval spec and each ATL spec in Specware has an interpretation into Lisp. See the below and the release notes for details.

ARRAY

Slang Spec: array.re
Lisp Spec: simple-vector.re
Slang-to-Lisp: array-to-simple-vector.re

EMPTY

Slang Spec: empty.re

INTEGER

Slang Spec: integer.re
Lisp Spec: integer.re
Slang-to-Lisp: integer-to-integer.re

LIST and LIST-HO

Slang Spec: list.re
Lisp Spec: list.re
Slang-to-Lisp: list-to-list.re

TRIV

Slang Spec: triv.re
Lisp Spec: triv.re
Slang-to-Lisp: triv-to-triv.re

ATL for C++

Same as for Common Lisp. Note: each primeval spec and each ATL spec in Specware has an interpretation into C++. See the below and the release notes for details.

ARRAY

C++ Spec: array.re
Slang-to-C++: array-to-array.re

INTEGER

C++ Spec: integer.re
Slang-to-C++: integer-to-integer.re

LIST

C++ Spec: list.re
Slang-to-C++: list-to-list.re

TRIV

C++ Spec: triv.re
Slang-to-C++: triv-to-triv.re

Other Lisp Specs and Slang to Lisp Morphisms

ARRAY-K

Lisp Spec: array-k.re
Slang-to-Lisp: array-k-to-array-k.re

BITVECTOR-K

Lisp Spec: bitvector.re
Slang-to-Lisp: bitvector-k-to-bitvector-k.re

NAT-CONSTANT and NAT-PREFIX

Lisp Spec: nat-constant.re
Lisp Spec: nat-prefix.re
Slang-to-Lisp: nat-prefix-to-nat-prefix.re

SEQ

Lisp Spec: seq.re

STRING-HO

Lisp Spec: string-ho.re

SpecWeb Index