|
@@ -1361,7 +1361,95 @@ positive: long integers as set elements
|
|
|
first := MIN (SET) + 2; last := first + 1; set := {first .. last}; ASSERT (set = {first, last});
|
|
|
first := MIN (SET) + 2; last := first - 1; set := {first .. last}; ASSERT (set = {});
|
|
|
END Test.
|
|
|
-
|
|
|
+
|
|
|
+positive: huge integer as set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN
|
|
|
+ element := MIN (SET); set := {element}; ASSERT (element IN set); ASSERT (set - {element} = {});
|
|
|
+ element := MAX (SET); set := {element}; ASSERT (element IN set); ASSERT (set - {element} = {});
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: huge integer as too small set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN element := MIN (SET) - 1; set := {element};
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: huge integer as too large set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN element := MAX (SET) + 1; set := {element};
|
|
|
+ END Test.
|
|
|
+
|
|
|
+positive: huge integer as first set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN
|
|
|
+ element := MIN (SET); set := {element .. MAX (SET)}; ASSERT (element IN set); ASSERT (set = {MIN (SET) .. MAX (SET)}); ASSERT (-set = {});
|
|
|
+ element := MIN (SET); set := {element .. MIN (SET)}; ASSERT (element IN set); ASSERT (set = {MIN (SET) .. MIN (SET)}); ASSERT (set = {element}); ASSERT (set = {MIN (SET)});
|
|
|
+ element := MIN (SET) + 2; set := {element .. MAX (SET)}; ASSERT (element IN set); ASSERT (set = {MIN (SET) + 2 .. MAX (SET)}); ASSERT (-set = {MIN (SET), MIN (SET) + 1});
|
|
|
+ element := MIN (SET) + 2; set := {element .. MIN (SET)}; ASSERT (~(element IN set)); ASSERT (set = {element .. MIN (SET)}); ASSERT (set = {});
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: huge integer as too small first set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN element := MIN (SET) - 1;set := {element .. MAX (SET)};
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: huge integer as too large first set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN element := MAX (SET) + 1;set := {element .. MAX (SET)};
|
|
|
+ END Test.
|
|
|
+
|
|
|
+positive: huge integer as last set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN
|
|
|
+ element := MAX (SET); set := {MIN (SET) .. element}; ASSERT (element IN set); ASSERT (set = {MIN (SET) .. MAX (SET)}); ASSERT (-set = {});
|
|
|
+ element := MAX (SET); set := {MAX (SET) .. element}; ASSERT (element IN set); ASSERT (set = {MAX (SET) .. MAX (SET)}); ASSERT (set = {MAX (SET)});
|
|
|
+ element := MAX (SET) - 2; set := {MIN (SET) .. element}; ASSERT (element IN set); ASSERT (set = {MIN (SET) .. MAX (SET) - 2}); ASSERT (-set = {MAX (SET) - 1, MAX (SET)});
|
|
|
+ element := MAX (SET) - 2; set := {MAX (SET).. element}; ASSERT (~(element IN set)); ASSERT (set = {MAX (SET) .. element}); ASSERT (set = {});
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: huge integer as too small last set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN element := MIN (SET) - 1;set := {MIN (SET) .. element};
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: huge integer as too large last set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR element: HUGEINT; set: SET;
|
|
|
+ BEGIN element := MAX (SET) + 1;set := {MIN (SET) .. element};
|
|
|
+ END Test.
|
|
|
+
|
|
|
+positive: huge integers as set elements
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR first, last: HUGEINT; set: SET;
|
|
|
+ BEGIN
|
|
|
+ first := MIN (SET); last := MAX (SET); set := {first .. last}; ASSERT (set = {MIN (SET) .. MAX (SET)});
|
|
|
+ ASSERT (first IN set); ASSERT (last IN set); ASSERT (-set = {});
|
|
|
+ first := MIN (SET) + 2; last := MAX (SET) - 2; set := {first .. last}; ASSERT (set = {MIN (SET) + 2 .. MAX (SET) - 2});
|
|
|
+ ASSERT (first IN set); ASSERT (last IN set); ASSERT (-set = {MIN (SET), MIN (SET) + 1, MAX (SET) - 1, MAX (SET)});
|
|
|
+ first := MIN (SET) + 2; last := first; set := {first .. last}; ASSERT (set = {first});
|
|
|
+ first := MIN (SET) + 2; last := first + 1; set := {first .. last}; ASSERT (set = {first, last});
|
|
|
+ first := MIN (SET) + 2; last := first - 1; set := {first .. last}; ASSERT (set = {});
|
|
|
+ END Test.
|
|
|
+
|
|
|
+
|
|
|
# odd test
|
|
|
|
|
|
positive: odd test on short integer
|
|
@@ -5457,7 +5545,30 @@ negative: include statement with too large long integer as set element
|
|
|
BEGIN set := {}; element := MAX (SET) + 1; INCL (set, element);
|
|
|
END Test.
|
|
|
|
|
|
+positive: include statement with huge integer as set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR set: SET; element: HUGEINT;
|
|
|
+ BEGIN
|
|
|
+ set := {}; element := MIN (SET); INCL (set, element); ASSERT (set = {element}); ASSERT (set = {MIN (SET)}); ASSERT (element IN set);
|
|
|
+ set := {}; element := MAX (SET); INCL (set, element); ASSERT (set = {element}); ASSERT (set = {MAX (SET)}); ASSERT (element IN set);
|
|
|
+ element := MIN (SET); set := {element}; INCL (set, element); ASSERT (set = {element}); ASSERT (set = {MIN (SET)}); ASSERT (element IN set);
|
|
|
+ element := MAX (SET); set := {element}; INCL (set, element); ASSERT (set = {element}); ASSERT (set = {MAX (SET)}); ASSERT (element IN set);
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: include statement with too small huge integer as set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR set: SET; element: HUGEINT;
|
|
|
+ BEGIN set := {}; element := MIN (SET) - 1; INCL (set, element);
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: include statement with too large huge integer as set element
|
|
|
|
|
|
+ MODULE Test;
|
|
|
+ VAR set: SET; element: HUGEINT;
|
|
|
+ BEGIN set := {}; element := MAX (SET) + 1; INCL (set, element);
|
|
|
+ END Test.
|
|
|
|
|
|
|
|
|
# exclude statement
|
|
@@ -5537,6 +5648,31 @@ negative: exclude statement with too large long integer as set element
|
|
|
BEGIN set := {}; element := MAX (SET) + 1; EXCL (set, element);
|
|
|
END Test.
|
|
|
|
|
|
+positive: exclude statement with huge integer as set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR set: SET; element: HUGEINT;
|
|
|
+ BEGIN
|
|
|
+ set := {}; element := MIN (SET); EXCL (set, element); ASSERT (set = {}); ASSERT (~(element IN set));
|
|
|
+ set := {}; element := MAX (SET); EXCL (set, element); ASSERT (set = {}); ASSERT (~(element IN set));
|
|
|
+ element := MIN (SET); set := {element}; EXCL (set, element); ASSERT (set = {}); ASSERT (~(element IN set));
|
|
|
+ element := MAX (SET); set := {element}; EXCL (set, element); ASSERT (set = {}); ASSERT (~(element IN set));
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: exclude statement with too small huge integer as set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR set: SET; element: HUGEINT;
|
|
|
+ BEGIN set := {}; element := MIN (SET) - 1; EXCL (set, element);
|
|
|
+ END Test.
|
|
|
+
|
|
|
+negative: exclude statement with too large huge integer as set element
|
|
|
+
|
|
|
+ MODULE Test;
|
|
|
+ VAR set: SET; element: HUGEINT;
|
|
|
+ BEGIN set := {}; element := MAX (SET) + 1; EXCL (set, element);
|
|
|
+ END Test.
|
|
|
+
|
|
|
|
|
|
# await statement
|
|
|
|