|
product_posnat: THEORY
%------------------------------------------------------------------------------
% The products theory introduces and defines properties of the product
% function that multiples an arbitrary function F: [posnat -> int] over a range
% from low to high
%
% high
% ----
% product(low, high, F) = | | F(j)
% | |
% j = low
%
% AUTHORS:
%
% Rick Butler NASA Langley Research Center
% Paul Miner NASA Langley Research Center
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING product[posnat]
int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high
posnat_is_T_low : JUDGEMENT posnat SUBTYPE_OF T_low
low, n, m: VAR posnat
high: VAR int
F: VAR function[posnat -> int]
% --------- Following Theorems Not Provable In Generic Framework -------
product_shift: THEOREM product(low+m,high+m,F) =
product(low,high, (LAMBDA (n: posnat): F(n+m)))
product_shift_neg: THEOREM low - m > 0 IMPLIES
product(low-m,high-m,F) =
product(low,high, (LAMBDA n: IF n-m <= 0 THEN 0
ELSE F(n-m)
ENDIF))
product_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES
product(low, high, F) =
product(low, m, F) * product(m+1, high, F)
END product_posnat
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
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
|
