|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Env.vdmpp
Sprache: PVS
Original 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.32 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
