Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/analysis/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: poly2bernstein.pvs Sprache: PVS

poly2bernstein : THEORY
BEGIN

  IMPORTING multi_polynomial,
            multi_bernstein

  polydegmono,
  bsdegmono   : VAR DegreeMono
  pprod       : VAR Polyproduct
  mpoly       : VAR MultiPolynomial
  nvars,terms : VAR posnat
  cf          : VAR Coeff

  bs_convert_mono(pprod,polydegmono,bsdegmono,nvars)(j:nat)(s:nat): real =
    IF s>bsdegmono(j) THEN 0
    ELSE sigma(0,s,LAMBDA(i:nat):IF i>s OR i>polydegmono(j) THEN 0
                                 ELSE pprod(j)(i)*(C(s,i)/C(bsdegmono(j),i))
                                 ENDIF)
    ENDIF

  bs_convert_poly(mpoly,polydegmono,bsdegmono,nvars,terms)(r:nat): Polyproduct =
    bs_convert_mono(mpoly(r),polydegmono,bsdegmono,nvars)

  bs_convert_poly_def: LEMMA le_below_mono?(nvars)(polydegmono,bsdegmono) IMPLIES
    multipoly_eval(mpoly,polydegmono,cf,nvars,terms) =
    multibs_eval(bs_convert_poly(mpoly,polydegmono,bsdegmono,nvars,terms),
                 bsdegmono,cf,nvars,terms)

END poly2bernstein