|
prelude_aux: THEORY
BEGIN
px: VAR posreal
x,y: VAR real
i: VAR nat
floor_le : LEMMA x <= y IMPLIES floor(x) <= floor(y)
floor_lt : LEMMA x < y IMPLIES floor(x) < floor(y) + 1
floor_div_le: LEMMA y >= 1 IMPLIES floor(px/y) <= px
floor_div_lt: LEMMA y > 1 IMPLIES floor(px/y) < px
floor_le_floor: LEMMA y >= 1 IMPLIES floor(px/y) <= floor(px)
floor_lt_floor_int: LEMMA i > 1 AND x >= i IMPLIES
floor(x / i) < floor(x)
%% this is a generalization of what is already in the prelude
floor_small: LEMMA abs(x) < abs(y) IMPLIES
floor(x/y) = IF x/y >= 0 THEN 0 ELSE -1 ENDIF
END prelude_aux
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.26Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
