products/sources/formale Sprachen/Delphi/Autor 0.7/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: TimeBug.vdmpp   Sprache: Unknown

BarrierReached : () ==> ()
BarrierReached() == 
(
 while  (card dom wakeUpMap = barrierCount) do
   (
    currentTime := currentTime + stepLength;
    let threadSet : set of nat = {th | th in set dom wakeUpMap 
             & wakeUpMap(th) <> nil and wakeUpMap(th) <= currentTime }
  in
     (debugSet := threadSet;
   for all t in set threadSet 
   do
    wakeUpMap := {t} <-: wakeUpMap;
   );
 );
)
post forall x in set rng wakeUpMap & x = nil or x > currentTime;

AddToWakeUpMap : nat * [nat] ==> ()

[ Verzeichnis aufwärts0.0unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]