CASL - The CoFI Algebraic Specification Language
Tentative Design: Language Summary, version 0.95

With annotations by the CoFI Semantics Task Group
concerning questions and doubts, and how these
will be resolved in version 0.96 of the design

25 April 1997

This document is available for browsing on WWW, and in various formats for printing by FTP.

Abstract

This is version 0.95 of the official summary of the Tentative Design of CASL, the CoFI Algebraic Specification Language, annotated by the CoFI Semantics Task Group with questions and doubts concerning the meaning of constructs and the semantics of the interaction of constructs, and with notes on how these worries will be discharged in version 0.96 of the design. Comments should be sent to the CoFI Semantics mailing list (cofi-semantics@brics.dk).

Contents

  • About this document
  • Version history
  • Contributors
  • Structure
  • Part I: Basic Specifications
  • 1 Basic Concepts
  • 1.1 Signatures
  • 1.2 Models
  • 1.3 Sentences
  • 1.4 Satisfaction
  • 1.5 Proof System
  • 2 Basic Constructs
  • 2.1 Signature Declarations
  • 2.1.1 Sorts
  • 2.1.2 Constants and Functions
  • 2.1.3 Predicates
  • 2.2 Variable Declarations
  • 2.3 Axioms and Terms
  • 2.3.1 Quantifiers
  • 2.3.2 Logical Connectives
  • 2.3.3 Atomic Formulae and Terms
  • 2.4 Sort Generation
  • 3 Subsorting Concepts
  • 3.1 Signatures
  • 3.2 Models
  • 3.3 Subsorted Sentences
  • 4 Subsorting Constructs
  • 4.1 Subsort Declarations
  • 4.2 Predicative Subsort Definitions
  • 4.3 Axioms and Terms
  • Part II: Structured Specifications
  • 5 Structuring Concepts
  • 6 Structuring Constructs
  • 6.1 Structured Specifications
  • 6.1.1 Translations and Reductions
  • 6.1.2 Unions and Extensions
  • 6.2 Type Definition Group
  • 6.3 Generic Specifications
  • Part III: Architectural Specifications
  • 7 Architectural Concepts
  • 8 Architectural Constructs
  • 8.1 Unit Declarations
  • 8.2 Unit Compositions
  • Part IV: Specification Libraries
  • 9 Library Concepts
  • 10 Library Constructs
  • 10.1 Libraries
  • 10.2 Downloading
  • Appendices:
  • Appendix A: Abstract Syntax
  • Identifiers
  • Basic Specifications
  • Basic Specifications with Subsorts
  • Structured Specifications
  • Generic Specifications
  • Architectural Specifications
  • Specification Libraries
  • Appendix C: Proposed Changes
  • Basic Constructs: Attribution
  • Basic Constructs: Local Declarations and Definitions
  • Architectural Constructs: Local Definitions
  • Library Constructs: Local Definitions
  • Index
  • Footnotes
    • This document was converted from LaTeX2e sources to HTML using Hyperlatex 2.2.
    CoFI Note: S-1 --Version 1.3-- 25 April 1997.
    Comments to cofi-semantics@brics.dk