Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit 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/co_structures/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 3 kB

Quelle csequence_extract.pvs Sprache: PVS

%-----------------------------------------------------------------------------
% Extraction of contiguous subsequences of a sequence of countable length.
%
% Author: Jerry James <loganjerry@gmail.com>
%
% This file and its accompanying proof file are distributed under the CC0 1.0
% Universal license: http://creativecommons.org/publicdomain/zero/1.0/.
%
% Version history:
%   2007 Feb 14: PVS 4.0 version
%   2011 May  6: PVS 5.0 version
%   2013 Jan 14: PVS 6.0 version
%-----------------------------------------------------------------------------
csequence_extract[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence_nth[T]
  IMPORTING csequence_add[T]  % Proofs only

  t: VAR T
  p: VAR pred[T]
  index, n, m: VAR nat
  range, range2: VAR [nat, nat]
  cseq, cseq1, cseq2: VAR csequence
  fseq: VAR finite_csequence
  nfseq: VAR nonempty_finite_csequence

  ^(cseq, range): RECURSIVE finite_csequence =
    LET (m, n) = range IN
      IF empty?(cseq) OR m > n THEN empty_cseq
      ELSIF m > 0 THEN rest(cseq) ^ (m - 1, n - 1)
      ELSE add(first(cseq),
               IF n = 0 THEN empty_cseq ELSE rest(cseq) ^ (m, n - 1) ENDIF)
      ENDIF
     MEASURE range`2

  extract_empty: THEOREM
    FORALL cseq, range:
      empty?(cseq ^ range) IFF
       range`1 > range`2 OR (is_finite(cseq) AND NOT index?(cseq)(range`1))

  extract_nonempty: COROLLARY
    FORALL cseq, range:
      nonempty?(cseq ^ range) IFF
       range`1 <= range`2 AND (is_infinite(cseq) OR index?(cseq)(range`1))

  extract_length: THEOREM
    FORALL cseq, range:
      length(cseq ^ range) =
       IF (range`1 > range`2 OR (is_finite(cseq) AND range`1 >= length(cseq)))
         THEN 0
       ELSIF is_finite(cseq) AND range`2 >= length(cseq)
         THEN length(cseq) - range`1
       ELSE range`2 - range`1 + 1
       ENDIF

  extract_def: THEOREM
    FORALL nfseq, n: n >= length(nfseq) - 1 IMPLIES nfseq ^ (0, n) = nfseq

  extract_rest: THEOREM
    FORALL nfseq: nfseq ^ (1, length(nfseq) - 1) = rest(nfseq)

  extract_rest2: THEOREM
    FORALL cseq, m, n:
      nonempty?(cseq ^ (m, n)) IMPLIES
       rest(cseq ^ (m, n)) = cseq ^ (m + 1, n)

  extract_extract: THEOREM
    FORALL cseq, range, range2:
      (cseq ^ range) ^ range2 =
       cseq ^ (range`1 + range2`1, min(range`2, range`1 + range2`2))

  extract_index: THEOREM
    FORALL cseq, m, n, index:
      index?(cseq ^ (m, n))(index) IFF
       m + index <= n AND index?(cseq)(m + index)

  extract_first: THEOREM
    FORALL cseq, m, n:
      nonempty?(cseq ^ (m, n)) IMPLIES first(cseq ^ (m, n)) = nth(cseq, m)

  extract_nth: THEOREM
    FORALL cseq, (m: indexes(cseq)), (n: nat), (i: indexes(cseq ^ (m, n))):
      nth(cseq ^ (m, n), i) = nth(cseq, m + i)

  extract_add: THEOREM
    FORALL cseq, t, m, n:
      add(t, cseq) ^ (m, n) =
       IF m > n THEN empty_cseq
       ELSIF m > 0 THEN cseq ^ (m - 1, max(0, n - 1))
       ELSIF n > 0 THEN add(t, cseq ^ (m, n - 1))
       ELSE add(t, empty_cseq)
       ENDIF

  extract_last: THEOREM
    FORALL cseq, m, n:
      nonempty?(cseq ^ (m, n)) IMPLIES
       last(cseq ^ (m, n)) =
        IF index?(cseq)(n) THEN nth(cseq, n) ELSE last(cseq) ENDIF

  extract_extensionality: THEOREM
    FORALL cseq1, cseq2:
      (FORALL range: cseq1 ^ range = cseq2 ^ range) IMPLIES cseq1 = cseq2

  extract_some: THEOREM
    FORALL cseq, m, n, p:
      some(p)(cseq ^ (m, n)) IFF
       (EXISTS index:
          m <= index AND
           index <= n AND index?(cseq)(index) AND p(nth(cseq, index)))

  extract_every: THEOREM
    FORALL cseq, m, n, p:
      every(p)(cseq ^ (m, n)) IFF
       (FORALL index:
          m <= index AND index <= n AND index?(cseq)(index) IMPLIES
           p(nth(cseq, index)))

END csequence_extract

quality88%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.