SPECL

摘要

The SPECL programming system is an attempt to combine the characteristics of an implementation language with those desirable for verifiability (human and mechanical) and transportability. The former requires efficient code generation and access to hardware; the latter requires a highly structured language and isolation of machine dependencies. SPECL will be embedded in the ECL programming system, which currently includes an interpreter and compatible compiler for the extensible language EL1, and a set of tools for debugging, metering, and verification. The SPECL compiler (under design) will restrict the semantics of EL1 to eliminate the need for run-time support and type checking, and couple specification of machine representation of modes and operators with the EL1 definitional mechanism to enable generation of efficient object code.