| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/VDM/VDMSL/ProgLangSL/ (Wiener Entwicklungsmethode ©) |
|
Quelle finite_bags_aux.pvs Sprache: PVS |
|||||||||
|
finite_bags_aux[T: TYPE]: THEORY
%------------------------------------------------------------------------- % % Additional properties of finite bags. % % Author: David Griffioen (CWI Amsterdam and KUN) % %------------------------------------------------------------------------- BEGIN IMPORTING finite_bags[T], bags_aux[T] x,e: VAR T b: VAR finite_bag p: VAR pred[T] n,xn: VAR nat finite_bag_rest: LEMMA is_finite(rest[T](b)) JUDGEMENT rest(b) HAS_TYPE finite_bag card_bag_rest : LEMMA nonempty_bag?(b) IMPLIES card(b) = card(rest(b)) + 1 %% ===== on finite bags and filters ===== finite_filter : THEOREM is_finite(filter(b,p)) JUDGEMENT filter(b,p) HAS_TYPE finite_bag card_filter_insert: LEMMA card(filter(insert(x,b),p)) = card(filter(b,p)) + IF p(x) THEN 1 ELSE 0 ENDIF card_filter_delete: LEMMA card(filter(delete(x,b,n),p)) = card(filter(b,p)) - IF p(x) THEN min(b(x),n) ELSE 0 ENDIF END finite_bags_aux ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
