| products/Sources/formale Sprachen/VDM/VDMPP/KLVPP/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: csequence_finseq.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%-----------------------------------------------------------------------------
% Conversions between sequences of countable length defined as coalgebraic % datatypes and the prelude finseq type. % % 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_finseq[T: TYPE]: THEORY BEGIN IMPORTING finite_sequences[T], csequence_nth[T] n: VAR nat fs: VAR finseq fseq: VAR finite_csequence % Convert a finseq to a finite_csequence from_finseq(fs): RECURSIVE finite_csequence = IF fs`length = 0 THEN empty_cseq ELSE add(fs`seq(0), from_finseq((# length := fs`length - 1, seq := LAMBDA (x: below[fs`length - 1]): fs`seq(x + 1) #))) ENDIF MEASURE fs`length from_finseq_length: THEOREM FORALL fs: length(from_finseq(fs)) = fs`length from_finseq_index: THEOREM FORALL fs, n: index?(from_finseq(fs))(n) IFF n < fs`length from_finseq_nth: THEOREM FORALL fs, (n: below[fs`length]): nth(from_finseq(fs), n) = fs`seq(n) % Convert a finite_csequence to a finseq to_finseq(fseq): finseq = (# length := length(fseq), seq := LAMBDA (x: below[length(fseq)]): nth(fseq, x) #) to_finseq_length: THEOREM FORALL fseq: to_finseq(fseq)`length = length(fseq) to_finseq_index: THEOREM FORALL fseq, n: n < to_finseq(fseq)`length IFF index?(fseq)(n) to_finseq_nth: THEOREM FORALL fseq, (n: indexes(fseq)): to_finseq(fseq)`seq(n) = nth(fseq, n) % Applying both conversions gives you back what you started with to_from_finseq: THEOREM FORALL fs: to_finseq(from_finseq(fs)) = fs from_to_finseq: THEOREM FORALL fseq: from_finseq(to_finseq(fseq)) = fseq END csequence_finseq ¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
