(java.util.List.of(2L, 3L, 5L, 7L))) {
- if (prime == number) {
+ if ((long) prime == number) {
return true;
}
}
@@ -86,6 +86,43 @@ public static Boolean intsAreUnique(
return true;
}
+ /**
+ * Check whether {@code number} is in {@code numbers}, item by item.
+ *
+ * Java boxes both {@code number} and the items as {@code Long}'s, so that {@code ==}
+ * would compare their references. The test data looks up the numbers beyond -128
+ * and 127 on purpose, as Java caches the boxed values in that range, and
+ * the references would be equal by chance.
+ */
+ public static Boolean containsByLoop(
+ Long number,
+ List numbers) {
+ for (var other : numbers) {
+ if ((long) other == number) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ /**
+ * Check that {@code numbers} are unique by comparing them pair-wise.
+ *
+ * Java boxes the items as {@code Double}'s, so that {@code ==} would compare their
+ * references.
+ */
+ public static Boolean floatsAreUnique(
+ List numbers) {
+ for (int i = 0; i < numbers.size(); i++) {
+ for (int j = i + 1; j < numbers.size(); j++) {
+ if ((double) numbers.get(i) == numbers.get(j)) {
+ return false;
+ }
+ }
+ }
+ return true;
+ }
+
/**
* Check whether {@code text} is one of the separators.
*/
@@ -222,6 +259,20 @@ public Stream transformSomething(
"Some strings must not be separators.")));
}
+ if (!(!containsByLoop(-500L, that.getSomeInts()))) {
+ errorStream = Stream.concat(errorStream,
+ Stream.of(new Reporting.Error(
+ "Invariant violated:\n" +
+ "Some ints must not contain -500.")));
+ }
+
+ if (!floatsAreUnique(that.getSomeFloats())) {
+ errorStream = Stream.concat(errorStream,
+ Stream.of(new Reporting.Error(
+ "Invariant violated:\n" +
+ "Some floats must be unique.")));
+ }
+
return errorStream;
}
}
diff --git a/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/verification.py b/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/verification.py
index a010f8e6e..ce8cf8908 100644
--- a/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/verification.py
+++ b/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/verification.py
@@ -111,6 +111,42 @@ def ints_are_unique(
return True
+def contains_by_loop(
+ number: int,
+ numbers: Sequence[int]
+) -> bool:
+ """
+ Check whether :paramref:`number` is in :paramref:`numbers`, item by item.
+
+ Java boxes both :paramref:`number` and the items as ``Long``'s, so that ``==``
+ would compare their references. The test data looks up the numbers beyond -128
+ and 127 on purpose, as Java caches the boxed values in that range, and
+ the references would be equal by chance.
+ """
+ # pylint: disable=all
+ for other in numbers:
+ if other == number:
+ return True
+ return False
+
+
+def floats_are_unique(
+ numbers: Sequence[float]
+) -> bool:
+ """
+ Check that :paramref:`numbers` are unique by comparing them pair-wise.
+
+ Java boxes the items as ``Double``'s, so that ``==`` would compare their
+ references.
+ """
+ # pylint: disable=all
+ for i in range(0, len(numbers)):
+ for j in range(i + 1, len(numbers)):
+ if numbers[i] == numbers[j]:
+ return False
+ return True
+
+
def is_separator(
text: str
) -> bool:
@@ -232,6 +268,16 @@ def transform_something(
'Some strings must not be separators.'
)
+ if not (not contains_by_loop(-500, that.some_ints)):
+ yield Error(
+ 'Some ints must not contain -500.'
+ )
+
+ if not floats_are_unique(that.some_floats):
+ yield Error(
+ 'Some floats must be unique.'
+ )
+
_TRANSFORMER = _Transformer()
diff --git a/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/verification.ts b/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/verification.ts
index 8ba11fd66..0b220bea2 100644
--- a/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/verification.ts
+++ b/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/verification.ts
@@ -247,6 +247,49 @@ export function intsAreUnique(
return true;
}
+/**
+ * Check whether `number` is in `numbers`, item by item.
+ *
+ * @remarks
+ *
+ * Java boxes both `number` and the items as `Long`'s, so that `==`
+ * would compare their references. The test data looks up the numbers beyond -128
+ * and 127 on purpose, as Java caches the boxed values in that range, and
+ * the references would be equal by chance.
+ */
+export function containsByLoop(
+ number: number,
+ numbers: Array
+): boolean {
+ for (const other of numbers) {
+ if (other == number) {
+ return true;
+ }
+ }
+ return false;
+}
+
+/**
+ * Check that `numbers` are unique by comparing them pair-wise.
+ *
+ * @remarks
+ *
+ * Java boxes the items as `Double`'s, so that `==` would compare their
+ * references.
+ */
+export function floatsAreUnique(
+ numbers: Array
+): boolean {
+ for (let i = 0; i < numbers.length; i++) {
+ for (let j = i + 1; j < numbers.length; j++) {
+ if (OurCommon.at(numbers, i) == OurCommon.at(numbers, j)) {
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
/**
* Check whether `text` is one of the separators.
*/
@@ -392,6 +435,18 @@ class Verifier
"Some strings must not be separators."
)
}
+
+ if (!(!containsByLoop(-500, that.someInts))) {
+ yield new VerificationError(
+ "Some ints must not contain -500."
+ )
+ }
+
+ if (!floatsAreUnique(that.someFloats)) {
+ yield new VerificationError(
+ "Some floats must be unique."
+ )
+ }
}
}
diff --git a/dev/test_data/parse/common_meta_models/list_of_primitives/expected_symbol_table.txt b/dev/test_data/parse/common_meta_models/list_of_primitives/expected_symbol_table.txt
index fe41c321f..52af6aa45 100644
--- a/dev/test_data/parse/common_meta_models/list_of_primitives/expected_symbol_table.txt
+++ b/dev/test_data/parse/common_meta_models/list_of_primitives/expected_symbol_table.txt
@@ -370,6 +370,39 @@ UnverifiedSymbolTable(
original_node=...),
original_node=...),
original_node=...)"""),
+ node=...),
+ Invariant(
+ description='Some ints must not contain -500.',
+ body=textwrap.dedent("""\
+ Not(
+ operand=FunctionCall(
+ name='contains_by_loop',
+ args=[
+ Constant(
+ value=-500,
+ original_node=...),
+ Member(
+ instance=Name(
+ identifier='self',
+ original_node=...),
+ name='some_ints',
+ original_node=...)],
+ original_node=...),
+ original_node=...)"""),
+ node=...),
+ Invariant(
+ description='Some floats must be unique.',
+ body=textwrap.dedent("""\
+ FunctionCall(
+ name='floats_are_unique',
+ args=[
+ Member(
+ instance=Name(
+ identifier='self',
+ original_node=...),
+ name='some_floats',
+ original_node=...)],
+ original_node=...)"""),
node=...)],
serialization=None,
description=None,
@@ -741,6 +774,191 @@ UnverifiedSymbolTable(
original_node=...)""")],
node=...,
arguments_by_name=...),
+ UnderstoodMethod(
+ name='contains_by_loop',
+ verification=True,
+ visibility='PUBLIC',
+ arguments=[
+ Argument(
+ name='number',
+ type_annotation=AtomicTypeAnnotation(
+ identifier='int',
+ node=...),
+ default=None,
+ node=...),
+ Argument(
+ name='numbers',
+ type_annotation=SubscriptedTypeAnnotation(
+ identifier='Sequence',
+ subscripts=[
+ AtomicTypeAnnotation(
+ identifier='int',
+ node=...)],
+ node=...),
+ default=None,
+ node=...)],
+ returns=AtomicTypeAnnotation(
+ identifier='bool',
+ node=...),
+ description=Description(
+ document=...,
+ node=...),
+ contracts=Contracts(
+ preconditions=[],
+ snapshots=[],
+ postconditions=[]),
+ non_mutating=False,
+ body=[
+ textwrap.dedent("""\
+ For(
+ generator=ForEach(
+ variable=Name(
+ identifier='other',
+ original_node=...),
+ iteration=Name(
+ identifier='numbers',
+ original_node=...),
+ original_node=...),
+ body=[
+ If(
+ branches=[
+ IfBranch(
+ condition=Comparison(
+ left=Name(
+ identifier='other',
+ original_node=...),
+ op='EQ',
+ right=Name(
+ identifier='number',
+ original_node=...),
+ original_node=...),
+ body=[
+ Return(
+ value=Constant(
+ value=True,
+ original_node=...),
+ original_node=...)],
+ original_node=...)],
+ default=None,
+ original_node=...)],
+ original_node=...)"""),
+ textwrap.dedent("""\
+ Return(
+ value=Constant(
+ value=False,
+ original_node=...),
+ original_node=...)""")],
+ node=...,
+ arguments_by_name=...),
+ UnderstoodMethod(
+ name='floats_are_unique',
+ verification=True,
+ visibility='PUBLIC',
+ arguments=[
+ Argument(
+ name='numbers',
+ type_annotation=SubscriptedTypeAnnotation(
+ identifier='Sequence',
+ subscripts=[
+ AtomicTypeAnnotation(
+ identifier='float',
+ node=...)],
+ node=...),
+ default=None,
+ node=...)],
+ returns=AtomicTypeAnnotation(
+ identifier='bool',
+ node=...),
+ description=Description(
+ document=...,
+ node=...),
+ contracts=Contracts(
+ preconditions=[],
+ snapshots=[],
+ postconditions=[]),
+ non_mutating=False,
+ body=[
+ textwrap.dedent("""\
+ For(
+ generator=ForRange(
+ variable=Name(
+ identifier='i',
+ original_node=...),
+ start=Constant(
+ value=0,
+ original_node=...),
+ end=FunctionCall(
+ name='len',
+ args=[
+ Name(
+ identifier='numbers',
+ original_node=...)],
+ original_node=...),
+ original_node=...),
+ body=[
+ For(
+ generator=ForRange(
+ variable=Name(
+ identifier='j',
+ original_node=...),
+ start=Add(
+ left=Name(
+ identifier='i',
+ original_node=...),
+ right=Constant(
+ value=1,
+ original_node=...),
+ original_node=...),
+ end=FunctionCall(
+ name='len',
+ args=[
+ Name(
+ identifier='numbers',
+ original_node=...)],
+ original_node=...),
+ original_node=...),
+ body=[
+ If(
+ branches=[
+ IfBranch(
+ condition=Comparison(
+ left=Index(
+ collection=Name(
+ identifier='numbers',
+ original_node=...),
+ index=Name(
+ identifier='i',
+ original_node=...),
+ original_node=...),
+ op='EQ',
+ right=Index(
+ collection=Name(
+ identifier='numbers',
+ original_node=...),
+ index=Name(
+ identifier='j',
+ original_node=...),
+ original_node=...),
+ original_node=...),
+ body=[
+ Return(
+ value=Constant(
+ value=False,
+ original_node=...),
+ original_node=...)],
+ original_node=...)],
+ default=None,
+ original_node=...)],
+ original_node=...)],
+ original_node=...)"""),
+ textwrap.dedent("""\
+ Return(
+ value=Constant(
+ value=True,
+ original_node=...),
+ original_node=...)""")],
+ node=...,
+ arguments_by_name=...),
UnderstoodMethod(
name='is_separator',
verification=True,