| products/Sources/formale Sprachen/VDM/VDMPP/KLVPP/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Test.vdmpp Sprache: VDMOriginal von: VDM© |
|
||||||
|
\section{The Test Class}
The Test class defines an environment for executing test cases. The class maintains a reference to a KLV instance, and it provides two operations, runOneTest for execution of one test event, and runTests for execution of a sequence of test events. Different kinds of test events can be executed. These are defined by the Event class hierarchy defined below. The data types represent different kinds of categories of results. \begin{vdm_al} class Test types public TestResult = KLVstate | BeaconsMet | MaxSpeed; public KLVstate :: cd : CabDisp eb : EmerBreak; public CabDisp :: alarm : bool emerbr : bool grfault : bool; public EmerBreak :: break : bool; public BeaconsMet :: ann : seq of TIVD res : seq of TIVE; public TIVD :: ts : real; public TIVE :: sp : real; public MaxSpeed :: ms: real; instance variables klv : KLV := new KLV(); operations public runTests : seq of Event ==> seq of TestResult runTests (events) == return [e.execute(klv) | e in seq events ]; public runOneTest : Event ==> TestResult runOneTest (event) == return event.execute(klv) pre ((isofclass(HeadMeetBeaconEvent,event) => let e1: HeadMeetBeaconEvent = event in isofclass(TIV_E, e1.getBeacon())) => klv.getAnnouncements() <> []) and ((isofclass(TailMeetBeaconEvent,event) => let e2: TailMeetBeaconEvent = event in isofclass(TIV_E,e2.getBeacon())) => (klv.getFirstSpeedRestriction() or klv.getSpeedRestrictions() <> [])); end Test \end{vdm_al} ¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
