SSL base_repr.pvs Interaktion und
PortierbarkeitPVS

base_repr : THEORY

%------------------------------------------------------------
%
%   Base n representation of natural numbers.
%
%   Given n>1, the base n representation of k>=0 is
%   k = (a_0, a_1, a_2, ...) where 0<=a_i<n
%
%   k = sum_{i=0}^\infty a_i*n^i.
%
%
%
%   Author: Aaron Dutle, NASA Langley Research Center
%
%
%
%------------------------------------------------------------

  BEGIN

  IMPORTING log_nat, sigma_nat, structures@array2list

  base_n(n: {x:nat| x>1}, k:nat)(i:nat): RECURSIVE nat =
                       IF k<n THEN (IF i = 0 THEN k ELSE 0 ENDIF)
         ELSE (IF i=0 THEN mod(k, n)  ELSE base_n(n, (k-mod(k,n))/n)(i-1) ENDIF)
         ENDIF
         MEASURE k

  %base_n_lt_n: LEMMA
  %    FORALL (n: {x:nat| x>1}, k,i:nat):
  %    base_n(n,k)(i)<=n-1

  upper_index(n: {x:nat| x>1}, k:nat): nat = IF k=0 THEN 0 ELSE log_nat(k,n)`1 ENDIF

  base_n_lt_n: LEMMA FORALL (n:{x:nat|x>1},k,i:nat):
    base_n(n,k)(i)<n

  upper_is_bound: LEMMA FORALL (n: {x:nat|x>1}, k:nat, m:nat):
        m>upper_index(n, k) IMPLIES base_n(n,k)(m) = 0

  base_n_is_n: LEMMA FORALL(n:{x:nat|x>1}, k:nat):
        k = sigma(0, upper_index(n,k), LAMBDA(s:nat): n^s*base_n(n,k)(s))

  base_n_to_nat(n:{x:nat|x>1},F:[nat->nat], m:nat): nat = sigma(0, m, LAMBDA(s:nat): n^s*F(s))

  base_n_is_n_alt: LEMMA FORALL (n: {x:nat|x>1}, k, m:nat):
        k<n^(m+1) IMPLIES  k = base_n_to_nat(n,base_n(n,k),m)

  base_n_to_nat_lt: LEMMA FORALL (F:[nat->nat],m:nat,(n:nat|n>1)):
    (FORALL (i:nat): i<=m IMPLIES F(i)<n) IMPLIES base_n_to_nat(n,F,m) < n^(m+1)

  base_n_0: LEMMA FORALL (n: {x:nat|x>1}, k:nat, m:nat):
        k<n^m IMPLIES base_n(n,k)(m) = 0

  base_n_unique: LEMMA FORALL (d:nat,n:{x:nat|x>1},numseq:[nat->below(n)]):
    LET k = sigma(0,d,LAMBDA (s:nat): n^s*numseq(s)) IN
      (FORALL (j:nat): j<=d IMPLIES numseq(j)=base_n(n,k)(j))

  base_n_base_n_to_nat: LEMMA FORALL (n:{x:nat|x>1},F:[nat->nat], m:nat):
    (FORALL (i:upto(m)): F(i)<n)
    IMPLIES
    FORALL (i:upto(m)): base_n(n,base_n_to_nat(n,F,m))(i) = F(i)

  base_n_to_nat_eq: LEMMA FORALL (n: {x:nat|x>1}, k, m:nat,F,G:[nat->nat]):
    (FORALL (i:upto(m)): F(i)=G(i)) IMPLIES
    base_n_to_nat(n,F,m) = base_n_to_nat(n,G,m)

  base_n_to_nat_unique: LEMMA FORALL (n: {x:nat|x>1}, k, m:nat,F,G:[nat->nat]):
    (FORALL (i:upto(m)): F(i)<n AND G(i)<n) AND
    base_n_to_nat(n,F,m) = base_n_to_nat(n,G,m)
    IMPLIES
    (FORALL (i:upto(m)): F(i)=G(i))

  base_list(n: {x:nat|x>1},k:nat):
    listn[below(n)](upper_index(n,k)+1) =
     array2list[below(n)](upper_index(n,k)+1)( base_n(n,k))

  base_list(n: {x:nat|x>1}, k:nat, digits:posnat):
     listn[below(n)](digits) = array2list[below(n)](digits)(base_n(n,k))

  base_list_cdr: LEMMA FORALL (n: {x:nat|x>1}, k:nat, j:posnat):
          cdr(base_list(n,k,j+1)) = base_list(n, (k-mod(k,n))/n, j)

  base_list_faster(n: {x:nat|x>1}, k:nat, digits:posnat): RECURSIVE listn[below(n)](digits) =
    IF digits = 1 THEN (: mod(k, n) :)
    ELSE cons(mod(k, n), base_list_faster(n, (k-mod(k, n))/n, digits-1))
    ENDIF
    MEASURE digits

  base_list_same: LEMMA FORALL (n: {x:nat|x>1}, k:nat, digits:posnat):
       base_list_faster(n, k, digits) = base_list(n,k,digits)

  base_to_array(n:posnat, l:list[below(n)]): [nat->below(n)] = list2array[below(n)](0)(l)

  base_to_array_sound: LEMMA FORALL (n:{x:nat|x>1}, k:nat, j:above(upper_index(n,k))):
       base_to_array(n, base_list(n, k, j)) = base_n(n,k)

  END base_repr

quality36%

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

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

SSL base_repr.pvs Interaktion und PortierbarkeitPVS

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

Haftungshinweis

Bemerkung:

SSL base_repr.pvs Interaktion und
PortierbarkeitPVS