products/sources/formale sprachen/PVS/structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: PVS

Original von: PVS©
seq2set[T: TYPE]: THEORY
%----------------------------------------------------------------------------
%
% Utility functions for converting to/from sets and sequences
%
% Version 1.0, January, 2004
% Author: Kristin Y. Rozier
%----------------------------------------------------------------------------
BEGIN

   IMPORTING seqs[T]

   fs: VAR finite_sequence[T]

   seq2set(fs): finite_set[T] 
   = {s: T | (EXISTS (kk: below(length(fs))): fs(kk) = s)}

   seq2set_lem: LEMMA (FORALL (ii: below(length(fs))): seq2set(fs)(fs(ii)))

   card_seq2set: LEMMA card[T](seq2set(fs)) <= length(fs)

   ss: VAR ne_seqs  % length > 0

   JUDGEMENT seq2set(ss) HAS_TYPE (nonempty?[T]) 

END seq2set

minmax_seq2set[T: TYPE+, <= : (total_order?[T]) ]: THEORY
BEGIN

   IMPORTING sort_seq_lems[T,<=],
             finite_sets@finite_sets_minmax[T,<=],
             seq2set[T]

   ne_fs: VAR ne_seqs[T]

   minmax_seq2set: LEMMA min[T,<=](seq2set(ne_fs)) = min(ne_fs) AND
                         max[T,<=](seq2set(ne_fs)) = max(ne_fs)

END minmax_seq2set

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

Eigene Datei ansehen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff