Quelle  Event.vdmpp

\section{The Event Class}

The Event class is the abstract super class of the class hierarchy of
test events. Each class implementing this event class must define an
execute operation.

\begin{vdm_al}
class Event

operations

  public
  execute : KLV ==> Test`TestResult
  execute (-) ==
    is subclass responsibility;

end Event
\end{vdm_al}