|
\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.22 Sekunden
(vorverarbeitet)
¤
|
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.
|
