Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/TRS/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Test.vdmsl Sprache: VDM

Original von: VDM^©

\section{The Test Module}

\begin{vdm_al}
module Test

imports
from AST all,
from STATSEM all,
from DYNSEM all

exports all
definitions

values

  binexpr: AST`Expr =
           mk_AST`BinaryExpr(mk_AST`IntVal(4),
                             <Add>,
                             mk_AST`IntVal(5))
functions

RunTypeCheck: () -> bool * [AST`Type]
RunTypeCheck() ==
  STATSEM`wf_Expr(binexpr,{|->});

RunEval: () -> AST`Value
RunEval() ==
  DYNSEM`EvalExpr(binexpr,{|->})

end Test
\end{vdm_al}