The Datatypes REAL and COMPLEX in CASL

Till Mossakowski
Markus Roggenbach

13 April 1999

This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.3.

Abstract

Real (and, to some degree, also complex) numbers should be a part of the CASL standard library, since they occur in many applications and programming languages. In this note, we address the specification of real and complex numbers at two levels: at the mathematical level and at the computer representation level.

[RM99a][RM99b] can be seen as complementary notes, since they contain basic datatypes resp. describe annotations and syntax extensions we frequently use here.

Full Contents

  • Version History
  • 1 Introduction
  • 2 Basic Datatypes
  • 2.1 The Specifications of Note M-6
  • 2.2 Naming Conventions for Specifications in Note M-6
  • The Prefix "Generate".
  • The Prefix "Define".
  • 2.3 Representations of Numbers in Note M-6
  • 3 Annotations
  • 4 A Specification of Real Numbers
  • 4.1 The Structure of the Specifications
  • 4.2 Some Algebraic Specifications
  • 4.3 The Specification DefineBasicReal
  • 4.4 The Specification BasicReal
  • 4.5 The Specification CompactBasicReal
  • 5 More About the Specification BasicReal
  • 5.1 Proof of the Uncountability of the Reals
  • 5.2 The Categoricity of the Reals
  • 5.3 The Specification of the Reals in Higher-Order CASL
  • 5.4 A Short Remark on Related Work
  • 6 Towards a Datatype REAL
  • 6.1 Screens and Roundings
  • 6.2 Proposal of an Abstract Datatype REAL
  • 6.3 Proposal of two Executable Datatypes REAL
  • Proposal Based on [KM81]
  • Proposal Based on the IEEE Standards.
  • Comparison of the Proposed Executable Datatypes.
  • 7 A Specification of Complex Numbers
  • References
  • Footnotes

  • CoFI Note: M-7 -- Version: 0.2 -- 13 April 1999.
    Comments to till@informatik.uni-bremen.de