Pluss/Asspegique+
Language Design

Version 0.1

[ 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 Michel Bidoit; any comments and corrections should be addressed to Michel.Bidoit@ens.fr.

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.

The following is very preliminary !
Note: While the former versions of Asspegique only supported a subset of the Pluss specification language, the latest version,(1) known as Asspegique+, supports the whole Pluss specification language; there is therefore no need for distinction between Asspegique+ and Pluss in what follows.

  • 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.1.6 other
  • 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.2.6 other
  • 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.3.7 other
  • 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.4.8 other
  • 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
  • 1.5.6 other
  • 1.6 Other
  • 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.1.3 other
  • 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.2.10 other
  • 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.3.6 other
  • 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 graph
  • 2.4.5 composition, instantiation, sub-framework
  • 2.4.6 other
  • 2.5 Other
  • Footnotes
    • Asspegique, May 14, 1996