SPECTRAL
Language Design

Version 0.2

[ Outline | ABEL | ACT-ONE+TWO | ASF+SDF | Asspegique+ | Clear |
   EML | LPG | LSL | OBSCURE | RSL | SMoLCS | SPECTRAL | Spectrum | Z ]

This document is part of the CoFI Catalogue of Algebraic Specification Frameworks. It was provided by Bernd Krieg-Brückner; any comments and corrections should be addressed to bkb@Informatik.Uni-Bremen.DE.

It will be made available formatted for printing as compressed Postscript (~100Kb) and DVI (~50Kb).

The WWW version provides only a rough approximation (mostly generated automatically by Hyperlatex) to the symbols used in the formatted versions. Please inform pdmosses@brics.dk about any places where an alternative approximation is desirable!

N.B. All sections of the catalogue are TENTATIVE first versions, unless explicitly marked otherwise. Sections dealing with Methodology, Tools, and Documentation will be added later.

  • 1 Specification in the Small
  • 1.1 Basic Constructs
  • 1.1.1 signatures
  • 1.1.2 axioms
  • 1.1.3 models
  • 1.1.4 constraints
  • 1.1.5 status
  • 1.2 Types
  • 1.2.1 predefined types
  • 1.2.2 algebra of types
  • 1.2.3 parametrized type constructors
  • 1.2.4 polymorphic types
  • 1.2.5 dependent types
  • 1.3 Partiality
  • 1.3.1 subtypes defined by predicates
  • 1.3.2 subtypes declared in the signature
  • 1.3.3 equations
  • 1.3.4 (un)definedness
  • 1.3.5 logic
  • 1.3.6 strictness
  • 1.4 Notations
  • 1.4.1 offside rule
  • 1.4.2 graphical symbols
  • 1.4.3 overloading
  • 1.4.4 mixfix notation
  • 1.4.5 operator precedence
  • 1.4.6 associativity
  • 1.4.7 values of predefined types
  • 1.5 Abbreviations
  • 1.5.1 type inference
  • 1.5.2 conditionals
  • 1.5.3 variable abstraction
  • 1.5.4 variable inference
  • 1.5.5 lambda-abstraction
  • 2 Specification in the Large
  • 2.1 Structuring Concepts
  • 2.1.1 structure of specifications v. programs
  • 2.1.2 structuring logic/institution-independence
  • 2.2 Basic Constructs
  • 2.2.1 naming
  • 2.2.2 union
  • 2.2.3 renaming
  • 2.2.4 hiding
  • 2.2.5 sub-specifications
  • 2.2.6 nesting of signatures
  • 2.2.7 morphisms as entities
  • 2.2.8 behavioural encapsulation
  • 2.2.9 other basic structuring constructs
  • 2.3 Parametrization
  • 2.3.1 specifications parametrized by programs
  • 2.3.2 specifications of parametrized programs
  • 2.3.3 higher-order parametrization
  • 2.3.4 dependent specifications
  • 2.3.5 uniqueness of instantiations
  • 2.4 Multiple Logics
  • 2.4.1 heterogeneous specifications
  • 2.4.2 heterogeneous developments
  • 2.4.3 logic morphisms, representation morphisms
  • 2.4.4 navigation in logic (sub)graph
  • 2.4.5 composition, instantiation, sub-framework
    • SPECTRAL, May 14, 1996