Quelle MATH.vdmpp Sprache: VDM

class MATH

-- Overture STANDARD LIBRARY: MATH
--      --------------------------------------------
-- Version 1.0.0
--
-- Standard library for the Overture Interpreter. When the interpreter
-- evaluates the preliminary functions/operations in this file,
-- corresponding internal functions is called instead of issuing a run
-- time error. Signatures should not be changed, as well as name of
-- module (VDM-SL) or class (VDM++). Pre/post conditions is
-- fully user customisable.
-- Dont care's may NOT be used in the parameter lists.

  functions
public static
    sin:real +> real
    sin(v) ==
    is not yet specified
    post abs RESULT <= 1;

public static
    cos:real +> real
    cos(v) ==
    is not yet specified
    post abs RESULT <= 1;

public static
    tan:real -> real
    tan(a) ==
    is not yet specified
    pre cos(a) <> 0;

public static
    cot:real -> real
    cot(a) ==
    is not yet specified -- Could also be: 1/tan(r)
    pre sin(a) <> 0;

public static
    asin:real -> real
    asin(a) ==
    is not yet specified
    pre abs a <= 1;

public static
    acos:real -> real
    acos(a) ==
    is not yet specified
    pre abs a <= 1;

public static
    atan:real +> real
    atan(v) ==
    is not yet specified;

public static
    acot:real +> real
    acot(a) ==
    atan(1/a)
    pre a <> 0;

public static
    sqrt:real -> real
    sqrt(a) ==
    is not yet specified
    pre a >= 0;

public static
    pi_f:() +> real
    pi_f () ==
    is not yet specified

  operations

public static
    srand:int ==> ()
    srand(a) ==
    let - = MATH`srand2(a) in skip
    pre a >= -1;

public static
    rand:int ==> int
    rand(a) ==
    is not yet specified;

public static
    srand2:int ==> int
    srand2(a) ==
    is not yet specified
    pre a >= -1

  functions

public static
    exp:real +> real
    exp(a) ==
    is not yet specified;

public static
    ln:real -> real
    ln(a) ==
    is not yet specified
    pre a > 0;

public static
    log:real -> real
    log(a) ==
    is not yet specified
    pre a > 0;

public static
    fac:nat -> nat1
    fac(a) ==
    is not yet specified
    pre a < 21;         -- The limit for 64-bit calculations

  values
public
    pi = 3.14159265358979323846

end MATH

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.