diff --git a/aas_core_codegen/cpp/transpilation.py b/aas_core_codegen/cpp/transpilation.py index f41d3894b..f6d12662b 100644 --- a/aas_core_codegen/cpp/transpilation.py +++ b/aas_core_codegen/cpp/transpilation.py @@ -1154,6 +1154,30 @@ def transform_is_in( f"Please contact the developers if you need this feature.", ) + # NOTE (mristin): + # The membership in a string is a check for a sub-string, while + # ``common::Contains`` would look for a single character. + if ( + intermediate_type_inference.try_primitive_type(container_type) + is intermediate_type_inference.PrimitiveType.STR + ): + if not isinstance(node.container, parse_tree.Name): + container = Stripped(f"({container})") + + one_liner = f"{container}.find({member}) != std::wstring::npos" + if "\n" not in one_liner and len(one_liner) <= 60: + return Stripped(one_liner), None + + return ( + Stripped( + f"""\ +{container}.find( +{I}{indent_but_first_line(member, I)} +) != std::wstring::npos""" + ), + None, + ) + # NOTE (mristin): # We look up the member in a set in constant time, while # ``common::Contains`` iterates over all the items. @@ -1177,6 +1201,12 @@ def transform_is_in( None, ) + # NOTE (mristin): + # The lengths are ``size_t``'s, so we convert them to our integers to avoid + # comparing the signed and the unsigned integers in ``std::find``. + if isinstance(container_type, intermediate_type_inference.ListTypeAnnotation): + member = self._as_int64_position(node.member, member) + contains_function = cpp_naming.function_name(Identifier("contains")) return ( diff --git a/aas_core_codegen/golang/lib/_generate_common.py b/aas_core_codegen/golang/lib/_generate_common.py index ad3f9fcb2..98f7b0837 100644 --- a/aas_core_codegen/golang/lib/_generate_common.py +++ b/aas_core_codegen/golang/lib/_generate_common.py @@ -366,6 +366,22 @@ def generate(symbol_table: intermediate.SymbolTable) -> str: func MapContains[K comparable, V any](m map[K]V, k K) bool {{ {I}_, ok := m[k] {I}return ok +}}""" + ), + Stripped( + f"""\ +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool {{ +{I}for _, item := range s {{ +{II}if any(item) == any(v) {{ +{III}return true +{II}}} +{I}}} +{I}return false }}""" ), Stripped( diff --git a/aas_core_codegen/golang/transpilation.py b/aas_core_codegen/golang/transpilation.py index 93313d92d..de362bd3f 100644 --- a/aas_core_codegen/golang/transpilation.py +++ b/aas_core_codegen/golang/transpilation.py @@ -776,8 +776,14 @@ def transform_is_in( # NOTE (mristin): # The lengths are ``int``'s, so we convert them to our integers to look - # them up in a set. - if isinstance(container_type, intermediate_type_inference.SetTypeAnnotation): + # them up in a set or a list. + if isinstance( + container_type, + ( + intermediate_type_inference.SetTypeAnnotation, + intermediate_type_inference.ListTypeAnnotation, + ), + ): member = self._as_int64_position(node.member, member) # NOTE (mristin): @@ -796,6 +802,36 @@ def transform_is_in( ourcommon.MapContains( {I}{indent_but_first_line(container, I)}, {I}{indent_but_first_line(member, I)}, +)""" + ), + None, + ) + + elif isinstance(container_type, intermediate_type_inference.ListTypeAnnotation): + return ( + Stripped( + f"""\ +ourcommon.SliceContains( +{I}{indent_but_first_line(container, I)}, +{I}{indent_but_first_line(member, I)}, +)""" + ), + None, + ) + + elif ( + intermediate_type_inference.try_primitive_type(container_type) + is intermediate_type_inference.PrimitiveType.STR + ): + # NOTE (mristin): + # The native ``strings.Contains`` works on the UTF-8 bytes, which is + # equivalent to the check on the characters for a valid UTF-8. + return ( + Stripped( + f"""\ +strings.Contains( +{I}{indent_but_first_line(container, I)}, +{I}{indent_but_first_line(member, I)}, )""" ), None, diff --git a/aas_core_codegen/intermediate/type_inference.py b/aas_core_codegen/intermediate/type_inference.py index bd35cca65..47b161096 100644 --- a/aas_core_codegen/intermediate/type_inference.py +++ b/aas_core_codegen/intermediate/type_inference.py @@ -3874,22 +3874,82 @@ def transform_is_in(self, node: parse_tree.IsIn) -> Optional["TypeAnnotationUnio ) success = False + # NOTE (mristin): + # The membership in a JSON-able object is a question about its keys, so + # we restrict only the search in a list. + if isinstance(container_type, ListTypeAnnotation) and isinstance( + member_type, + ( + JsonValueTypeAnnotation, + JsonArrayTypeAnnotation, + JsonObjectTypeAnnotation, + ), + ): + self.errors.append( + Error( + node.member.original_node, + f"We do not support searching for a JSON-able value in a list " + f"with ``in``, but the member is inferred to be {member_type}. " + f"The targets disagree on the comparison: Python compares " + f"the JSON-able values by value, while C#, Java and " + f"TypeScript compare the references of their arrays and " + f"objects, and Go panics when comparing them. Please " + f"contact the developers if you need this feature.", + ) + ) + success = False + + if try_primitive_type(member_type) is PrimitiveType.BYTEARRAY: + self.errors.append( + Error( + node.member.original_node, + f"We do not support looking up a byte array with ``in``, " + f"but the member is inferred to be {member_type}. " + f"The targets disagree on the comparison: Python compares " + f"the byte arrays byte by byte, C# and Java compare " + f"the references of their ``byte[]``'s, while Go can not " + f"compare ``[]byte`` with ``==`` at all. Please compare " + f"the byte arrays explicitly instead, *e.g.*, in a for-loop.", + ) + ) + success = False + if not success: return None # NOTE (mristin): - # The targets look up the member in a hash set, so the member has to be of - # the same type as the items. We accept the constrained primitives in - # either direction, as they are represented by their constrainees. - if isinstance(container_type, SetTypeAnnotation) and not ( + # The targets look up the member in a hash set or search for it in a list + # with the equality of the items, so the member has to be of the same type + # as the items. We accept the constrained primitives in either direction, + # as they are represented by their constrainees. + if isinstance(container_type, (SetTypeAnnotation, ListTypeAnnotation)) and not ( _assignable(target_type=container_type.items, value_type=member_type) or _assignable(target_type=member_type, value_type=container_type.items) ): + what = "set" if isinstance(container_type, SetTypeAnnotation) else "list" + self.errors.append( Error( node.member.original_node, f"Expected the member to be of the type of the items of " - f"the set {container_type}, but got: {member_type}", + f"the {what} {container_type}, but got: {member_type}", + ) + ) + return None + + # NOTE (mristin): + # The membership in a string is a check for a sub-string, so the member + # has to be a string as well. + if ( + try_primitive_type(container_type) is PrimitiveType.STR + and try_primitive_type(member_type) is not PrimitiveType.STR + ): + self.errors.append( + Error( + node.member.original_node, + f"Expected the member to be a string as we check for " + f"a sub-string in the container {container_type}, " + f"but got: {member_type}", ) ) return None diff --git a/aas_core_codegen/typescript/transpilation.py b/aas_core_codegen/typescript/transpilation.py index 33b8d6f0c..40cf7ef13 100644 --- a/aas_core_codegen/typescript/transpilation.py +++ b/aas_core_codegen/typescript/transpilation.py @@ -681,10 +681,8 @@ def transform_is_in( None, ) elif ( - isinstance( - container_type, intermediate_type_inference.PrimitiveTypeAnnotation - ) - and container_type.a_type is intermediate_type_inference.PrimitiveType.STR + intermediate_type_inference.try_primitive_type(container_type) + is intermediate_type_inference.PrimitiveType.STR ): return Stripped(f"{container}.includes({member})"), None else: diff --git a/dev/test_data/common_meta_models/list_of_classes.py b/dev/test_data/common_meta_models/list_of_classes.py index 6a33b950e..b91ea2d1f 100644 --- a/dev/test_data/common_meta_models/list_of_classes.py +++ b/dev/test_data/common_meta_models/list_of_classes.py @@ -71,6 +71,42 @@ def some_items_of(items: Sequence[Abstract_item]) -> List[Abstract_item]: return result +@verification +def is_in_simples(simple: Simple, simples: Sequence[Simple]) -> bool: + """ + Check whether :paramref:`simple` is in :paramref:`simples`. + + The targets compare the instances of the classes by their references. + """ + return simple in simples + + +@verification +def is_in_local_copy_of_simples(simple: Simple, simples: Sequence[Simple]) -> bool: + """ + Check whether :paramref:`simple` is in a local copy of :paramref:`simples`. + + The local copy is built with ``append``, and holds the same instances as + :paramref:`simples`. + """ + copied: List[Simple] = [] + for other in simples: + copied.append(other) + + return simple in copied + + +@invariant( + lambda self: all( + is_in_local_copy_of_simples(simple, self.some_simples) + for simple in self.some_simples + ), + "Each of some simples must be in a local copy of some simples.", +) +@invariant( + lambda self: not is_in_simples(self.item, self.some_simples), + "Item must not be one of some simples.", +) @invariant( lambda self: len(some_items_of(self.some_items)) <= 1, "At most one of some items must be a some item.", diff --git a/dev/test_data/common_meta_models/list_of_constrained_primitives.py b/dev/test_data/common_meta_models/list_of_constrained_primitives.py index e78482b63..22d50ebf2 100644 --- a/dev/test_data/common_meta_models/list_of_constrained_primitives.py +++ b/dev/test_data/common_meta_models/list_of_constrained_primitives.py @@ -3,6 +3,10 @@ The list literal holds constrained primitives, while the appended items are plain strings sliced from them. + +We also check the membership ``in`` them. We look up a plain string in the list +of constrained primitives, a sliced string in a local list built with +``append``, and check for a sub-string in a constrained primitive. """ from typing import List, Sequence @@ -34,6 +38,48 @@ def initials_of(names: Sequence[Name]) -> List[str]: return initials +@verification +def initials_are_unique(names: Sequence[Name]) -> bool: + """Check that :paramref:`names` start with unique characters.""" + initials: List[str] = [] + for name in names: + initial = name[:1] + if initial in initials: + return False + + initials.append(initial) + + return True + + +@verification +def is_in_names(text: str, names: Sequence[Name]) -> bool: + """Check whether :paramref:`text` is in :paramref:`names`.""" + return text in names + + +@verification +def contains_space(name: Name) -> bool: + """Check whether :paramref:`name` contains a space.""" + return " " in name + + +@invariant( + lambda self: initials_are_unique(self.some_names), + "Initials of some names must be unique.", +) +@invariant( + lambda self: all(not contains_space(name) for name in self.some_names), + "Some names must not contain spaces.", +) +@invariant( + lambda self: not is_in_names("Mallory", self.some_names), + "Some names must not contain Mallory.", +) +@invariant( + lambda self: not ("Eve" in self.some_names), + "Some names must not contain Eve.", +) @invariant( lambda self: all(initial != "x" for initial in initials_of(self.some_names)), "Some names must not start with x.", diff --git a/dev/test_data/common_meta_models/list_of_enums.py b/dev/test_data/common_meta_models/list_of_enums.py index cc130e592..ee2d8a4c5 100644 --- a/dev/test_data/common_meta_models/list_of_enums.py +++ b/dev/test_data/common_meta_models/list_of_enums.py @@ -1,4 +1,9 @@ -"""Check the lists of enumeration literals, their list literals and ``append``.""" +""" +Check the lists of enumeration literals, their list literals and ``append``. + +We also check the membership ``in`` a list of enumeration literals, passed as +an argument and given as a list literal. +""" from enum import Enum from typing import List, Sequence @@ -31,6 +36,23 @@ def failures_of(results: Sequence[Result]) -> List[Result]: return failures +@verification +def is_in_results(result: Result, results: Sequence[Result]) -> bool: + """Check whether :paramref:`result` is in :paramref:`results`.""" + return result in results + + +@invariant( + lambda self: all( + result in [Result.Ok, Result.Fail] for result in self.some_results + ), + "Some results must be either ok or fail.", +) +@invariant( + lambda self: not is_in_results(Result.Fail, self.some_results) + or Result.Ok in self.some_results, + "Some results must contain an ok if they contain a failure.", +) @invariant( lambda self: len(failures_of(self.some_results)) <= 1, "Some results must contain at most one failure.", diff --git a/dev/test_data/common_meta_models/list_of_primitives.py b/dev/test_data/common_meta_models/list_of_primitives.py index d709a01ef..018f12e00 100644 --- a/dev/test_data/common_meta_models/list_of_primitives.py +++ b/dev/test_data/common_meta_models/list_of_primitives.py @@ -1,11 +1,17 @@ """ Check the lists of primitives. -We also check the list literals and the local lists built with ``append``. +We check the list literals and the local lists built with ``append``. The lengths are appended to and put in a list literal on purpose, since the targets represent them differently from our integers. + +We also check the membership ``in`` a list of primitives, passed as a read-only +and as an optional argument, built locally with ``append`` or given as a list +literal, and the membership ``in`` a string, *i.e.*, the check for a sub-string. +The integer literals and the lengths are looked up in the list of integers on +purpose, since the targets represent them differently from the items. """ -from typing import List, Sequence +from typing import List, Optional, Sequence from icontract import DBC, invariant @@ -41,6 +47,74 @@ def positives_of(numbers: Sequence[int]) -> List[int]: return result +@verification +def ints_are_unique(numbers: Sequence[int]) -> bool: + """Check that :paramref:`numbers` are unique with a local list of the seen.""" + seen: List[int] = [] + for number in numbers: + if number in seen: + return False + + seen.append(number) + + return True + + +@verification +def is_separator(text: str) -> bool: + """Check whether :paramref:`text` is one of the separators.""" + return text in [".", ",", ";"] + + +@verification +def is_in_ints(number: int, numbers: Sequence[int]) -> bool: + """Check whether :paramref:`number` is in :paramref:`numbers`.""" + return number in numbers + + +@verification +def is_in_optional_strings(text: str, texts: Optional[Sequence[str]]) -> bool: + """Check whether :paramref:`text` is in :paramref:`texts`, if specified.""" + if texts is None: + return False + + return text in texts + + +@verification +def contains_dot(text: str) -> bool: + """Check whether :paramref:`text` contains a dot.""" + return "." in text + + +@invariant( + lambda self: all(not is_separator(text) for text in self.some_strings), + "Some strings must not be separators.", +) +@invariant( + lambda self: ints_are_unique(self.some_ints), + "Some ints must be unique.", +) +@invariant( + lambda self: all(not contains_dot(text) for text in self.some_strings), + "Strings must not contain dots.", +) +@invariant( + lambda self: not is_in_optional_strings("", self.some_strings), + "Strings must not contain an empty string.", +) +@invariant( + lambda self: not (-1.0 in self.some_floats), + "Floats must not contain minus one.", +) +@invariant( + lambda self: not is_in_ints(len(self.some_strings), self.some_ints), + "Ints must not contain the number of strings.", +) +@invariant( + lambda self: not (0 in self.some_ints), + "Ints must not contain zero.", +) @invariant( lambda self: len(positives_of(self.some_ints)) <= 1, "At most one of some ints must be positive.", diff --git a/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt b/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt index 20aad55e0..3ca426f67 100644 --- a/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt +++ b/dev/test_data/intermediate/common_meta_models/list_of_classes/expected_symbol_table.txt @@ -469,6 +469,60 @@ SymbolTable( original_node=...), original_node=...)"""), specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Item must not be one of some simples.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_simples', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='item', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_simples', + original_node=...)], + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Each of some simples must be in a local copy of some simples.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='simple', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_simples', + original_node=...), + original_node=...), + condition=FunctionCall( + name='is_in_local_copy_of_simples', + args=[ + Name( + identifier='simple', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_simples', + original_node=...)], + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', parsed=...)], serialization=Serialization( with_model_type=False), @@ -605,6 +659,84 @@ SymbolTable( snapshots=[], postconditions=[]), parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_in_simples', + visibility='PUBLIC', + arguments=[ + Argument( + name='simple', + type_annotation=OurTypeAnnotation( + our_type='Reference to our type Simple', + parsed=...), + default=None, + mutable=False, + parsed=...), + Argument( + name='simples', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Simple', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether simple is in simples.', + remarks=[ + 'The targets compare the instances of the classes by their references.'], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_in_local_copy_of_simples', + visibility='PUBLIC', + arguments=[ + Argument( + name='simple', + type_annotation=OurTypeAnnotation( + our_type='Reference to our type Simple', + parsed=...), + default=None, + mutable=False, + parsed=...), + Argument( + name='simples', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Simple', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether simple is in a local copy of simples.', + remarks=[ + textwrap.dedent("""\ + The local copy is built with append, and holds the same instances as + simples.""")], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., arguments_by_name=...)], verification_functions_by_name=..., meta_model=MetaModel( diff --git a/dev/test_data/intermediate/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt b/dev/test_data/intermediate/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt index a57a7da40..77474fcec 100644 --- a/dev/test_data/intermediate/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt +++ b/dev/test_data/intermediate/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt @@ -173,6 +173,86 @@ SymbolTable( original_node=...), original_node=...)"""), specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some names must not contain Eve.', + body=textwrap.dedent("""\ + Not( + operand=IsIn( + member=Constant( + value='Eve', + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some names must not contain Mallory.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_names', + args=[ + Constant( + value='Mallory', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...)], + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some names must not contain spaces.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='name', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...), + original_node=...), + condition=Not( + operand=FunctionCall( + name='contains_space', + args=[ + Name( + identifier='name', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Initials of some names must be unique.', + body=textwrap.dedent("""\ + FunctionCall( + name='initials_are_unique', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...)], + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', parsed=...)], serialization=Serialization( with_model_type=False), @@ -266,6 +346,99 @@ SymbolTable( snapshots=[], postconditions=[]), parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='initials_are_unique', + visibility='PUBLIC', + arguments=[ + Argument( + name='names', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Name', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check that names start with unique characters.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_in_names', + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=PrimitiveTypeAnnotation( + a_type='STR', + parsed=...), + default=None, + mutable=False, + parsed=...), + Argument( + name='names', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Name', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether text is in names.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='contains_space', + visibility='PUBLIC', + arguments=[ + Argument( + name='name', + type_annotation=OurTypeAnnotation( + our_type='Reference to our type Name', + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether name contains a space.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., arguments_by_name=...)], verification_functions_by_name=..., meta_model=MetaModel( @@ -274,7 +447,11 @@ SymbolTable( remarks=[ textwrap.dedent("""\ The list literal holds constrained primitives, while the appended items are - plain strings sliced from them.""")], + plain strings sliced from them."""), + textwrap.dedent("""\ + We also check the membership in them. We look up a plain string in the list + of constrained primitives, a sliced string in a local list built with + append, and check for a sub-string in a constrained primitive.""")], constraints_by_identifier=[], parsed=...), version='dummy', diff --git a/dev/test_data/intermediate/common_meta_models/list_of_enums/expected_symbol_table.txt b/dev/test_data/intermediate/common_meta_models/list_of_enums/expected_symbol_table.txt index 48e8f8975..963ec8d64 100644 --- a/dev/test_data/intermediate/common_meta_models/list_of_enums/expected_symbol_table.txt +++ b/dev/test_data/intermediate/common_meta_models/list_of_enums/expected_symbol_table.txt @@ -127,6 +127,81 @@ SymbolTable( original_node=...), original_node=...)"""), specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some results must contain an ok if they contain a failure.', + body=textwrap.dedent("""\ + Implication( + antecedent=FunctionCall( + name='is_in_results', + args=[ + Member( + instance=Name( + identifier='Result', + original_node=...), + name='Fail', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_results', + original_node=...)], + original_node=...), + consequent=IsIn( + member=Member( + instance=Name( + identifier='Result', + original_node=...), + name='Ok', + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_results', + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some results must be either ok or fail.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='result', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_results', + original_node=...), + original_node=...), + condition=IsIn( + member=Name( + identifier='result', + original_node=...), + container=ListLiteral( + items=[ + Member( + instance=Name( + identifier='Result', + original_node=...), + name='Ok', + original_node=...), + Member( + instance=Name( + identifier='Result', + original_node=...), + name='Fail', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', parsed=...)], serialization=Serialization( with_model_type=False), @@ -207,12 +282,52 @@ SymbolTable( snapshots=[], postconditions=[]), parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_in_results', + visibility='PUBLIC', + arguments=[ + Argument( + name='result', + type_annotation=OurTypeAnnotation( + our_type='Reference to our type Result', + parsed=...), + default=None, + mutable=False, + parsed=...), + Argument( + name='results', + type_annotation=ListTypeAnnotation( + items=OurTypeAnnotation( + our_type='Reference to our type Result', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether result is in results.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., arguments_by_name=...)], verification_functions_by_name=..., meta_model=MetaModel( description=DescriptionOfMetaModel( summary='Check the lists of enumeration literals, their list literals and append.', - remarks=[], + remarks=[ + textwrap.dedent("""\ + We also check the membership in a list of enumeration literals, passed as + an argument and given as a list literal.""")], constraints_by_identifier=[], parsed=...), version='dummy', diff --git a/dev/test_data/intermediate/common_meta_models/list_of_primitives/expected_symbol_table.txt b/dev/test_data/intermediate/common_meta_models/list_of_primitives/expected_symbol_table.txt index 46dae648b..d98ae77c8 100644 --- a/dev/test_data/intermediate/common_meta_models/list_of_primitives/expected_symbol_table.txt +++ b/dev/test_data/intermediate/common_meta_models/list_of_primitives/expected_symbol_table.txt @@ -269,6 +269,158 @@ SymbolTable( original_node=...), original_node=...)"""), specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Ints must not contain zero.', + body=textwrap.dedent("""\ + Not( + operand=IsIn( + member=Constant( + value=0, + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_ints', + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Ints must not contain the number of strings.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_ints', + args=[ + FunctionCall( + name='len', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...)], + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_ints', + original_node=...)], + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Floats must not contain minus one.', + body=textwrap.dedent("""\ + Not( + operand=IsIn( + member=Constant( + value=-1.0, + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_floats', + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Strings must not contain an empty string.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_optional_strings', + args=[ + Constant( + value='', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...)], + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Strings must not contain dots.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='text', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...), + original_node=...), + condition=Not( + operand=FunctionCall( + name='contains_dot', + args=[ + Name( + identifier='text', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some ints must be unique.', + body=textwrap.dedent("""\ + FunctionCall( + name='ints_are_unique', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_ints', + original_node=...)], + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', + parsed=...), + Invariant( + description='Some strings must not be separators.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='text', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...), + original_node=...), + condition=Not( + operand=FunctionCall( + name='is_separator', + args=[ + Name( + identifier='text', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), + specified_for='Reference to ConcreteClass Something', parsed=...)], serialization=Serialization( with_model_type=False), @@ -379,6 +531,165 @@ SymbolTable( snapshots=[], postconditions=[]), parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='ints_are_unique', + visibility='PUBLIC', + arguments=[ + Argument( + name='numbers', + type_annotation=ListTypeAnnotation( + items=PrimitiveTypeAnnotation( + a_type='INT', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check that numbers are unique with a local list of the seen.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_separator', + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=PrimitiveTypeAnnotation( + a_type='STR', + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether text is one of the separators.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_in_ints', + visibility='PUBLIC', + arguments=[ + Argument( + name='number', + type_annotation=PrimitiveTypeAnnotation( + a_type='INT', + parsed=...), + default=None, + mutable=False, + parsed=...), + Argument( + name='numbers', + type_annotation=ListTypeAnnotation( + items=PrimitiveTypeAnnotation( + a_type='INT', + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether number is in numbers.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='is_in_optional_strings', + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=PrimitiveTypeAnnotation( + a_type='STR', + parsed=...), + default=None, + mutable=False, + parsed=...), + Argument( + name='texts', + type_annotation=OptionalTypeAnnotation( + value=ListTypeAnnotation( + items=PrimitiveTypeAnnotation( + a_type='STR', + parsed=...), + parsed=...), + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether text is in texts, if specified.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., + arguments_by_name=...), + TranspilableVerification( + name='contains_dot', + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=PrimitiveTypeAnnotation( + a_type='STR', + parsed=...), + default=None, + mutable=False, + parsed=...)], + returns=PrimitiveTypeAnnotation( + a_type='BOOL', + parsed=...), + description=DescriptionOfSignature( + summary='Check whether text contains a dot.', + remarks=[], + arguments_by_name=[], + returns=None, + parsed=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + parsed=..., arguments_by_name=...)], verification_functions_by_name=..., meta_model=MetaModel( @@ -386,9 +697,15 @@ SymbolTable( summary='Check the lists of primitives.', remarks=[ textwrap.dedent("""\ - We also check the list literals and the local lists built with append. + We check the list literals and the local lists built with append. The lengths are appended to and put in a list literal on purpose, since - the targets represent them differently from our integers.""")], + the targets represent them differently from our integers."""), + textwrap.dedent("""\ + We also check the membership in a list of primitives, passed as a read-only + and as an optional argument, built locally with append or given as a list + literal, and the membership in a string, i.e., the check for a sub-string. + The integer literals and the lengths are looked up in the list of integers on + purpose, since the targets represent them differently from the items.""")], constraints_by_identifier=[], parsed=...), version='dummy', diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/initials_not_unique.json b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/initials_not_unique.json new file mode 100644 index 000000000..cb28fc61a --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/initials_not_unique.json @@ -0,0 +1,6 @@ +{ + "someNames": [ + "Alice", + "Anna" + ] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/name_contains_space.json b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/name_contains_space.json new file mode 100644 index 000000000..a5569468d --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/name_contains_space.json @@ -0,0 +1,5 @@ +{ + "someNames": [ + "Alice Smith" + ] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/names_contain_eve.json b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/names_contain_eve.json new file mode 100644 index 000000000..73fd24383 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/names_contain_eve.json @@ -0,0 +1,6 @@ +{ + "someNames": [ + "Alice", + "Eve" + ] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/names_contain_mallory.json b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/names_contain_mallory.json new file mode 100644 index 000000000..35ec8b59b --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/names_contain_mallory.json @@ -0,0 +1,5 @@ +{ + "someNames": [ + "Mallory" + ] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/initials_not_unique.xml b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/initials_not_unique.xml new file mode 100644 index 000000000..17c190780 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/initials_not_unique.xml @@ -0,0 +1 @@ +AliceAnna \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/name_contains_space.xml b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/name_contains_space.xml new file mode 100644 index 000000000..11bc5b30f --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/name_contains_space.xml @@ -0,0 +1 @@ +Alice Smith \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/names_contain_eve.xml b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/names_contain_eve.xml new file mode 100644 index 000000000..a6b87a68c --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/names_contain_eve.xml @@ -0,0 +1 @@ +AliceEve \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/names_contain_mallory.xml b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/names_contain_mallory.xml new file mode 100644 index 000000000..b19ab84e7 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_constrained_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/names_contain_mallory.xml @@ -0,0 +1 @@ +Mallory \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_enums/Json/Unexpected/Invalid/InvariantViolation/Something/fail_without_ok.json b/dev/test_data/live_tests/common_test_data/list_of_enums/Json/Unexpected/Invalid/InvariantViolation/Something/fail_without_ok.json new file mode 100644 index 000000000..8c7f95e70 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_enums/Json/Unexpected/Invalid/InvariantViolation/Something/fail_without_ok.json @@ -0,0 +1,5 @@ +{ + "someResults": [ + "fail" + ] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_enums/Xml/Unexpected/Invalid/InvariantViolation/something/fail_without_ok.xml b/dev/test_data/live_tests/common_test_data/list_of_enums/Xml/Unexpected/Invalid/InvariantViolation/something/fail_without_ok.xml new file mode 100644 index 000000000..26b162692 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_enums/Xml/Unexpected/Invalid/InvariantViolation/something/fail_without_ok.xml @@ -0,0 +1 @@ +fail \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/floats_contain_minus_one.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/floats_contain_minus_one.json new file mode 100644 index 000000000..89283f710 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/floats_contain_minus_one.json @@ -0,0 +1,10 @@ +{ + "someBools": [], + "someInts": [], + "someFloats": [ + 0.5, + -1.0 + ], + "someStrings": [], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_number_of_strings.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_number_of_strings.json new file mode 100644 index 000000000..864eca0a8 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_number_of_strings.json @@ -0,0 +1,14 @@ +{ + "someBools": [], + "someInts": [ + 4 + ], + "someFloats": [], + "someStrings": [ + "a", + "b", + "c", + "d" + ], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_zero.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_zero.json new file mode 100644 index 000000000..43a594217 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_contain_zero.json @@ -0,0 +1,10 @@ +{ + "someBools": [], + "someInts": [ + 1, + 0 + ], + "someFloats": [], + "someStrings": [], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_not_unique.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_not_unique.json new file mode 100644 index 000000000..a1d671ee1 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/ints_not_unique.json @@ -0,0 +1,10 @@ +{ + "someBools": [], + "someInts": [ + -4, + -4 + ], + "someFloats": [], + "someStrings": [], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/string_is_separator.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/string_is_separator.json new file mode 100644 index 000000000..945be7abd --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/string_is_separator.json @@ -0,0 +1,9 @@ +{ + "someBools": [], + "someInts": [], + "someFloats": [], + "someStrings": [ + ";" + ], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/strings_contain_dot.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/strings_contain_dot.json new file mode 100644 index 000000000..c88177560 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/strings_contain_dot.json @@ -0,0 +1,9 @@ +{ + "someBools": [], + "someInts": [], + "someFloats": [], + "someStrings": [ + "a.b" + ], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/strings_contain_empty.json b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/strings_contain_empty.json new file mode 100644 index 000000000..fdd628533 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Json/Unexpected/Invalid/InvariantViolation/Something/strings_contain_empty.json @@ -0,0 +1,10 @@ +{ + "someBools": [], + "someInts": [], + "someFloats": [], + "someStrings": [ + "a", + "" + ], + "someBytes": [] +} diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/floats_contain_minus_one.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/floats_contain_minus_one.xml new file mode 100644 index 000000000..e2182bb59 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/floats_contain_minus_one.xml @@ -0,0 +1 @@ +0.5-1.0 \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_number_of_strings.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_number_of_strings.xml new file mode 100644 index 000000000..0c2a31e46 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_number_of_strings.xml @@ -0,0 +1 @@ +4abcd \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_zero.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_zero.xml new file mode 100644 index 000000000..6f62c1a53 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_contain_zero.xml @@ -0,0 +1 @@ +10 \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_not_unique.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_not_unique.xml new file mode 100644 index 000000000..76372c3b3 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/ints_not_unique.xml @@ -0,0 +1 @@ +-4-4 \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/string_is_separator.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/string_is_separator.xml new file mode 100644 index 000000000..c74124a73 --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/string_is_separator.xml @@ -0,0 +1 @@ +; \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/strings_contain_dot.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/strings_contain_dot.xml new file mode 100644 index 000000000..29525b6ee --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/strings_contain_dot.xml @@ -0,0 +1 @@ +a.b \ No newline at end of file diff --git a/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/strings_contain_empty.xml b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/strings_contain_empty.xml new file mode 100644 index 000000000..d0e76caab --- /dev/null +++ b/dev/test_data/live_tests/common_test_data/list_of_primitives/Xml/Unexpected/Invalid/InvariantViolation/something/strings_contain_empty.xml @@ -0,0 +1 @@ +a \ No newline at end of file diff --git a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp index f546f856e..4b436c3b7 100644 --- a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp +++ b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/include/dummy/verification.hpp @@ -243,6 +243,27 @@ std::vector< >& items ); +/// \brief Check whether \p simple is in \p simples. +/// +/// The targets compare the instances of the classes by their references. +bool IsInSimples( + const std::shared_ptr& simple, + const std::vector< + std::shared_ptr + >& simples +); + +/// \brief Check whether \p simple is in a local copy of \p simples. +/// +/// The local copy is built with `append`, and holds the same instances as +/// \p simples. +bool IsInLocalCopyOfSimples( + const std::shared_ptr& simple, + const std::vector< + std::shared_ptr + >& simples +); + // endregion Verification functions } // namespace verification diff --git a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp index 38bfe0e81..226711371 100644 --- a/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp +++ b/dev/test_data/main/cpp/expected/list_of_classes/expected_output/src/verification.cpp @@ -86,6 +86,38 @@ std::vector< return result; } +bool IsInSimples( + const std::shared_ptr& simple, + const std::vector< + std::shared_ptr + >& simples +) { + return ( + common::Contains( + simples, + simple + ) + ); +} + +bool IsInLocalCopyOfSimples( + const std::shared_ptr& simple, + const std::vector< + std::shared_ptr + >& simples +) { + std::vector > copied = std::vector >(); + for (const std::shared_ptr& other : simples) { + copied.push_back(other); + } + return ( + common::Contains( + copied, + simple + ) + ); +} + // endregion Verification functions namespace { @@ -157,6 +189,35 @@ bool Something_2( ).size() <= 1; } +bool Something_3( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !verification::IsInSimples( + that->item(), + that->some_simples() + ); +} + +bool Something_4( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return common::All( + [&](const std::shared_ptr& simple) -> bool { + return verification::IsInLocalCopyOfSimples( + simple, + that->some_simples() + ); + }, + that->some_simples() + ); +} + /** * Give out the checks of the values of the \p shape. */ @@ -176,6 +237,15 @@ const std::vector& ChecksOf(Shape shape) { { &Something_2, L"At most one of some items must be a some item." + }, + { + &Something_3, + L"Item must not be one of some simples." + }, + { + &Something_4, + L"Each of some simples must be in a local copy of some " + L"simples." } }; return checks; diff --git a/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/include/dummy/verification.hpp b/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/include/dummy/verification.hpp index 75f03dfb3..7d02f359a 100644 --- a/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/include/dummy/verification.hpp +++ b/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/include/dummy/verification.hpp @@ -225,6 +225,22 @@ std::vector InitialsOf( const std::vector& names ); +/// \brief Check that \p names start with unique characters. +bool InitialsAreUnique( + const std::vector& names +); + +/// \brief Check whether \p text is in \p names. +bool IsInNames( + const std::wstring& text, + const std::vector& names +); + +/// \brief Check whether \p name contains a space. +bool ContainsSpace( + const std::wstring& name +); + // endregion Verification functions // region Verification of constrained primitives diff --git a/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/src/verification.cpp b/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/src/verification.cpp index 28b83313f..d8068c40b 100644 --- a/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/src/verification.cpp +++ b/dev/test_data/main/cpp/expected/list_of_constrained_primitives/expected_output/src/verification.cpp @@ -60,6 +60,43 @@ std::vector InitialsOf( return initials; } +bool InitialsAreUnique( + const std::vector& names +) { + std::vector initials = std::vector(); + for (const std::wstring& name : names) { + std::wstring initial = common::SliceStr(name, 0, 1); + if ( + common::Contains( + initials, + initial + ) + ) { + return false; + } + initials.push_back(initial); + } + return true; +} + +bool IsInNames( + const std::wstring& text, + const std::vector& names +) { + return ( + common::Contains( + names, + text + ) + ); +} + +bool ContainsSpace( + const std::wstring& name +) { + return name.find(L" ") != std::wstring::npos; +} + // endregion Verification functions namespace { @@ -133,6 +170,57 @@ bool Something_1( ); } +bool Something_2( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !common::Contains( + that->some_names(), + L"Eve" + ); +} + +bool Something_3( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !verification::IsInNames( + L"Mallory", + that->some_names() + ); +} + +bool Something_4( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return common::All( + [&](std::wstring name) -> bool { + return !verification::ContainsSpace( + name + ); + }, + that->some_names() + ); +} + +bool Something_5( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return verification::InitialsAreUnique( + that->some_names() + ); +} + /** * Give out the checks of the values of the \p shape. */ @@ -157,6 +245,22 @@ const std::vector& ChecksOf(Shape shape) { { &Something_1, L"Some names must not start with x." + }, + { + &Something_2, + L"Some names must not contain Eve." + }, + { + &Something_3, + L"Some names must not contain Mallory." + }, + { + &Something_4, + L"Some names must not contain spaces." + }, + { + &Something_5, + L"Initials of some names must be unique." } }; return checks; diff --git a/dev/test_data/main/cpp/expected/list_of_enums/expected_output/include/dummy/verification.hpp b/dev/test_data/main/cpp/expected/list_of_enums/expected_output/include/dummy/verification.hpp index 9d7ead47f..cdf76a5e7 100644 --- a/dev/test_data/main/cpp/expected/list_of_enums/expected_output/include/dummy/verification.hpp +++ b/dev/test_data/main/cpp/expected/list_of_enums/expected_output/include/dummy/verification.hpp @@ -224,6 +224,12 @@ std::vector FailuresOf( const std::vector& results ); +/// \brief Check whether \p result is in \p results. +bool IsInResults( + types::Result result, + const std::vector& results +); + // endregion Verification functions } // namespace verification diff --git a/dev/test_data/main/cpp/expected/list_of_enums/expected_output/src/verification.cpp b/dev/test_data/main/cpp/expected/list_of_enums/expected_output/src/verification.cpp index c8943dc63..6212cfbec 100644 --- a/dev/test_data/main/cpp/expected/list_of_enums/expected_output/src/verification.cpp +++ b/dev/test_data/main/cpp/expected/list_of_enums/expected_output/src/verification.cpp @@ -68,6 +68,18 @@ std::vector FailuresOf( return failures; } +bool IsInResults( + types::Result result, + const std::vector& results +) { + return ( + common::Contains( + results, + result + ) + ); +} + // endregion Verification functions namespace { @@ -127,6 +139,42 @@ bool Something_1( ).size() <= 1; } +bool Something_2( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !verification::IsInResults( + types::Result::kFail, + that->some_results() + ) + || common::Contains( + that->some_results(), + types::Result::kOk + ); +} + +bool Something_3( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return common::All( + [&](types::Result result) -> bool { + return common::Contains( + std::vector{ + types::Result::kOk, + types::Result::kFail + }, + result + ); + }, + that->some_results() + ); +} + /** * Give out the checks of the values of the \p shape. */ @@ -141,6 +189,14 @@ const std::vector& ChecksOf(Shape shape) { { &Something_1, L"Some results must contain at most one failure." + }, + { + &Something_2, + L"Some results must contain an ok if they contain a failure." + }, + { + &Something_3, + L"Some results must be either ok or fail." } }; return checks; diff --git a/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/include/dummy/verification.hpp b/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/include/dummy/verification.hpp index 40d259030..d2f0ffa5e 100644 --- a/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/include/dummy/verification.hpp +++ b/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/include/dummy/verification.hpp @@ -229,6 +229,35 @@ std::vector PositivesOf( const std::vector& numbers ); +/// \brief Check that \p numbers are unique with a local list of the seen. +bool IntsAreUnique( + const std::vector& numbers +); + +/// \brief Check whether \p text is one of the separators. +bool IsSeparator( + const std::wstring& text +); + +/// \brief Check whether \p number is in \p numbers. +bool IsInInts( + int64_t number, + const std::vector& numbers +); + +/// \brief Check whether \p text is in \p texts, if specified. +bool IsInOptionalStrings( + const std::wstring& text, + const common::optional< + std::vector + >& texts +); + +/// \brief Check whether \p text contains a dot. +bool ContainsDot( + const std::wstring& text +); + // endregion Verification functions } // namespace verification diff --git a/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/src/verification.cpp b/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/src/verification.cpp index c7e0edefa..c91d16a07 100644 --- a/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/src/verification.cpp +++ b/dev/test_data/main/cpp/expected/list_of_primitives/expected_output/src/verification.cpp @@ -74,6 +74,70 @@ std::vector PositivesOf( return result; } +bool IntsAreUnique( + const std::vector& numbers +) { + std::vector seen = std::vector(); + for (int64_t number : numbers) { + if ( + common::Contains( + seen, + number + ) + ) { + return false; + } + seen.push_back(number); + } + return true; +} + +bool IsSeparator( + const std::wstring& text +) { + return ( + common::Contains( + std::vector{L".", L",", L";"}, + text + ) + ); +} + +bool IsInInts( + int64_t number, + const std::vector& numbers +) { + return ( + common::Contains( + numbers, + number + ) + ); +} + +bool IsInOptionalStrings( + const std::wstring& text, + const common::optional< + std::vector + >& texts +) { + if (!(texts.has_value())) { + return false; + } + return ( + common::Contains( + (*texts), + text + ) + ); +} + +bool ContainsDot( + const std::wstring& text +) { + return text.find(L".") != std::wstring::npos; +} + // endregion Verification functions namespace { @@ -149,6 +213,97 @@ bool Something_2( ).size() <= 1; } +bool Something_3( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !common::Contains( + that->some_ints(), + 0 + ); +} + +bool Something_4( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !verification::IsInInts( + that->some_strings().size(), + that->some_ints() + ); +} + +bool Something_5( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !common::Contains( + that->some_floats(), + -1.0 + ); +} + +bool Something_6( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return !verification::IsInOptionalStrings( + L"", + that->some_strings() + ); +} + +bool Something_7( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return common::All( + [&](std::wstring text) -> bool { + return !verification::ContainsDot( + text + ); + }, + that->some_strings() + ); +} + +bool Something_8( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return verification::IntsAreUnique( + that->some_ints() + ); +} + +bool Something_9( + const void* value +) { + const types::ISomething* that = ( + static_cast(value) + ); + return common::All( + [&](std::wstring text) -> bool { + return !verification::IsSeparator( + text + ); + }, + that->some_strings() + ); +} + /** * Give out the checks of the values of the \p shape. */ @@ -168,6 +323,34 @@ const std::vector& ChecksOf(Shape shape) { { &Something_2, L"At most one of some ints must be positive." + }, + { + &Something_3, + L"Ints must not contain zero." + }, + { + &Something_4, + L"Ints must not contain the number of strings." + }, + { + &Something_5, + L"Floats must not contain minus one." + }, + { + &Something_6, + L"Strings must not contain an empty string." + }, + { + &Something_7, + L"Strings must not contain dots." + }, + { + &Something_8, + L"Some ints must be unique." + }, + { + &Something_9, + L"Some strings must not be separators." } }; return checks; diff --git a/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs b/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs index c4abbd712..2b908b28e 100644 --- a/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs +++ b/dev/test_data/main/csharp/expected/list_of_classes/expected_output/dummy/verification.cs @@ -84,6 +84,40 @@ List items return result; } // public static List SomeItemsOf + /// + /// Check whether is in . + /// + /// + /// The targets compare the instances of the classes by their references. + /// + public static bool IsInSimples( + ISimple simple, + List simples + ) + { + return simples.Contains(simple); + } // public static bool IsInSimples + + /// + /// Check whether is in a local copy of . + /// + /// + /// The local copy is built with append, and holds the same instances as + /// . + /// + public static bool IsInLocalCopyOfSimples( + ISimple simple, + List simples + ) + { + List copied = new List(); + foreach (var other in simples) + { + copied.Add(other); + } + return copied.Contains(simple); + } // public static bool IsInLocalCopyOfSimples + /// /// Hash allowed enum values for efficient validation of enums. /// @@ -157,6 +191,24 @@ Our.ISomething that "At most one of some items must be a some item."); } + if (!( + !Verification.IsInSimples(that.Item, that.SomeSimples))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Item must not be one of some simples."); + } + + if (!( + that.SomeSimples.All( + simple => Verification.IsInLocalCopyOfSimples(simple, that.SomeSimples)))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Each of some simples must be in a local copy of some " + + "simples."); + } + foreach (var error in Verification.Verify(that.Item)) { error.PrependSegment( diff --git a/dev/test_data/main/csharp/expected/list_of_constrained_primitives/expected_output/dummy/verification.cs b/dev/test_data/main/csharp/expected/list_of_constrained_primitives/expected_output/dummy/verification.cs index 0776490b7..408291cde 100644 --- a/dev/test_data/main/csharp/expected/list_of_constrained_primitives/expected_output/dummy/verification.cs +++ b/dev/test_data/main/csharp/expected/list_of_constrained_primitives/expected_output/dummy/verification.cs @@ -62,6 +62,47 @@ List names return initials; } // public static List InitialsOf + /// + /// Check that start with unique characters. + /// + public static bool InitialsAreUnique( + List names + ) + { + List initials = new List(); + foreach (var name in names) + { + var initial = Common.StringHelpers.Slice(name, 0, 1); + if (initials.Contains(initial)) + { + return false; + } + initials.Add(initial); + } + return true; + } // public static bool InitialsAreUnique + + /// + /// Check whether is in . + /// + public static bool IsInNames( + string text, + List names + ) + { + return names.Contains(text); + } // public static bool IsInNames + + /// + /// Check whether contains a space. + /// + public static bool ContainsSpace( + string name + ) + { + return name.Contains(" "); + } // public static bool ContainsSpace + /// /// Hash allowed enum values for efficient validation of enums. /// @@ -101,6 +142,36 @@ Our.ISomething that "Some names must not start with x."); } + if (!(!that.SomeNames.Contains("Eve"))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some names must not contain Eve."); + } + + if (!(!Verification.IsInNames("Mallory", that.SomeNames))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some names must not contain Mallory."); + } + + if (!( + that.SomeNames.All( + name => !Verification.ContainsSpace(name)))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some names must not contain spaces."); + } + + if (!Verification.InitialsAreUnique(that.SomeNames)) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Initials of some names must be unique."); + } + foreach (var error in Verification.Verify_ListOf_Name(that.SomeNames)) { error.PrependSegment( diff --git a/dev/test_data/main/csharp/expected/list_of_enums/expected_output/dummy/verification.cs b/dev/test_data/main/csharp/expected/list_of_enums/expected_output/dummy/verification.cs index 6e184b373..93396f5dc 100644 --- a/dev/test_data/main/csharp/expected/list_of_enums/expected_output/dummy/verification.cs +++ b/dev/test_data/main/csharp/expected/list_of_enums/expected_output/dummy/verification.cs @@ -66,6 +66,17 @@ List results return failures; } // public static List FailuresOf + /// + /// Check whether is in . + /// + public static bool IsInResults( + Result result, + List results + ) + { + return results.Contains(result); + } // public static bool IsInResults + /// /// Hash allowed enum values for efficient validation of enums. /// @@ -108,6 +119,24 @@ Our.ISomething that "Some results must contain at most one failure."); } + if (!( + !Verification.IsInResults(Result.Fail, that.SomeResults) + || that.SomeResults.Contains(Result.Ok))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some results must contain an ok if they contain a failure."); + } + + if (!( + that.SomeResults.All( + result => (new List { Result.Ok, Result.Fail }).Contains(result)))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some results must be either ok or fail."); + } + foreach ( var error in Verification.Verify_ListOf_Result( that.SomeResults)) diff --git a/dev/test_data/main/csharp/expected/list_of_primitives/expected_output/dummy/verification.cs b/dev/test_data/main/csharp/expected/list_of_primitives/expected_output/dummy/verification.cs index 1f0a6e1c6..b18744d3a 100644 --- a/dev/test_data/main/csharp/expected/list_of_primitives/expected_output/dummy/verification.cs +++ b/dev/test_data/main/csharp/expected/list_of_primitives/expected_output/dummy/verification.cs @@ -81,6 +81,72 @@ List numbers return result; } // public static List PositivesOf + /// + /// Check that are unique with a local list of the seen. + /// + public static bool IntsAreUnique( + List numbers + ) + { + List seen = new List(); + foreach (var number in numbers) + { + if (seen.Contains(number)) + { + return false; + } + seen.Add(number); + } + return true; + } // public static bool IntsAreUnique + + /// + /// Check whether is one of the separators. + /// + public static bool IsSeparator( + string text + ) + { + return ( + (new List { ".", ",", ";" }).Contains(text)); + } // public static bool IsSeparator + + /// + /// Check whether is in . + /// + public static bool IsInInts( + long number, + List numbers + ) + { + return numbers.Contains(number); + } // public static bool IsInInts + + /// + /// Check whether is in , if specified. + /// + public static bool IsInOptionalStrings( + string text, + List? texts + ) + { + if (texts == null) + { + return false; + } + return texts.Contains(text); + } // public static bool IsInOptionalStrings + + /// + /// Check whether contains a dot. + /// + public static bool ContainsDot( + string text + ) + { + return text.Contains("."); + } // public static bool ContainsDot + /// /// Hash allowed enum values for efficient validation of enums. /// @@ -127,6 +193,61 @@ Our.ISomething that "Invariant violated:\n" + "At most one of some ints must be positive."); } + + if (!(!that.SomeInts.Contains(0))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Ints must not contain zero."); + } + + if (!( + !Verification.IsInInts(that.SomeStrings.Count, that.SomeInts))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Ints must not contain the number of strings."); + } + + if (!(!that.SomeFloats.Contains(-1.0))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Floats must not contain minus one."); + } + + if (!( + !Verification.IsInOptionalStrings("", that.SomeStrings))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Strings must not contain an empty string."); + } + + if (!( + that.SomeStrings.All( + text => !Verification.ContainsDot(text)))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Strings must not contain dots."); + } + + if (!Verification.IntsAreUnique(that.SomeInts)) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some ints must be unique."); + } + + if (!( + that.SomeStrings.All( + text => !Verification.IsSeparator(text)))) + { + yield return new Reporting.Error( + "Invariant violated:\n" + + "Some strings must not be separators."); + } } } // private class Transformer diff --git a/dev/test_data/main/golang/expected/aas_core_meta.v3/expected_output/common/common.go b/dev/test_data/main/golang/expected/aas_core_meta.v3/expected_output/common/common.go index 4fcf2084c..aef908bbd 100644 --- a/dev/test_data/main/golang/expected/aas_core_meta.v3/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/aas_core_meta.v3/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/annotated_assignments/expected_output/common/common.go b/dev/test_data/main/golang/expected/annotated_assignments/expected_output/common/common.go index 95ce0cf4e..384cf6ed6 100644 --- a/dev/test_data/main/golang/expected/annotated_assignments/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/annotated_assignments/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/arithmetic/expected_output/common/common.go b/dev/test_data/main/golang/expected/arithmetic/expected_output/common/common.go index c798c2e1a..3eed0b382 100644 --- a/dev/test_data/main/golang/expected/arithmetic/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/arithmetic/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/assert_statements/expected_output/common/common.go b/dev/test_data/main/golang/expected/assert_statements/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/assert_statements/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/assert_statements/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/assignment_targets/expected_output/common/common.go b/dev/test_data/main/golang/expected/assignment_targets/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/assignment_targets/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/assignment_targets/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/collections_in_returns/expected_output/common/common.go b/dev/test_data/main/golang/expected/collections_in_returns/expected_output/common/common.go index cd022160d..e830e0e1d 100644 --- a/dev/test_data/main/golang/expected/collections_in_returns/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/collections_in_returns/expected_output/common/common.go @@ -26,6 +26,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/constrained_primitives/expected_output/common/common.go b/dev/test_data/main/golang/expected/constrained_primitives/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/constrained_primitives/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/constrained_primitives/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/custom_serialization_names/expected_output/common/common.go b/dev/test_data/main/golang/expected/custom_serialization_names/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/custom_serialization_names/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/custom_serialization_names/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/deep_class_hierarchy/expected_output/common/common.go b/dev/test_data/main/golang/expected/deep_class_hierarchy/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/deep_class_hierarchy/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/deep_class_hierarchy/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/empty_class/expected_output/common/common.go b/dev/test_data/main/golang/expected/empty_class/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/empty_class/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/empty_class/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/enum/expected_output/common/common.go b/dev/test_data/main/golang/expected/enum/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/enum/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/enum/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/float_only/expected_output/common/common.go b/dev/test_data/main/golang/expected/float_only/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/float_only/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/float_only/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/for_statements/expected_output/common/common.go b/dev/test_data/main/golang/expected/for_statements/expected_output/common/common.go index 9cb9e1e46..a93f333f5 100644 --- a/dev/test_data/main/golang/expected/for_statements/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/for_statements/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/if_statements/expected_output/common/common.go b/dev/test_data/main/golang/expected/if_statements/expected_output/common/common.go index 9cb9e1e46..a93f333f5 100644 --- a/dev/test_data/main/golang/expected/if_statements/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/if_statements/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/implementation_specific/expected_output/common/common.go b/dev/test_data/main/golang/expected/implementation_specific/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/implementation_specific/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/implementation_specific/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/int_length_interplay/expected_output/common/common.go b/dev/test_data/main/golang/expected/int_length_interplay/expected_output/common/common.go index 9cb9e1e46..a93f333f5 100644 --- a/dev/test_data/main/golang/expected/int_length_interplay/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/int_length_interplay/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/int_parsing_and_lstrip/expected_output/common/common.go b/dev/test_data/main/golang/expected/int_parsing_and_lstrip/expected_output/common/common.go index 489283bd9..0a823533a 100644 --- a/dev/test_data/main/golang/expected/int_parsing_and_lstrip/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/int_parsing_and_lstrip/expected_output/common/common.go @@ -26,6 +26,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/is_instance/expected_output/common/common.go b/dev/test_data/main/golang/expected/is_instance/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/is_instance/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/is_instance/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/json_types/expected_output/common/common.go b/dev/test_data/main/golang/expected/json_types/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/json_types/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/json_types/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/json_types_in_collections/expected_output/common/common.go b/dev/test_data/main/golang/expected/json_types_in_collections/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/json_types_in_collections/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/json_types_in_collections/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/json_types_in_invariants/expected_output/common/common.go b/dev/test_data/main/golang/expected/json_types_in_invariants/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/json_types_in_invariants/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/json_types_in_invariants/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/list_of_classes/expected_output/common/common.go b/dev/test_data/main/golang/expected/list_of_classes/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/list_of_classes/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/list_of_classes/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go b/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go index b6c220b36..227c6b0be 100644 --- a/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go +++ b/dev/test_data/main/golang/expected/list_of_classes/expected_output/verification/verification.go @@ -84,6 +84,37 @@ func SomeItemsOf( return result } +// Check whether simple is in simples. +// +// The targets compare the instances of the classes by their references. +func IsInSimples( + simple ourtypes.ISimple, + simples []ourtypes.ISimple, +) bool { + return ourcommon.SliceContains( + simples, + simple, + ) +} + +// Check whether simple is in a local copy of simples. +// +// The local copy is built with `append`, and holds the same instances as +// simples. +func IsInLocalCopyOfSimples( + simple ourtypes.ISimple, + simples []ourtypes.ISimple, +) bool { + var copied []ourtypes.ISimple = []ourtypes.ISimple{} + for _, other := range simples { + copied = append(copied, other) + } + return ourcommon.SliceContains( + copied, + simple, + ) +} + // Verify `that` instance of [ourtypes.ISomeItem]. // // You have to supply the callback `onError` to iterate over the errors. @@ -186,6 +217,34 @@ func VerifySomething( } } + if !(!IsInSimples(that.Item(), that.SomeSimples())) { + abort = onError( + newVerificationError( + "Item must not be one of some simples.",), + ) + if abort { + return + } + } + + if !( + ourcommon.All( + func(simple ourtypes.ISimple) bool { + return IsInLocalCopyOfSimples(simple, that.SomeSimples()) + }, + that.SomeSimples(), + )) { + abort = onError( + newVerificationError( + "Each of some simples must be in a local copy of some " + + "simples.", + ), + ) + if abort { + return + } + } + if that.Item() == nil { abort = onError( newVerificationError( diff --git a/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/common/common.go b/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/types/types.go b/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/types/types.go index bd08d828a..992ab2322 100644 --- a/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/types/types.go +++ b/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/types/types.go @@ -4,6 +4,10 @@ // // The list literal holds constrained primitives, while the appended items are // plain strings sliced from them. +// +// We also check the membership `in` them. We look up a plain string in the list +// of constrained primitives, a sliced string in a local list built with +// `append`, and check for a sub-string in a constrained primitive. package types // This code has been automatically generated by aas-core-codegen. diff --git a/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/verification/verification.go b/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/verification/verification.go index c81fab1b9..44fe1d152 100644 --- a/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/verification/verification.go +++ b/dev/test_data/main/golang/expected/list_of_constrained_primitives/expected_output/verification/verification.go @@ -12,6 +12,7 @@ package verification import ( "fmt" + "strings" ourcommon "github.com/dummy-works/dummy/common" ourreporting "github.com/dummy-works/dummy/reporting" ourtypes "github.com/dummy-works/dummy/types" @@ -68,6 +69,46 @@ func InitialsOf( return initials } +// Check that names start with unique characters. +func InitialsAreUnique( + names []string, +) bool { + var initials []string = []string{} + for _, name := range names { + initial := ourcommon.SliceStr(name, 0, 1) + if ( + ourcommon.SliceContains( + initials, + initial, + )) { + return false + } + initials = append(initials, initial) + } + return true +} + +// Check whether text is in names. +func IsInNames( + text string, + names []string, +) bool { + return ourcommon.SliceContains( + names, + text, + ) +} + +// Check whether name contains a space. +func ContainsSpace( + name string, +) bool { + return strings.Contains( + name, + " ", + ) +} + // Verify `that` instance of [ourtypes.ISomething]. // // You have to supply the callback `onError` to iterate over the errors. @@ -114,6 +155,56 @@ func VerifySomething( } } + if !( + !ourcommon.SliceContains( + that.SomeNames(), + "Eve", + )) { + abort = onError( + newVerificationError( + "Some names must not contain Eve.",), + ) + if abort { + return + } + } + + if !(!IsInNames("Mallory", that.SomeNames())) { + abort = onError( + newVerificationError( + "Some names must not contain Mallory.",), + ) + if abort { + return + } + } + + if !( + ourcommon.All( + func(name string) bool { + return !ContainsSpace(name) + }, + that.SomeNames(), + )) { + abort = onError( + newVerificationError( + "Some names must not contain spaces.",), + ) + if abort { + return + } + } + + if !InitialsAreUnique(that.SomeNames()) { + abort = onError( + newVerificationError( + "Initials of some names must be unique.",), + ) + if abort { + return + } + } + if that.SomeNames() == nil { abort = onError( newVerificationError( diff --git a/dev/test_data/main/golang/expected/list_of_enums/expected_output/common/common.go b/dev/test_data/main/golang/expected/list_of_enums/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/list_of_enums/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/list_of_enums/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/list_of_enums/expected_output/types/types.go b/dev/test_data/main/golang/expected/list_of_enums/expected_output/types/types.go index 25a7d42d9..c142a2492 100644 --- a/dev/test_data/main/golang/expected/list_of_enums/expected_output/types/types.go +++ b/dev/test_data/main/golang/expected/list_of_enums/expected_output/types/types.go @@ -1,6 +1,9 @@ // Package types provides the data structures corresponding to the meta-model. // // Check the lists of enumeration literals, their list literals and `append`. +// +// We also check the membership `in` a list of enumeration literals, passed as +// an argument and given as a list literal. package types // This code has been automatically generated by aas-core-codegen. diff --git a/dev/test_data/main/golang/expected/list_of_enums/expected_output/verification/verification.go b/dev/test_data/main/golang/expected/list_of_enums/expected_output/verification/verification.go index 24b9b981a..955cd0882 100644 --- a/dev/test_data/main/golang/expected/list_of_enums/expected_output/verification/verification.go +++ b/dev/test_data/main/golang/expected/list_of_enums/expected_output/verification/verification.go @@ -70,6 +70,17 @@ func FailuresOf( return failures } +// Check whether result is in results. +func IsInResults( + result ourtypes.Result, + results []ourtypes.Result, +) bool { + return ourcommon.SliceContains( + results, + result, + ) +} + // Verify `that` instance of [ourtypes.ISomething]. // // You have to supply the callback `onError` to iterate over the errors. @@ -108,6 +119,40 @@ func VerifySomething( } } + if !( + !IsInResults(ourtypes.ResultFail, that.SomeResults()) || + ourcommon.SliceContains( + that.SomeResults(), + ourtypes.ResultOk, + )) { + abort = onError( + newVerificationError( + "Some results must contain an ok if they contain a failure.",), + ) + if abort { + return + } + } + + if !( + ourcommon.All( + func(result ourtypes.Result) bool { + return ourcommon.SliceContains( + []ourtypes.Result{ourtypes.ResultOk, ourtypes.ResultFail}, + result, + ) + }, + that.SomeResults(), + )) { + abort = onError( + newVerificationError( + "Some results must be either ok or fail.",), + ) + if abort { + return + } + } + if that.SomeResults() == nil { abort = onError( newVerificationError( diff --git a/dev/test_data/main/golang/expected/list_of_primitives/expected_output/common/common.go b/dev/test_data/main/golang/expected/list_of_primitives/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/list_of_primitives/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/list_of_primitives/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/list_of_primitives/expected_output/types/types.go b/dev/test_data/main/golang/expected/list_of_primitives/expected_output/types/types.go index b9775072c..e68b96a25 100644 --- a/dev/test_data/main/golang/expected/list_of_primitives/expected_output/types/types.go +++ b/dev/test_data/main/golang/expected/list_of_primitives/expected_output/types/types.go @@ -2,9 +2,15 @@ // // Check the lists of primitives. // -// We also check the list literals and the local lists built with `append`. +// We check the list literals and the local lists built with `append`. // The lengths are appended to and put in a list literal on purpose, since // the targets represent them differently from our integers. +// +// We also check the membership `in` a list of primitives, passed as a read-only +// and as an optional argument, built locally with `append` or given as a list +// literal, and the membership `in` a string, i.e., the check for a sub-string. +// The integer literals and the lengths are looked up in the list of integers on +// purpose, since the targets represent them differently from the items. package types // This code has been automatically generated by aas-core-codegen. diff --git a/dev/test_data/main/golang/expected/list_of_primitives/expected_output/verification/verification.go b/dev/test_data/main/golang/expected/list_of_primitives/expected_output/verification/verification.go index da12a807d..27ed0ad40 100644 --- a/dev/test_data/main/golang/expected/list_of_primitives/expected_output/verification/verification.go +++ b/dev/test_data/main/golang/expected/list_of_primitives/expected_output/verification/verification.go @@ -12,6 +12,7 @@ package verification import ( "fmt" + "strings" ourcommon "github.com/dummy-works/dummy/common" ourreporting "github.com/dummy-works/dummy/reporting" ourtypes "github.com/dummy-works/dummy/types" @@ -81,6 +82,69 @@ func PositivesOf( return result } +// Check that numbers are unique with a local list of the seen. +func IntsAreUnique( + numbers []int64, +) bool { + var seen []int64 = []int64{} + for _, number := range numbers { + if ( + ourcommon.SliceContains( + seen, + number, + )) { + return false + } + seen = append(seen, number) + } + return true +} + +// Check whether text is one of the separators. +func IsSeparator( + text string, +) bool { + return ourcommon.SliceContains( + []string{".", ",", ";"}, + text, + ) +} + +// Check whether number is in numbers. +func IsInInts( + number int64, + numbers []int64, +) bool { + return ourcommon.SliceContains( + numbers, + number, + ) +} + +// Check whether text is in texts, if specified. +func IsInOptionalStrings( + text string, + texts []string, +) bool { + if texts == nil { + return false + } + return ourcommon.SliceContains( + texts, + text, + ) +} + +// Check whether text contains a dot. +func ContainsDot( + text string, +) bool { + return strings.Contains( + text, + ".", + ) +} + // Verify `that` instance of [ourtypes.ISomething]. // // You have to supply the callback `onError` to iterate over the errors. @@ -137,6 +201,100 @@ func VerifySomething( } } + if !( + !ourcommon.SliceContains( + that.SomeInts(), + 0, + )) { + abort = onError( + newVerificationError( + "Ints must not contain zero.",), + ) + if abort { + return + } + } + + if !( + !IsInInts( + int64(len(that.SomeStrings())), + that.SomeInts(), + )) { + abort = onError( + newVerificationError( + "Ints must not contain the number of strings.",), + ) + if abort { + return + } + } + + if !( + !ourcommon.SliceContains( + that.SomeFloats(), + -1.0, + )) { + abort = onError( + newVerificationError( + "Floats must not contain minus one.",), + ) + if abort { + return + } + } + + if !(!IsInOptionalStrings("", that.SomeStrings())) { + abort = onError( + newVerificationError( + "Strings must not contain an empty string.",), + ) + if abort { + return + } + } + + if !( + ourcommon.All( + func(text string) bool { + return !ContainsDot(text) + }, + that.SomeStrings(), + )) { + abort = onError( + newVerificationError( + "Strings must not contain dots.",), + ) + if abort { + return + } + } + + if !IntsAreUnique(that.SomeInts()) { + abort = onError( + newVerificationError( + "Some ints must be unique.",), + ) + if abort { + return + } + } + + if !( + ourcommon.All( + func(text string) bool { + return !IsSeparator(text) + }, + that.SomeStrings(), + )) { + abort = onError( + newVerificationError( + "Some strings must not be separators.",), + ) + if abort { + return + } + } + if that.SomeBools() == nil { abort = onError( newVerificationError( diff --git a/dev/test_data/main/golang/expected/method_references/expected_output/common/common.go b/dev/test_data/main/golang/expected/method_references/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/method_references/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/method_references/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/nested_any_in_all/expected_output/common/common.go b/dev/test_data/main/golang/expected/nested_any_in_all/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/nested_any_in_all/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/nested_any_in_all/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/nested_collections/expected_output/common/common.go b/dev/test_data/main/golang/expected/nested_collections/expected_output/common/common.go index cd022160d..e830e0e1d 100644 --- a/dev/test_data/main/golang/expected/nested_collections/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/nested_collections/expected_output/common/common.go @@ -26,6 +26,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/optional_arguments/expected_output/common/common.go b/dev/test_data/main/golang/expected/optional_arguments/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/optional_arguments/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/optional_arguments/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/primitive_types/expected_output/common/common.go b/dev/test_data/main/golang/expected/primitive_types/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/primitive_types/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/primitive_types/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/problematic_keywords/expected_output/common/common.go b/dev/test_data/main/golang/expected/problematic_keywords/expected_output/common/common.go index f9afae550..b7b572a16 100644 --- a/dev/test_data/main/golang/expected/problematic_keywords/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/problematic_keywords/expected_output/common/common.go @@ -24,6 +24,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/sets/expected_output/common/common.go b/dev/test_data/main/golang/expected/sets/expected_output/common/common.go index 0d730c739..c395e3d5e 100644 --- a/dev/test_data/main/golang/expected/sets/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/sets/expected_output/common/common.go @@ -26,6 +26,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/string_slicing_and_find/expected_output/common/common.go b/dev/test_data/main/golang/expected/string_slicing_and_find/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/string_slicing_and_find/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/string_slicing_and_find/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/switch_statements/expected_output/common/common.go b/dev/test_data/main/golang/expected/switch_statements/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/switch_statements/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/switch_statements/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/transpiled_methods/expected_output/common/common.go b/dev/test_data/main/golang/expected/transpiled_methods/expected_output/common/common.go index c798c2e1a..3eed0b382 100644 --- a/dev/test_data/main/golang/expected/transpiled_methods/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/transpiled_methods/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/tuples/expected_output/common/common.go b/dev/test_data/main/golang/expected/tuples/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/tuples/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/tuples/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/unions/expected_output/common/common.go b/dev/test_data/main/golang/expected/unions/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/unions/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/unions/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/golang/expected/visibility/expected_output/common/common.go b/dev/test_data/main/golang/expected/visibility/expected_output/common/common.go index 4df2957f9..0f9a80b11 100644 --- a/dev/test_data/main/golang/expected/visibility/expected_output/common/common.go +++ b/dev/test_data/main/golang/expected/visibility/expected_output/common/common.go @@ -25,6 +25,20 @@ func MapContains[K comparable, V any](m map[K]V, k K) bool { return ok } +// Check if the slice contains the given value. +// +// We can not use ``slices.Contains`` as it is available only from Go 1.21 on. +// We compare the values as ``any``'s, since the interfaces, such as our classes, +// satisfy the constraint ``comparable`` only from Go 1.20 on. +func SliceContains[T any](s []T, v T) bool { + for _, item := range s { + if any(item) == any(v) { + return true + } + } + return false +} + // Check if any of the elements satisfy the condition. func Some[V any](condition func(V) bool, l []V) bool { ok := false diff --git a/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java b/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java index db33f8d83..289665344 100644 --- a/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java +++ b/dev/test_data/main/java/expected/list_of_classes/expected_output/src/main/java/dummy/verification/Verification.java @@ -73,6 +73,33 @@ public static List someItemsOf( return result; } + /** + * Check whether {@code simple} is in {@code simples}. + * + *

The targets compare the instances of the classes by their references. + */ + public static Boolean isInSimples( + ISimple simple, + List simples) { + return simples.contains(simple); + } + + /** + * Check whether {@code simple} is in a local copy of {@code simples}. + * + *

The local copy is built with {@code append}, and holds the same instances as + * {@code simples}. + */ + public static Boolean isInLocalCopyOfSimples( + ISimple simple, + List simples) { + List copied = new java.util.ArrayList(); + for (var other : simples) { + copied.add(other); + } + return copied.contains(simple); + } + /** * Hash allowed enum values for efficient validation of enums. */ @@ -143,6 +170,24 @@ public Stream transformSomething( "At most one of some items must be a some item."))); } + if (!( + !isInSimples(that.getItem(), that.getSomeSimples()))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Item must not be one of some simples."))); + } + + if (!( + that.getSomeSimples().stream().allMatch( + simple -> isInLocalCopyOfSimples(simple, that.getSomeSimples())))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Each of some simples must be in a local copy of some " + + "simples."))); + } + errorStream = Stream.concat(errorStream, Stream.of(that.getItem()) .flatMap(Verification::verifyToErrorStream) diff --git a/dev/test_data/main/java/expected/list_of_constrained_primitives/expected_output/src/main/java/dummy/verification/Verification.java b/dev/test_data/main/java/expected/list_of_constrained_primitives/expected_output/src/main/java/dummy/verification/Verification.java index 6e68127a7..9915d3734 100644 --- a/dev/test_data/main/java/expected/list_of_constrained_primitives/expected_output/src/main/java/dummy/verification/Verification.java +++ b/dev/test_data/main/java/expected/list_of_constrained_primitives/expected_output/src/main/java/dummy/verification/Verification.java @@ -56,6 +56,39 @@ public static List initialsOf( return initials; } + /** + * Check that {@code names} start with unique characters. + */ + public static Boolean initialsAreUnique( + List names) { + List initials = new java.util.ArrayList(); + for (var name : names) { + var initial = StringHelpers.slice(name, 0, 1); + if (initials.contains(initial)) { + return false; + } + initials.add(initial); + } + return true; + } + + /** + * Check whether {@code text} is in {@code names}. + */ + public static Boolean isInNames( + String text, + List names) { + return names.contains(text); + } + + /** + * Check whether {@code name} contains a space. + */ + public static Boolean containsSpace( + String name) { + return name.contains(" "); + } + /** * Hash allowed enum values for efficient validation of enums. */ @@ -90,6 +123,36 @@ public Stream transformSomething( "Some names must not start with x."))); } + if (!(!that.getSomeNames().contains("Eve"))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some names must not contain Eve."))); + } + + if (!(!isInNames("Mallory", that.getSomeNames()))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some names must not contain Mallory."))); + } + + if (!( + that.getSomeNames().stream().allMatch( + name -> !containsSpace(name)))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some names must not contain spaces."))); + } + + if (!initialsAreUnique(that.getSomeNames())) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Initials of some names must be unique."))); + } + errorStream = Stream.concat(errorStream, Stream.of(that.getSomeNames()) .flatMap(Verification::verifyListOf_Name) diff --git a/dev/test_data/main/java/expected/list_of_enums/expected_output/src/main/java/dummy/verification/Verification.java b/dev/test_data/main/java/expected/list_of_enums/expected_output/src/main/java/dummy/verification/Verification.java index 176dc14f0..f3e3fcadd 100644 --- a/dev/test_data/main/java/expected/list_of_enums/expected_output/src/main/java/dummy/verification/Verification.java +++ b/dev/test_data/main/java/expected/list_of_enums/expected_output/src/main/java/dummy/verification/Verification.java @@ -57,6 +57,15 @@ public static List failuresOf( return failures; } + /** + * Check whether {@code result} is in {@code results}. + */ + public static Boolean isInResults( + Result result, + List results) { + return results.contains(result); + } + /** * Hash allowed enum values for efficient validation of enums. */ @@ -100,6 +109,24 @@ public Stream transformSomething( "Some results must contain at most one failure."))); } + if (!( + !isInResults(Result.FAIL, that.getSomeResults()) + || that.getSomeResults().contains(Result.OK))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some results must contain an ok if they contain a failure."))); + } + + if (!( + that.getSomeResults().stream().allMatch( + result -> (new java.util.ArrayList(java.util.List.of(Result.OK, Result.FAIL))).contains(result)))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some results must be either ok or fail."))); + } + errorStream = Stream.concat(errorStream, Stream.of(that.getSomeResults()) .flatMap(Verification::verifyListOf_Result) diff --git a/dev/test_data/main/java/expected/list_of_primitives/expected_output/src/main/java/dummy/verification/Verification.java b/dev/test_data/main/java/expected/list_of_primitives/expected_output/src/main/java/dummy/verification/Verification.java index b5a7a3718..bd19f880a 100644 --- a/dev/test_data/main/java/expected/list_of_primitives/expected_output/src/main/java/dummy/verification/Verification.java +++ b/dev/test_data/main/java/expected/list_of_primitives/expected_output/src/main/java/dummy/verification/Verification.java @@ -28,6 +28,7 @@ import dummy.types.model.*; import dummy.visitation.AbstractTransformer; import java.util.List; +import java.util.Optional; public class Verification { /** @@ -70,6 +71,59 @@ public static List positivesOf( return result; } + /** + * Check that {@code numbers} are unique with a local list of the seen. + */ + public static Boolean intsAreUnique( + List numbers) { + List seen = new java.util.ArrayList(); + for (var number : numbers) { + if (seen.contains(number)) { + return false; + } + seen.add(number); + } + return true; + } + + /** + * Check whether {@code text} is one of the separators. + */ + public static Boolean isSeparator( + String text) { + return ( + (new java.util.ArrayList(java.util.List.of(".", ",", ";"))).contains(text)); + } + + /** + * Check whether {@code number} is in {@code numbers}. + */ + public static Boolean isInInts( + Long number, + List numbers) { + return numbers.contains(number); + } + + /** + * Check whether {@code text} is in {@code texts}, if specified. + */ + public static Boolean isInOptionalStrings( + String text, + Optional> texts) { + if (!texts.isPresent()) { + return false; + } + return texts.get().contains(text); + } + + /** + * Check whether {@code text} contains a dot. + */ + public static Boolean containsDot( + String text) { + return text.contains("."); + } + /** * Hash allowed enum values for efficient validation of enums. */ @@ -111,6 +165,63 @@ public Stream transformSomething( "At most one of some ints must be positive."))); } + if (!(!that.getSomeInts().contains(0L))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Ints must not contain zero."))); + } + + if (!( + !isInInts( + (long) that.getSomeStrings().size(), + that.getSomeInts()))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Ints must not contain the number of strings."))); + } + + if (!(!that.getSomeFloats().contains(-1.0))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Floats must not contain minus one."))); + } + + if (!( + !isInOptionalStrings("", Optional.of(that.getSomeStrings())))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Strings must not contain an empty string."))); + } + + if (!( + that.getSomeStrings().stream().allMatch( + text -> !containsDot(text)))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Strings must not contain dots."))); + } + + if (!intsAreUnique(that.getSomeInts())) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some ints must be unique."))); + } + + if (!( + that.getSomeStrings().stream().allMatch( + text -> !isSeparator(text)))) { + errorStream = Stream.concat(errorStream, + Stream.of(new Reporting.Error( + "Invariant violated:\n" + + "Some strings must not be separators."))); + } + return errorStream; } } diff --git a/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py b/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py index 860c02869..5a8b3de48 100644 --- a/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py +++ b/dev/test_data/main/python/expected/list_of_classes/expected_output/dummy/verification.py @@ -102,6 +102,36 @@ def some_items_of( return result +def is_in_simples( + simple: our_types.Simple, + simples: Sequence[our_types.Simple] +) -> bool: + """ + Check whether :paramref:`simple` is in :paramref:`simples`. + + The targets compare the instances of the classes by their references. + """ + # pylint: disable=all + return simple in simples + + +def is_in_local_copy_of_simples( + simple: our_types.Simple, + simples: Sequence[our_types.Simple] +) -> bool: + """ + Check whether :paramref:`simple` is in a local copy of :paramref:`simples`. + + The local copy is built with ``append``, and holds the same instances as + :paramref:`simples`. + """ + # pylint: disable=all + copied: List[our_types.Simple] = [] + for other in simples: + copied.append(other) + return simple in copied + + class _Transformer( our_types.AbstractTransformer[ Iterator[Error] @@ -171,6 +201,25 @@ def transform_something( 'At most one of some items must be a some item.' ) + if not (not is_in_simples(that.item, that.some_simples)): + yield Error( + 'Item must not be one of some simples.' + ) + + if not ( + all( + is_in_local_copy_of_simples( + simple, + that.some_simples + ) + for simple in that.some_simples + ) + ): + yield Error( + 'Each of some simples must be in a local copy of some ' + + 'simples.' + ) + for error in verify(that.item): error.path._prepend( PropertySegment( diff --git a/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/types.py b/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/types.py index d8dded918..4814b0a9b 100644 --- a/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/types.py +++ b/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/types.py @@ -3,6 +3,10 @@ The list literal holds constrained primitives, while the appended items are plain strings sliced from them. + +We also check the membership ``in`` them. We look up a plain string in the list +of constrained primitives, a sliced string in a local list built with +``append``, and check for a sub-string in a constrained primitive. """ diff --git a/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/verification.py b/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/verification.py index cbde4e67b..5f607e35a 100644 --- a/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/verification.py +++ b/dev/test_data/main/python/expected/list_of_constrained_primitives/expected_output/dummy/verification.py @@ -87,6 +87,37 @@ def initials_of( return initials +def initials_are_unique( + names: Sequence[str] +) -> bool: + """Check that :paramref:`names` start with unique characters.""" + # pylint: disable=all + initials: List[str] = [] + for name in names: + initial = name[:1] + if initial in initials: + return False + initials.append(initial) + return True + + +def is_in_names( + text: str, + names: Sequence[str] +) -> bool: + """Check whether :paramref:`text` is in :paramref:`names`.""" + # pylint: disable=all + return text in names + + +def contains_space( + name: str +) -> bool: + """Check whether :paramref:`name` contains a space.""" + # pylint: disable=all + return ' ' in name + + class _Transformer( our_types.AbstractTransformer[ Iterator[Error] @@ -118,6 +149,31 @@ def transform_something( 'Some names must not start with x.' ) + if not (not ('Eve' in that.some_names)): + yield Error( + 'Some names must not contain Eve.' + ) + + if not (not is_in_names('Mallory', that.some_names)): + yield Error( + 'Some names must not contain Mallory.' + ) + + if not ( + all( + not contains_space(name) + for name in that.some_names + ) + ): + yield Error( + 'Some names must not contain spaces.' + ) + + if not initials_are_unique(that.some_names): + yield Error( + 'Initials of some names must be unique.' + ) + for error in _verify_list_of__name(that.some_names): error.path._prepend( PropertySegment( diff --git a/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/types.py b/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/types.py index 4ae7204e0..dbc637bc6 100644 --- a/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/types.py +++ b/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/types.py @@ -1,5 +1,8 @@ """ Check the lists of enumeration literals, their list literals and ``append``. + +We also check the membership ``in`` a list of enumeration literals, passed as +an argument and given as a list literal. """ diff --git a/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/verification.py b/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/verification.py index 01e85a4f3..c14cd65a5 100644 --- a/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/verification.py +++ b/dev/test_data/main/python/expected/list_of_enums/expected_output/dummy/verification.py @@ -85,6 +85,15 @@ def failures_of( return failures +def is_in_results( + result: our_types.Result, + results: Sequence[our_types.Result] +) -> bool: + """Check whether :paramref:`result` is in :paramref:`results`.""" + # pylint: disable=all + return result in results + + class _Transformer( our_types.AbstractTransformer[ Iterator[Error] @@ -110,6 +119,27 @@ def transform_something( 'Some results must contain at most one failure.' ) + if not ( + not is_in_results( + our_types.Result.FAIL, + that.some_results + ) + or (our_types.Result.OK in that.some_results) + ): + yield Error( + 'Some results must contain an ok if they contain a failure.' + ) + + if not ( + all( + result in [our_types.Result.OK, our_types.Result.FAIL] + for result in that.some_results + ) + ): + yield Error( + 'Some results must be either ok or fail.' + ) + _TRANSFORMER = _Transformer() diff --git a/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/types.py b/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/types.py index 1969ed391..2d3893348 100644 --- a/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/types.py +++ b/dev/test_data/main/python/expected/list_of_primitives/expected_output/dummy/types.py @@ -1,9 +1,15 @@ """ Check the lists of primitives. -We also check the list literals and the local lists built with ``append``. +We check the list literals and the local lists built with ``append``. The lengths are appended to and put in a list literal on purpose, since the targets represent them differently from our integers. + +We also check the membership ``in`` a list of primitives, passed as a read-only +and as an optional argument, built locally with ``append`` or given as a list +literal, and the membership ``in`` a string, *i.e.*, the check for a sub-string. +The integer literals and the lengths are looked up in the list of integers on +purpose, since the targets represent them differently from the items. """ 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 63ae09f0a..a010f8e6e 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 @@ -96,6 +96,59 @@ def positives_of( return result +def ints_are_unique( + numbers: Sequence[int] +) -> bool: + """ + Check that :paramref:`numbers` are unique with a local list of the seen. + """ + # pylint: disable=all + seen: List[int] = [] + for number in numbers: + if number in seen: + return False + seen.append(number) + return True + + +def is_separator( + text: str +) -> bool: + """Check whether :paramref:`text` is one of the separators.""" + # pylint: disable=all + return text in ['.', ',', ';'] + + +def is_in_ints( + number: int, + numbers: Sequence[int] +) -> bool: + """Check whether :paramref:`number` is in :paramref:`numbers`.""" + # pylint: disable=all + return number in numbers + + +def is_in_optional_strings( + text: str, + texts: Optional[Sequence[str]] +) -> bool: + """ + Check whether :paramref:`text` is in :paramref:`texts`, if specified. + """ + # pylint: disable=all + if texts is None: + return False + return text in texts + + +def contains_dot( + text: str +) -> bool: + """Check whether :paramref:`text` contains a dot.""" + # pylint: disable=all + return '.' in text + + class _Transformer( our_types.AbstractTransformer[ Iterator[Error] @@ -132,6 +185,53 @@ def transform_something( 'At most one of some ints must be positive.' ) + if not (not (0 in that.some_ints)): + yield Error( + 'Ints must not contain zero.' + ) + + if not ( + not is_in_ints(len(that.some_strings), that.some_ints) + ): + yield Error( + 'Ints must not contain the number of strings.' + ) + + if not (not (-1.0 in that.some_floats)): + yield Error( + 'Floats must not contain minus one.' + ) + + if not (not is_in_optional_strings('', that.some_strings)): + yield Error( + 'Strings must not contain an empty string.' + ) + + if not ( + all( + not contains_dot(text) + for text in that.some_strings + ) + ): + yield Error( + 'Strings must not contain dots.' + ) + + if not ints_are_unique(that.some_ints): + yield Error( + 'Some ints must be unique.' + ) + + if not ( + all( + not is_separator(text) + for text in that.some_strings + ) + ): + yield Error( + 'Some strings must not be separators.' + ) + _TRANSFORMER = _Transformer() diff --git a/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts b/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts index 9db3e4da5..02f1feeb1 100644 --- a/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts +++ b/dev/test_data/main/typescript/expected/list_of_classes/expected_output/src/verification.ts @@ -236,6 +236,39 @@ export function someItemsOf( return result; } +/** + * Check whether `simple` is in `simples`. + * + * @remarks + * + * The targets compare the instances of the classes by their references. + */ +export function isInSimples( + simple: OurTypes.Simple, + simples: Array +): boolean { + return simples.includes(simple); +} + +/** + * Check whether `simple` is in a local copy of `simples`. + * + * @remarks + * + * The local copy is built with `append`, and holds the same instances as + * `simples`. + */ +export function isInLocalCopyOfSimples( + simple: OurTypes.Simple, + simples: Array +): boolean { + const copied: Array = []; + for (const other of simples) { + copied.push(other); + } + return copied.includes(simple); +} + /** * Verify the items of `that` recursively. */ @@ -322,6 +355,27 @@ class Verifier ) } + if (!(!isInSimples(that.item, that.someSimples))) { + yield new VerificationError( + "Item must not be one of some simples." + ) + } + + if (!( + OurCommon.every( + OurCommon.map( + that.someSimples, + simple => + isInLocalCopyOfSimples(simple, that.someSimples) + ) + ) + )) { + yield new VerificationError( + "Each of some simples must be in a local copy of some " + + "simples." + ) + } + if (context === true) { for (const error of verify(that.item)) { error.path.prepend( diff --git a/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/types.ts b/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/types.ts index 9c8bc05c8..0e5daa12d 100644 --- a/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/types.ts +++ b/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/types.ts @@ -4,6 +4,10 @@ * @remarks * The list literal holds constrained primitives, while the appended items are * plain strings sliced from them. + * + * We also check the membership `in` them. We look up a plain string in the list + * of constrained primitives, a sliced string in a local list built with + * `append`, and check for a sub-string in a constrained primitive. */ // This code has been automatically generated by aas-core-codegen. diff --git a/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/verification.ts b/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/verification.ts index c57a519ae..912a35af0 100644 --- a/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/verification.ts +++ b/dev/test_data/main/typescript/expected/list_of_constrained_primitives/expected_output/src/verification.ts @@ -216,6 +216,42 @@ export function initialsOf( return initials; } +/** + * Check that `names` start with unique characters. + */ +export function initialsAreUnique( + names: Array +): boolean { + const initials: Array = []; + for (const name of names) { + const initial = OurCommon.sliceStr(name, 0, 1); + if (initials.includes(initial)) { + return false; + } + initials.push(initial); + } + return true; +} + +/** + * Check whether `text` is in `names`. + */ +export function isInNames( + text: string, + names: Array +): boolean { + return names.includes(text); +} + +/** + * Check whether `name` contains a space. + */ +export function containsSpace( + name: string +): boolean { + return name.includes(" "); +} + /** * Verify the items of `that` recursively. */ @@ -275,6 +311,38 @@ class Verifier ) } + if (!(!(that.someNames.includes("Eve")))) { + yield new VerificationError( + "Some names must not contain Eve." + ) + } + + if (!(!isInNames("Mallory", that.someNames))) { + yield new VerificationError( + "Some names must not contain Mallory." + ) + } + + if (!( + OurCommon.every( + OurCommon.map( + that.someNames, + name => + !containsSpace(name) + ) + ) + )) { + yield new VerificationError( + "Some names must not contain spaces." + ) + } + + if (!initialsAreUnique(that.someNames)) { + yield new VerificationError( + "Initials of some names must be unique." + ) + } + if (context === true) { for (const error of verify_ListOf_Name(that.someNames)) { error.path.prepend( diff --git a/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/types.ts b/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/types.ts index cf3c751c2..797792721 100644 --- a/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/types.ts +++ b/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/types.ts @@ -1,5 +1,9 @@ /** * Check the lists of enumeration literals, their list literals and `append`. + * + * @remarks + * We also check the membership `in` a list of enumeration literals, passed as + * an argument and given as a list literal. */ // This code has been automatically generated by aas-core-codegen. diff --git a/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/verification.ts b/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/verification.ts index 2e98038cb..d0e569464 100644 --- a/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/verification.ts +++ b/dev/test_data/main/typescript/expected/list_of_enums/expected_output/src/verification.ts @@ -218,6 +218,16 @@ export function failuresOf( return failures; } +/** + * Check whether `result` is in `results`. + */ +export function isInResults( + result: OurTypes.Result, + results: Array +): boolean { + return results.includes(result); +} + /** * Verify an instance of the model recursively or non-recursively (depending on the context). */ @@ -249,6 +259,29 @@ class Verifier "Some results must contain at most one failure." ) } + + if (!( + !isInResults(OurTypes.Result.Fail, that.someResults) + || (that.someResults.includes(OurTypes.Result.Ok)) + )) { + yield new VerificationError( + "Some results must contain an ok if they contain a failure." + ) + } + + if (!( + OurCommon.every( + OurCommon.map( + that.someResults, + result => + [OurTypes.Result.Ok, OurTypes.Result.Fail].includes(result) + ) + ) + )) { + yield new VerificationError( + "Some results must be either ok or fail." + ) + } } } diff --git a/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/types.ts b/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/types.ts index 646c92dd1..d34dddaed 100644 --- a/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/types.ts +++ b/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/src/types.ts @@ -2,9 +2,15 @@ * Check the lists of primitives. * * @remarks - * We also check the list literals and the local lists built with `append`. + * We check the list literals and the local lists built with `append`. * The lengths are appended to and put in a list literal on purpose, since * the targets represent them differently from our integers. + * + * We also check the membership `in` a list of primitives, passed as a read-only + * and as an optional argument, built locally with `append` or given as a list + * literal, and the membership `in` a string, *i.e.*, the check for a sub-string. + * The integer literals and the lengths are looked up in the list of integers on + * purpose, since the targets represent them differently from the items. */ // This code has been automatically generated by aas-core-codegen. 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 647d773f2..8ba11fd66 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 @@ -231,6 +231,63 @@ export function positivesOf( return result; } +/** + * Check that `numbers` are unique with a local list of the seen. + */ +export function intsAreUnique( + numbers: Array +): boolean { + const seen: Array = []; + for (const number of numbers) { + if (seen.includes(number)) { + return false; + } + seen.push(number); + } + return true; +} + +/** + * Check whether `text` is one of the separators. + */ +export function isSeparator( + text: string +): boolean { + return [".", ",", ";"].includes(text); +} + +/** + * Check whether `number` is in `numbers`. + */ +export function isInInts( + number: number, + numbers: Array +): boolean { + return numbers.includes(number); +} + +/** + * Check whether `text` is in `texts`, if specified. + */ +export function isInOptionalStrings( + text: string, + texts: Array | null +): boolean { + if (texts === null) { + return false; + } + return texts.includes(text); +} + +/** + * Check whether `text` contains a dot. + */ +export function containsDot( + text: string +): boolean { + return text.includes("."); +} + /** * Verify an instance of the model recursively or non-recursively (depending on the context). */ @@ -277,6 +334,64 @@ class Verifier "At most one of some ints must be positive." ) } + + if (!(!(that.someInts.includes(0)))) { + yield new VerificationError( + "Ints must not contain zero." + ) + } + + if (!(!isInInts(that.someStrings.length, that.someInts))) { + yield new VerificationError( + "Ints must not contain the number of strings." + ) + } + + if (!(!(that.someFloats.includes(-1.0)))) { + yield new VerificationError( + "Floats must not contain minus one." + ) + } + + if (!(!isInOptionalStrings("", that.someStrings))) { + yield new VerificationError( + "Strings must not contain an empty string." + ) + } + + if (!( + OurCommon.every( + OurCommon.map( + that.someStrings, + text => + !containsDot(text) + ) + ) + )) { + yield new VerificationError( + "Strings must not contain dots." + ) + } + + if (!intsAreUnique(that.someInts)) { + yield new VerificationError( + "Some ints must be unique." + ) + } + + if (!( + OurCommon.every( + OurCommon.map( + that.someStrings, + text => + !isSeparator(text) + ) + ) + )) { + yield new VerificationError( + "Some strings must not be separators." + ) + } } } diff --git a/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/test/verification.spec.ts b/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/test/verification.spec.ts index 5ee1ece36..512e61da4 100644 --- a/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/test/verification.spec.ts +++ b/dev/test_data/main/typescript/expected/list_of_primitives/expected_output/test/verification.spec.ts @@ -45,5 +45,21 @@ test("verification error stores provided path", () => { expect(error.path.toString()).toStrictEqual(".idShort"); }); +test("isSeparator returns boolean", () => { + const resultOnEmpty = OurVerification.isSeparator(""); + expect(typeof resultOnEmpty).toStrictEqual("boolean"); + + const resultOnSample = OurVerification.isSeparator("sample-value"); + expect(typeof resultOnSample).toStrictEqual("boolean"); +}); + +test("containsDot returns boolean", () => { + const resultOnEmpty = OurVerification.containsDot(""); + expect(typeof resultOnEmpty).toStrictEqual("boolean"); + + const resultOnSample = OurVerification.containsDot("sample-value"); + expect(typeof resultOnSample).toStrictEqual("boolean"); +}); + // This code has been automatically generated by aas-core-codegen. // Do NOT edit or append. diff --git a/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt b/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt index f2436d336..a5f956cf2 100644 --- a/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt +++ b/dev/test_data/parse/common_meta_models/list_of_classes/expected_symbol_table.txt @@ -344,6 +344,58 @@ UnverifiedSymbolTable( value=1, original_node=...), original_node=...)"""), + node=...), + Invariant( + description='Item must not be one of some simples.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_simples', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='item', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_simples', + original_node=...)], + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Each of some simples must be in a local copy of some simples.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='simple', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_simples', + original_node=...), + original_node=...), + condition=FunctionCall( + name='is_in_local_copy_of_simples', + args=[ + Name( + identifier='simple', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_simples', + original_node=...)], + original_node=...), + original_node=...)"""), node=...)], serialization=None, description=None, @@ -623,6 +675,145 @@ UnverifiedSymbolTable( original_node=...), original_node=...)""")], node=..., + arguments_by_name=...), + UnderstoodMethod( + name='is_in_simples', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='simple', + type_annotation=AtomicTypeAnnotation( + identifier='Simple', + node=...), + default=None, + node=...), + Argument( + name='simples', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Simple', + 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("""\ + Return( + value=IsIn( + member=Name( + identifier='simple', + original_node=...), + container=Name( + identifier='simples', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='is_in_local_copy_of_simples', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='simple', + type_annotation=AtomicTypeAnnotation( + identifier='Simple', + node=...), + default=None, + node=...), + Argument( + name='simples', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Simple', + 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("""\ + Assignment( + target=Name( + identifier='copied', + original_node=...), + value=ListLiteral( + items=[], + original_node=...), + annotation=Index( + collection=Name( + identifier='List', + original_node=...), + index=Name( + identifier='Simple', + original_node=...), + original_node=...), + original_node=...)"""), + textwrap.dedent("""\ + For( + generator=ForEach( + variable=Name( + identifier='other', + original_node=...), + iteration=Name( + identifier='simples', + original_node=...), + original_node=...), + body=[ + ExpressionStatement( + expression=MethodCall( + member=Member( + instance=Name( + identifier='copied', + original_node=...), + name='append', + original_node=...), + args=[ + Name( + identifier='other', + original_node=...)], + original_node=...), + original_node=...)], + original_node=...)"""), + textwrap.dedent("""\ + Return( + value=IsIn( + member=Name( + identifier='simple', + original_node=...), + container=Name( + identifier='copied', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., arguments_by_name=...)], meta_model=MetaModel( description=None, diff --git a/dev/test_data/parse/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt b/dev/test_data/parse/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt index 9449c81c8..bfe20394b 100644 --- a/dev/test_data/parse/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt +++ b/dev/test_data/parse/common_meta_models/list_of_constrained_primitives/expected_symbol_table.txt @@ -160,6 +160,82 @@ UnverifiedSymbolTable( original_node=...), original_node=...), original_node=...)"""), + node=...), + Invariant( + description='Some names must not contain Eve.', + body=textwrap.dedent("""\ + Not( + operand=IsIn( + member=Constant( + value='Eve', + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...), + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Some names must not contain Mallory.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_names', + args=[ + Constant( + value='Mallory', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...)], + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Some names must not contain spaces.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='name', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...), + original_node=...), + condition=Not( + operand=FunctionCall( + name='contains_space', + args=[ + Name( + identifier='name', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Initials of some names must be unique.', + body=textwrap.dedent("""\ + FunctionCall( + name='initials_are_unique', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_names', + original_node=...)], + original_node=...)"""), node=...)], serialization=None, description=None, @@ -343,6 +419,205 @@ UnverifiedSymbolTable( original_node=...), original_node=...)""")], node=..., + arguments_by_name=...), + UnderstoodMethod( + name='initials_are_unique', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='names', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Name', + 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("""\ + Assignment( + target=Name( + identifier='initials', + original_node=...), + value=ListLiteral( + items=[], + original_node=...), + annotation=Index( + collection=Name( + identifier='List', + original_node=...), + index=Name( + identifier='str', + original_node=...), + original_node=...), + original_node=...)"""), + textwrap.dedent("""\ + For( + generator=ForEach( + variable=Name( + identifier='name', + original_node=...), + iteration=Name( + identifier='names', + original_node=...), + original_node=...), + body=[ + Assignment( + target=Name( + identifier='initial', + original_node=...), + value=Slice( + collection=Name( + identifier='name', + original_node=...), + start=None, + end=Constant( + value=1, + original_node=...), + original_node=...), + annotation=None, + original_node=...), + If( + branches=[ + IfBranch( + condition=IsIn( + member=Name( + identifier='initial', + original_node=...), + container=Name( + identifier='initials', + original_node=...), + original_node=...), + body=[ + Return( + value=Constant( + value=False, + original_node=...), + original_node=...)], + original_node=...)], + default=None, + original_node=...), + ExpressionStatement( + expression=MethodCall( + member=Member( + instance=Name( + identifier='initials', + original_node=...), + name='append', + original_node=...), + args=[ + Name( + identifier='initial', + original_node=...)], + original_node=...), + original_node=...)], + original_node=...)"""), + textwrap.dedent("""\ + Return( + value=Constant( + value=True, + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='is_in_names', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=AtomicTypeAnnotation( + identifier='str', + node=...), + default=None, + node=...), + Argument( + name='names', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Name', + 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("""\ + Return( + value=IsIn( + member=Name( + identifier='text', + original_node=...), + container=Name( + identifier='names', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='contains_space', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='name', + type_annotation=AtomicTypeAnnotation( + identifier='Name', + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=IsIn( + member=Constant( + value=' ', + original_node=...), + container=Name( + identifier='name', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., arguments_by_name=...)], meta_model=MetaModel( description=Description( diff --git a/dev/test_data/parse/common_meta_models/list_of_enums/expected_symbol_table.txt b/dev/test_data/parse/common_meta_models/list_of_enums/expected_symbol_table.txt index 64b7b9e82..c15443f69 100644 --- a/dev/test_data/parse/common_meta_models/list_of_enums/expected_symbol_table.txt +++ b/dev/test_data/parse/common_meta_models/list_of_enums/expected_symbol_table.txt @@ -113,6 +113,79 @@ UnverifiedSymbolTable( value=1, original_node=...), original_node=...)"""), + node=...), + Invariant( + description='Some results must contain an ok if they contain a failure.', + body=textwrap.dedent("""\ + Implication( + antecedent=FunctionCall( + name='is_in_results', + args=[ + Member( + instance=Name( + identifier='Result', + original_node=...), + name='Fail', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_results', + original_node=...)], + original_node=...), + consequent=IsIn( + member=Member( + instance=Name( + identifier='Result', + original_node=...), + name='Ok', + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_results', + original_node=...), + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Some results must be either ok or fail.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='result', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_results', + original_node=...), + original_node=...), + condition=IsIn( + member=Name( + identifier='result', + original_node=...), + container=ListLiteral( + items=[ + Member( + instance=Name( + identifier='Result', + original_node=...), + name='Ok', + original_node=...), + Member( + instance=Name( + identifier='Result', + original_node=...), + name='Fail', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), node=...)], serialization=None, description=None, @@ -300,6 +373,54 @@ UnverifiedSymbolTable( original_node=...), original_node=...)""")], node=..., + arguments_by_name=...), + UnderstoodMethod( + name='is_in_results', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='result', + type_annotation=AtomicTypeAnnotation( + identifier='Result', + node=...), + default=None, + node=...), + Argument( + name='results', + type_annotation=SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='Result', + 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("""\ + Return( + value=IsIn( + member=Name( + identifier='result', + original_node=...), + container=Name( + identifier='results', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., arguments_by_name=...)], meta_model=MetaModel( description=Description( 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 7ae95f31a..fe41c321f 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 @@ -225,6 +225,151 @@ UnverifiedSymbolTable( value=1, original_node=...), original_node=...)"""), + node=...), + Invariant( + description='Ints must not contain zero.', + body=textwrap.dedent("""\ + Not( + operand=IsIn( + member=Constant( + value=0, + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_ints', + original_node=...), + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Ints must not contain the number of strings.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_ints', + args=[ + FunctionCall( + name='len', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...)], + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_ints', + original_node=...)], + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Floats must not contain minus one.', + body=textwrap.dedent("""\ + Not( + operand=IsIn( + member=Constant( + value=-1.0, + original_node=...), + container=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_floats', + original_node=...), + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Strings must not contain an empty string.', + body=textwrap.dedent("""\ + Not( + operand=FunctionCall( + name='is_in_optional_strings', + args=[ + Constant( + value='', + original_node=...), + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...)], + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Strings must not contain dots.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='text', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...), + original_node=...), + condition=Not( + operand=FunctionCall( + name='contains_dot', + args=[ + Name( + identifier='text', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), + node=...), + Invariant( + description='Some ints must be unique.', + body=textwrap.dedent("""\ + FunctionCall( + name='ints_are_unique', + args=[ + Member( + instance=Name( + identifier='self', + original_node=...), + name='some_ints', + original_node=...)], + original_node=...)"""), + node=...), + Invariant( + description='Some strings must not be separators.', + body=textwrap.dedent("""\ + All( + generator=ForEach( + variable=Name( + identifier='text', + original_node=...), + iteration=Member( + instance=Name( + identifier='self', + original_node=...), + name='some_strings', + original_node=...), + original_node=...), + condition=Not( + operand=FunctionCall( + name='is_separator', + args=[ + Name( + identifier='text', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)"""), node=...)], serialization=None, description=None, @@ -496,6 +641,306 @@ UnverifiedSymbolTable( original_node=...), original_node=...)""")], node=..., + arguments_by_name=...), + UnderstoodMethod( + name='ints_are_unique', + verification=True, + visibility='PUBLIC', + arguments=[ + 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("""\ + Assignment( + target=Name( + identifier='seen', + original_node=...), + value=ListLiteral( + items=[], + original_node=...), + annotation=Index( + collection=Name( + identifier='List', + original_node=...), + index=Name( + identifier='int', + original_node=...), + original_node=...), + original_node=...)"""), + textwrap.dedent("""\ + For( + generator=ForEach( + variable=Name( + identifier='number', + original_node=...), + iteration=Name( + identifier='numbers', + original_node=...), + original_node=...), + body=[ + If( + branches=[ + IfBranch( + condition=IsIn( + member=Name( + identifier='number', + original_node=...), + container=Name( + identifier='seen', + original_node=...), + original_node=...), + body=[ + Return( + value=Constant( + value=False, + original_node=...), + original_node=...)], + original_node=...)], + default=None, + original_node=...), + ExpressionStatement( + expression=MethodCall( + member=Member( + instance=Name( + identifier='seen', + original_node=...), + name='append', + original_node=...), + args=[ + Name( + identifier='number', + original_node=...)], + 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, + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=AtomicTypeAnnotation( + identifier='str', + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=IsIn( + member=Name( + identifier='text', + original_node=...), + container=ListLiteral( + items=[ + Constant( + value='.', + original_node=...), + Constant( + value=',', + original_node=...), + Constant( + value=';', + original_node=...)], + original_node=...), + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='is_in_ints', + 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("""\ + Return( + value=IsIn( + member=Name( + identifier='number', + original_node=...), + container=Name( + identifier='numbers', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='is_in_optional_strings', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=AtomicTypeAnnotation( + identifier='str', + node=...), + default=None, + node=...), + Argument( + name='texts', + type_annotation=SubscriptedTypeAnnotation( + identifier='Optional', + subscripts=[ + SubscriptedTypeAnnotation( + identifier='Sequence', + subscripts=[ + AtomicTypeAnnotation( + identifier='str', + node=...)], + 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("""\ + If( + branches=[ + IfBranch( + condition=IsNone( + value=Name( + identifier='texts', + original_node=...), + original_node=...), + body=[ + Return( + value=Constant( + value=False, + original_node=...), + original_node=...)], + original_node=...)], + default=None, + original_node=...)"""), + textwrap.dedent("""\ + Return( + value=IsIn( + member=Name( + identifier='text', + original_node=...), + container=Name( + identifier='texts', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., + arguments_by_name=...), + UnderstoodMethod( + name='contains_dot', + verification=True, + visibility='PUBLIC', + arguments=[ + Argument( + name='text', + type_annotation=AtomicTypeAnnotation( + identifier='str', + node=...), + default=None, + node=...)], + returns=AtomicTypeAnnotation( + identifier='bool', + node=...), + description=Description( + document=..., + node=...), + contracts=Contracts( + preconditions=[], + snapshots=[], + postconditions=[]), + non_mutating=False, + body=[ + textwrap.dedent("""\ + Return( + value=IsIn( + member=Constant( + value='.', + original_node=...), + container=Name( + identifier='text', + original_node=...), + original_node=...), + original_node=...)""")], + node=..., arguments_by_name=...)], meta_model=MetaModel( description=Description( diff --git a/dev/tests/intermediate/test_type_inference.py b/dev/tests/intermediate/test_type_inference.py index c71c14bc8..cfe0d18c3 100644 --- a/dev/tests/intermediate/test_type_inference.py +++ b/dev/tests/intermediate/test_type_inference.py @@ -6023,6 +6023,63 @@ def some_func(lists: Sequence[Sequence[str]], texts: Sequence[str]) -> bool: ), ) + def test_is_in_list_of_wrong_type_fails(self) -> None: + self.expect_type_inference_to_fail( + body="""\ +@verification +def some_func(number: int, texts: Sequence[str]) -> bool: + return number in texts""", + expected_joined_message=( + "Expected the member to be of the type of the items of the list " + "List[str], but got: int" + ), + ) + + def test_is_in_str_of_non_str_fails(self) -> None: + self.expect_type_inference_to_fail( + body="""\ +@verification +def some_func(number: int, text: str) -> bool: + return number in text""", + expected_joined_message=( + "Expected the member to be a string as we check for a sub-string " + "in the container str, but got: int" + ), + ) + + def test_bytearray_as_member_of_in_fails(self) -> None: + self.expect_type_inference_to_fail( + body="""\ +@verification +def some_func(blob: bytearray, blobs: Sequence[bytearray]) -> bool: + return blob in blobs""", + expected_joined_message=( + "We do not support looking up a byte array with ``in``, but " + "the member is inferred to be bytearray. The targets disagree on " + "the comparison: Python compares the byte arrays byte by byte, " + "C# and Java compare the references of their ``byte[]``'s, while " + "Go can not compare ``[]byte`` with ``==`` at all. Please compare " + "the byte arrays explicitly instead, *e.g.*, in a for-loop." + ), + ) + + def test_json_value_as_member_of_in_list_fails(self) -> None: + self.expect_type_inference_to_fail( + body="""\ +@verification +def some_func(value: JSONValue, values: Sequence[JSONValue]) -> bool: + return value in values""", + expected_joined_message=( + "We do not support searching for a JSON-able value in a list " + "with ``in``, but the member is inferred to be JSONValue. " + "The targets disagree on the comparison: Python compares " + "the JSON-able values by value, while C#, Java and TypeScript " + "compare the references of their arrays and objects, and Go " + "panics when comparing them. Please contact the developers if " + "you need this feature." + ), + ) + def test_copy_of_list_of_sets_fails(self) -> None: self.expect_type_inference_to_fail( body="""\