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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: PVS

Untersuchung 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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot  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