products/Sources/formale Sprachen/PVS/exact_real_arith/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: product_posnat.prf   Sprache: PVS

Untersuchung PVS©
%------------------------------------------------------------------------------
% Division
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

div: THEORY

BEGIN

  IMPORTING mul, inv

  x,y:   VAR real
  nzy:   VAR nonzero_real
  cx,cy: VAR cauchy_real
  nzcy:  VAR cauchy_nzreal
  
  div(x,nzy):real = x * inv(nzy)

  cauchy_div(cx,nzcy):cauchy_real = cauchy_mul (cx, cauchy_inv(nzcy))

  div_lemma: LEMMA cauchy_prop(x,cx) AND cauchy_prop(nzy,nzcy)
                   => cauchy_prop(x/nzy, cauchy_div(cx,nzcy))

END div

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff