products/sources/formale Sprachen/PVS/interval_arith/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: TestVDMController.vdmrt   Sprache: Unknown

interval_expr_trig : THEORY
BEGIN

  IMPORTING interval_expr,
            interval_trig
  
  expr : VAR RealExpr
  n    : VAR nat

  pi_safe : [Unit->real] = LAMBDA(u:Unit) : pi

  Pi_Inclusion : JUDGEMENT
    Pi(n) HAS_TYPE (Includes?(pi_safe(unit)))

  PI_n(n): MACRO RealExpr = CONST(pi_safe,Pi(n))

  Sin_Inclusion : JUDGEMENT
    Sin(n) HAS_TYPE (Inclusion?(PreTrue,sin))

  Sin_Fundamental : JUDGEMENT
    Sin(n) HAS_TYPE (Fundamental?(PreTrue))

  SIN_n(n)(expr): MACRO RealExpr = FUN(PreTrue,sin,Sin(n),expr)

  Cos_Inclusion : JUDGEMENT
    Cos(n) HAS_TYPE (Inclusion?(PreTrue,cos))

  Cos_Fundamental : JUDGEMENT
    Cos(n) HAS_TYPE (Fundamental?(PreTrue))

  COS_n(n)(expr): MACRO RealExpr = FUN(PreTrue,cos,Cos(n),expr)

  tan_safe(x:real): real = IF Tan?(x) THEN tan(x) ELSE 0 ENDIF

  Tan_Inclusion : JUDGEMENT
    Tan(n) HAS_TYPE (Inclusion?(TAN?(n),tan_safe))

  Tan_Fundamental : JUDGEMENT
    Tan(n) HAS_TYPE (Fundamental?(TAN?(n)))

  TAN_Precondition : JUDGEMENT
    TAN?(n) HAS_TYPE (Precondition?)

  TAN_n(n)(expr): MACRO RealExpr = FUN(TAN?(n),tan_safe,Tan(n),expr)

  Atan_Inclusion : JUDGEMENT
    Atan(n) HAS_TYPE (Inclusion?(PreTrue,atan))

  Atan_Fundamental : JUDGEMENT
    Atan(n) HAS_TYPE (Fundamental?(PreTrue))

  ATAN_n(n)(expr): MACRO RealExpr = FUN(PreTrue,atan,Atan(n),expr)

END interval_expr_trig

[ Seitenstruktur0.0Drucken  etwas mehr zur Ethik  ]