| products/Sources/formale Sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: measure_equality.prf Sprache: VDMUntersuchung VDM© |
|
||||||
|
\begin{vdm_al}
class InsertAddress is subclass of EnvironmentTask operations public InsertAddress: EventDispatcher * nat ==> InsertAddress InsertAddress (ped, pno) == EnvironmentTask("InsertAddress", ped, pno); -- handleEvent receives the responses from the system -- and checks whether the response time for the matching -- stimulus was less than or equal to 2000 time units protected handleEvent: Event ==> () handleEvent (pev) == duration (0) logSysToEnv(pev.getEvent()); -- post checkResponseTimes(e2s,s2e,6000); -- createSignal generates the stimuli for the system createSignal: () ==> () createSignal () == duration (0) if (card dom e2s < max_stimuli) then ( dcl num : nat := getNum(); logEnvToSys(num); raiseInterrupt("HandleKeyPress", num) ); -- start the thread of the task public Run: () ==> () Run () == start(self) thread periodic (1000,0,0,0) (createSignal) end InsertAddress \end{vdm_al} ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
