Quelle  subset_algebra.pvs

%------------------------------------------------------------------------------
% Subset Algebra
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------
subset_algebra[T:TYPE, (IMPORTING subset_algebra_def[T])
               S:subset_algebra[T]]: THEORY

BEGIN

  x,y: VAR (S)

  subset_algebra_emptyset:     JUDGEMENT emptyset[T]       HAS_TYPE (S)
  subset_algebra_fullset:      JUDGEMENT fullset[T]        HAS_TYPE (S)
  subset_algebra_complement:   JUDGEMENT complement(x)     HAS_TYPE (S)
  subset_algebra_union:        JUDGEMENT union(x,y)        HAS_TYPE (S)
  subset_algebra_intersection: JUDGEMENT intersection(x,y) HAS_TYPE (S)
  subset_algebra_difference:   JUDGEMENT difference(x,y)   HAS_TYPE (S)

END subset_algebra