products/sources/formale Sprachen/PVS/co_structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: digest.bat   Sprache: PVS

Untersuchung PVS©
%-----------------------------------------------------------------------------
% The combination of the zip and unzip operators on sequences of countable
% length.
%
% Author: Jerry James <[email protected]>
%
% 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_zip_unzip[T1, T2: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_unzip[T1, T2], csequence_zip[T1, T2]

  cseq: VAR csequence[[T1, T2]]
  cseq1: VAR csequence[T1]
  cseq2: VAR csequence[T2]

  zip_unzip_eta: THEOREM FORALL cseq: zip(unzip(cseq)) = cseq

  unzip_zip_eta: THEOREM
    FORALL cseq1, cseq2:
      length_eq(cseq1, cseq2) IMPLIES
       unzip(zip(cseq1, cseq2)) = (cseq1, cseq2)

 END csequence_zip_unzip

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



Druckansicht
unsichere Verbindung
Druckansicht
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