Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: top.pvs Sprache: PVS

Original von: PVS^©

top: THEORY
%-------------------------------------------------------------------------------
% Complex Numbers
%
%     Author: David Lester, Manchester University & NIA
%
%
% The complex numbers are defined (axiomatically) in this way so that we can
% conveniently use the numeric constants 0, 1, 2 etc.
%
% The alternative -- using pairs of reals to represent the real and imaginary
% components -- would lead to the somewhat unappealing formulation of Euler's
% result as "exp((0,1)*(pi,0)) = (-1,0)". As a matter of taste, I prefer the
% somewhat more elegant formulation: "exp(i*pi) = -1".
%
% When theory interpretations can handle this, we'll be able to prove that the
% two formulations are equivalent, and hence use the beautiful version, and
% consigning the undignified version to the background!
%
% If we get really lucky, the number_fields_bis ("bis" from the Italian for
% extra) can be consigned to the dustbin of history, and it's functions
% incorporated into the general PVS decision procedures. In the mean time...
%
%
%     Version 1.0            5/29/04   Initial version (DRL)
%     Version 2.9            4/25/07
%------------------------------------------------------------------------------
BEGIN

  IMPORTING complex_types,       % Basic Definitions of Complex Number Types
            polar,               % Polar coordinate complex numbers
            arithmetic,          % Basic Arithmetic on Complex Numbers
            exp,                 % Complex logarithm and exponential functions
            complex_sqrt,        % sqrt of a complex number
            complex_field,       % complex numbers form a field
            complex_sets         % set-valued complex functions

END top

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.