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_insert.pvs Sprache: PVS

%-----------------------------------------------------------------------------
% Insert an element into a sequence of countable length defined as a
% coalgebraic datatype.
%
% 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_insert[T: TYPE]: THEORY
BEGIN

  IMPORTING csequence_nth[T]

  t, u: VAR T
  p: VAR pred[T]
  index, n, m: VAR nat
  cseq, cseq1, cseq2: VAR csequence
  fseq: VAR finite_csequence
  iseq: VAR infinite_csequence

  % Insert t at position index in sequence cseq.  If index is greater than
  % length(cseq), then t is appended instead.
  insert(t, index, cseq): RECURSIVE nonempty_csequence =
    IF index = 0 OR empty?(cseq) THEN add(t, cseq)
    ELSE add(first(cseq), insert(t, index - 1, rest(cseq)))
    ENDIF
     MEASURE index

  insert_finite: JUDGEMENT
    insert(t, index, fseq) HAS_TYPE nonempty_finite_csequence

  insert_infinite: JUDGEMENT
    insert(t, index, iseq) HAS_TYPE infinite_csequence

  insert_first: THEOREM
    FORALL t, index, cseq:
      first(insert(t, index, cseq)) =
       IF index = 0 OR empty?(cseq) THEN t ELSE first(cseq) ENDIF

  insert_rest: THEOREM
    FORALL t, index, cseq:
      rest(insert(t, index, cseq)) =
       IF index = 0 OR empty?(cseq) THEN cseq
       ELSE insert(t, index - 1, rest(cseq))
       ENDIF

  insert_length: THEOREM
    FORALL fseq, t, index: length(insert(t, index, fseq)) = length(fseq) + 1

  insert_index: THEOREM
    FORALL t, index, cseq, n:
      index?(insert(t, index, cseq))(n) IFF n = 0 OR index?(cseq)(n - 1)

  insert_nth: THEOREM
    FORALL cseq, t, index, (n: indexes(cseq)):
      nth(cseq, n) =
       nth(insert(t, index, cseq), n + IF n < index THEN 0 ELSE 1 ENDIF)

  insert_0: THEOREM FORALL t, cseq: insert(t, 0, cseq) = add(t, cseq)

  insert_add: THEOREM
    FORALL t, u, index, cseq:
      add(u, insert(t, index, cseq)) = insert(t, index + 1, add(u, cseq))

  insert_last: THEOREM
    FORALL t, index, fseq:
      last(insert(t, index, fseq)) =
       IF index?(fseq)(index) THEN last(fseq) ELSE t ENDIF

  insert_beyond: THEOREM
    FORALL t, index, fseq:
      index > length(fseq) IMPLIES
       insert(t, index, fseq) = insert(t, length(fseq), fseq)

  insert_insert: THEOREM
    FORALL t, u, n, m, cseq:
      insert(t, n, insert(u, m, cseq)) =
       IF is_finite(cseq) AND n > length(cseq) AND m > length(cseq)
         THEN insert(u, length(cseq), insert(t, n, cseq))
       ELSIF n <= m THEN insert(u, m + 1, insert(t, n, cseq))
       ELSE insert(u, m, insert(t, n - 1, cseq))
       ENDIF

  insert_extensionality: THEOREM
    FORALL t, index, cseq1, cseq2:
      insert(t, index, cseq1) = insert(t, index, cseq2) IMPLIES
       cseq1 = cseq2

  insert_some: THEOREM
    FORALL t, index, cseq:
      some(p)(insert(t, index, cseq)) IFF p(t) OR some(p)(cseq)

  insert_every: THEOREM
    FORALL t, index, cseq:
      every(p)(insert(t, index, cseq)) IFF p(t) AND every(p)(cseq)

END csequence_insert

quality65%

¤ Dauer der Verarbeitung: 0.16 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.