%------------------------------------------------------------------------------
% Rationals
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
rat: THEORY
BEGIN
IMPORTING cauchy, int, div
x: VAR rat
i: VAR int
pn: VAR posnat
pns: VAR (nonempty?[posnat])
denominators(x):(nonempty?[posnat]) = {pn | EXISTS i: x = i/pn}
denominator(x):posnat = min(denominators(x))
numerator(x):int = x*denominator(x)
cauchy_rat(x):cauchy_real
= cauchy_div(cauchy_int(numerator(x)),cauchy_int(denominator(x)))
rat_lemma: LEMMA cauchy_prop(x, cauchy_rat(x))
END rat
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.12Angebot
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
|