Quelle  group_test.pvs

%------------------------------------------------------------------------------
% Example groups
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

group_test: THEORY

  BEGIN

  IMPORTING abelian_group

  integer_plus:      abelian_group[int,+,0]    = fullset[int]
  nz_rational_mult:  abelian_group[nzrat,*,1]  = fullset[nzrat]
  pos_rational_mult: abelian_group[posrat,*,1] = fullset[posrat]

  END group_test