Stufen

Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 3 kB

Quelle bags.pvs Sprache: PVS

bags [T: TYPE] : THEORY
%------------------------------------------------------------------------
%
%  Fundamental definitions and properties of bags.
%
%    Authors: Rick Butler      NASA Langley
%             Lee Pike         NASA Langley
%------------------------------------------------------------------------

BEGIN
  x,y,t: VAR T

  bag: TYPE = [T -> nat]
  a,b,c: VAR bag
  n: VAR nat

  count(x,b): nat = b(x)

  emptybag         : bag = (LAMBDA t: 0)

  singleton_bag(t) : bag = (LAMBDA (x: T): IF x = t THEN 1 ELSE 0 ENDIF)

  insert(x,b)      : bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF)

  purge(x,b)       : bag = (LAMBDA t: IF x = t THEN 0 ELSE b(t) ENDIF)

  delete(x,b,n)    : bag = (LAMBDA t: IF x = t THEN
                                        IF b(t) >= n THEN b(t) - n ELSE 0 ENDIF
                                      ELSE b(t) ENDIF)

  extract(x,b)     : bag = (LAMBDA t: IF x = t THEN b(t) ELSE 0 ENDIF)

  plus(a,b)        : bag = (LAMBDA t: a(t) + b(t))

  union(a,b)       : bag = (LAMBDA t: max(a(t),b(t)))

  intersection(a,b): bag = (LAMBDA t: min(a(t),b(t)))

  % --------- some predicates over bags ------------

  member(x,b)        : bool = b(x) > 0

  empty?(b)          : bool = (FORALL x: b(x) = 0)

  nonempty_bag?(b)   : bool = NOT empty?(b)

  eqmult(x,a,b)      : bool = (a(x) = b(x))

  subbag?(a,b)       : bool = (FORALL x: a(x) <= b(x))

  proper_subbag?(a,b): bool = (FORALL x: a(x) < b(x))

  disjoint?(a, b)    : bool = empty?(intersection(a, b))

% ---------- useful lemmas ----------

  emptybag_is_empty?    : LEMMA empty?(b) IFF b = emptybag

  delete_purge          : LEMMA n >= b(x) IMPLIES delete(x,b,n) = purge(x,b)

  insert_unique         : LEMMA insert(x,a) = insert(x,b) IMPLIES a = b

  insert_exchange       : LEMMA insert(x,insert(y,b)) = insert(y,insert(x,b))

  delete_insert         : LEMMA n > 0 IMPLIES
                                  (delete(x,insert(x,b),n) = delete(x,b,n-1))

  insert_delete         : LEMMA b(x) > 0 IMPLIES insert(x,delete(x,b,1)) = b

  delete_insert_diff    : LEMMA x /= y IMPLIES
                            (delete(x,insert(y,b),n) = insert(y,delete(x,b,n)))

  decomposition         : LEMMA NOT empty?(b) IMPLIES
                                  (EXISTS a,x: b = insert(x,a))

  bag_equality          : LEMMA a = b IFF (FORALL x: eqmult(x,a,b))

  subbag_empty          : LEMMA subbag?(emptybag,a)

  subbag_equality       : LEMMA a = b IFF subbag?(a,b) AND subbag?(b,a)

  subbag_trans          : LEMMA subbag?(a,b) AND subbag?(b,c) IMPLIES subbag?(a,c)

% because of empty types the following is not provable -- look into it later
% proper_subbag_rew     : LEMMA proper_subbag?(a,b) IMPLIES subbag?(a,b) AND a /= b

  bag_plus_union        : LEMMA plus(union(a,b),intersection(a,b)) = plus(a,b)

  bag_plus_comm         : LEMMA plus(a,b) = plus(b,a)

  plus_emptybag         : LEMMA plus(emptybag,a) = a

  bag_plus_insert       : LEMMA plus(insert(x,a),b) = insert(x,plus(a,b))

  bag_distributive      : LEMMA intersection(a,union(b,c)) =
                                  union(intersection(a,b),intersection(a,c))

  extract_subbag        : LEMMA subbag?(extract(x,a), a)

  extract_disj          : LEMMA x /= y IMPLIES disjoint?(extract(x,a), extract(y,a))

  bag_disj_comm         : LEMMA disjoint?(a,b) = disjoint?(b,a)

  bag_union_comm        : LEMMA union(a,b) = union(b,a)

  bag_union_fix_pt      : LEMMA union(a,a) = a

  bag_purge_extract       : LEMMA a = union(purge(x,a), extract(x,a))

  bag_disj_extract_perge  : LEMMA disjoint?(extract(x,a), purge(x,a))

  bag_extract_union_subbag: LEMMA x /= y IMPLIES subbag?(union(extract(x,a),extract(y,a)),a)

  union_upper_bound       : LEMMA subbag?(a, c) and subbag?(b, c) IMPLIES
                                    subbag?(union(a, b), c)

END bags

quality72%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.