| products/sources/formale Sprachen/Delphi/Autor 0.7/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Decimal.v Sprache: VDMUntersuchung VDM© |
|
||||||
|
\begin{vdm_al}
class GLOBAL values public SENSOR_APERTURE = 90; public FLARE_APERTURE = 120; public DISPENSER_APERTURE = 30 types -- there are three different types of missiles public MissileType = <MissileA> | <MissileB> | <MissileC>; -- there are nine different flare types, three per missile public FlareType = <FlareOneA> | <FlareTwoA> | <DoNothingA> | <FlareOneB> | <FlareTwoB> | <DoNothingB> | <FlareOneC> | <FlareTwoC> | <DoNothingC>; -- the angle at which the missile is incoming public Angle = nat inv num == num < 360; public EventId = nat; public Time = nat operations pure public canObserve: Angle * Angle * Angle ==> bool canObserve (pangle, pleft, psize) == def pright = (pleft + psize) mod 360 in if pright < pleft -- check between [0,pright> and [pleft,360> then return (pangle < pright or pangle >= pleft) -- check between [pleft, pright> else return (pangle >= pleft and pangle < pright); public getAperture: () ==> Angle * Angle getAperture () == is subclass responsibility; end GLOBAL \end{vdm_al} \begin{rtinfo}[GLOBAL`canObserve] {vdm.tc}[GLOBAL] \end{rtinfo} ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot 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 |
