/[eiffelstudio]/branches/eth/eve/Src/framework/eiffel2boogie/tests/sets/sets.e
ViewVC logotype

Contents of /branches/eth/eve/Src/framework/eiffel2boogie/tests/sets/sets.e

Parent Directory Parent Directory | Revision Log Revision Log


Revision 92762 - (show annotations)
Mon Jul 1 16:00:14 2013 UTC (6 years, 3 months ago) by polikarn
File size: 534 byte(s)
Added some tests for MML_SET features
1 class SETS
2
3 feature
4
5 good (s: MML_SET[INTEGER])
6 local
7 s1, s2: MML_SET[INTEGER]
8 do
9 check s1.is_empty end
10 s1 := s & 1 & 2
11 check s1.has (1) end
12 s2 := s1 / 2
13 check s2 <= s1 end
14 check s1 >= s2 end
15 check (s1 * s2).has(1) end
16 check (s1 - s2).is_disjoint(s2 - s1) end
17 check s1 <= s1 + s2 end
18 end
19
20 bad (s: MML_SET[INTEGER])
21 local
22 s1: MML_SET[INTEGER]
23 do
24 s1 := s1 & 1;
25 check bad_disjoint: s.is_disjoint (s1) end
26 check bad_empty: s.is_empty end
27 check bad_has: s.has (1) end
28 end
29
30 end

Properties

Name Value
svn:eol-style native
svn:keywords Author Date ID Revision

  ViewVC Help
Powered by ViewVC 1.1.23