| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 775 B |
|
Quellcode-Bibliothek finite_bags_minmax.pvs Sprache: PVS |
|||||||||
|
%----------------------------------------------------------------------------
% Lee Pike % lee.s.pike@nasa.gov % Formal Methods Group, NASA Langley Research Center % % PVS Version 3.1 % % PURPOSE: % Define the minimum and maximum for ordered finite bags. %---------------------------------------------------------------------------- finite_bags_minmax[T: NONEMPTY_TYPE, leq: (total_order?[T])]: THEORY BEGIN IMPORTING finite_bags[T], finite_sets@finite_sets_minmax[T, leq], finite_bags_inductions[T] D : VAR nonempty_finite_bag max(D) : T = max(bag_to_set(D)) min(D) : T = min(bag_to_set(D)) max_member : LEMMA member(max(D), D) min_member : LEMMA member(min(D), D) END finite_bags_minmax ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.11Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28