| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/PacemakerSimplePP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 976 B |
|
Quelle Heart.vdmpp Sprache: VDM |
|||||||||
|
class Heart
types public Trace = seq of [Event]; public Event = <A> | <V>; values instance variables aperiod : nat := 15; vdelay : nat := 10; operations public Heart: nat * nat ==> Heart Heart(aperi,vdel) == (aperiod := aperi; vdelay := vdel); public IdealHeart: () ==> Trace IdealHeart() == return [ if i mod aperiod = 1 then <A> elseif i mod aperiod = vdelay + 1 then <V> else nil | i in set {1,...,100}]; public FaultyHeart() tr : Trace ext rd aperiod : nat post len tr = 100 and Periodic(tr,<A>,aperiod) and not Periodic(tr,<V>,aperiod); functions public Periodic: Trace * Event * nat1 -> bool Periodic(tr,e,p) == forall t in set inds tr & (tr(t) = e) => (t + p <= len tr => ((tr(t+p) = e and forall i in set {t+1, ..., t+p-1} & tr(i) <> e)) and (t + p > len tr => forall i in set {t+1, ..., len tr} & tr(i) <> e)); end Heart ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28