Stufen

Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Sprache: Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 8 kB

Quelle product_seq_scaf.pvs Sprache: PVS

product_seq_scaf: THEORY
BEGIN

   IMPORTING finite_sequences[posnat]

   fs: VAR finite_sequence

   product_rec(fs: finite_sequence, i: below(length(fs)) ): RECURSIVE posnat =
                 IF i = 0 THEN seq(fs)(0)
                 ELSE seq(fs)(i) * product_rec(fs,i-1)
                 ENDIF MEASURE i

   fs1,fs2: VAR finite_sequence
   n,m: VAR nat

   product_rec_mult: LEMMA n < length(fs1 o fs2) IMPLIES
                   product_rec(fs1 o fs2,n) =
                          IF n < length(fs1) THEN
                             product_rec(fs1,n)
                          ELSIF length(fs1) = 0 THEN
                             product_rec(fs2,n)
                          ELSE
                             product_rec(fs1,length(fs1)-1)
                             * product_rec(fs2,n-length(fs1))
                          ENDIF

   product_rec_caret: LEMMA n < length(fs) AND m < length(fs)
                               AND n <= m IMPLIES product_rec(fs, n) =
                               product_rec(fs ^ (0, m), n)

END product_seq_scaf

quality93%