diff --git a/dev/test_data/common_meta_models/enum.py b/dev/test_data/common_meta_models/enum.py
index 5f6ee2889..89bf6ddff 100644
--- a/dev/test_data/common_meta_models/enum.py
+++ b/dev/test_data/common_meta_models/enum.py
@@ -9,6 +9,19 @@ class Result(Enum):
Not_ok = "not-ok"
+@verification
+def negated(result: Result) -> Result:
+ """Negate :paramref:`result`, returning an enumeration literal."""
+ if result == Result.Ok:
+ return Result.Not_ok
+
+ return Result.Ok
+
+
+@invariant(
+ lambda self: negated(negated(self.some_result)) == self.some_result,
+ "Negating the result twice must give the result.",
+)
class Something:
some_result: Result
diff --git a/dev/test_data/intermediate/common_meta_models/enum/expected_symbol_table.txt b/dev/test_data/intermediate/common_meta_models/enum/expected_symbol_table.txt
index a82b4ee97..a99070324 100644
--- a/dev/test_data/intermediate/common_meta_models/enum/expected_symbol_table.txt
+++ b/dev/test_data/intermediate/common_meta_models/enum/expected_symbol_table.txt
@@ -73,7 +73,35 @@ SymbolTable(
name='some_result',
argument='some_result',
default=None)""")]),
- invariants=[],
+ invariants=[
+ Invariant(
+ description='Negating the result twice must give the result.',
+ body=textwrap.dedent("""\
+ Comparison(
+ left=FunctionCall(
+ name='negated',
+ args=[
+ FunctionCall(
+ name='negated',
+ args=[
+ Member(
+ instance=Name(
+ identifier='self',
+ original_node=...),
+ name='some_result',
+ original_node=...)],
+ original_node=...)],
+ original_node=...),
+ op='EQ',
+ right=Member(
+ instance=Name(
+ identifier='self',
+ original_node=...),
+ name='some_result',
+ original_node=...),
+ original_node=...)"""),
+ specified_for='Reference to ConcreteClass Something',
+ parsed=...)],
serialization=Serialization(
with_model_type=False),
description=None,
@@ -95,7 +123,34 @@ SymbolTable(
named_unions=[],
constants=[],
constants_by_name=...,
- verification_functions=[],
+ verification_functions=[
+ TranspilableVerification(
+ name='negated',
+ visibility='PUBLIC',
+ arguments=[
+ Argument(
+ name='result',
+ type_annotation=OurTypeAnnotation(
+ our_type='Reference to our type Result',
+ parsed=...),
+ default=None,
+ mutable=False,
+ parsed=...)],
+ returns=OurTypeAnnotation(
+ our_type='Reference to our type Result',
+ parsed=...),
+ description=DescriptionOfSignature(
+ summary='Negate result, returning an enumeration literal.',
+ remarks=[],
+ arguments_by_name=[],
+ returns=None,
+ parsed=...),
+ contracts=Contracts(
+ preconditions=[],
+ snapshots=[],
+ postconditions=[]),
+ parsed=...,
+ arguments_by_name=...)],
verification_functions_by_name=...,
meta_model=MetaModel(
description=None,
diff --git a/dev/test_data/main/cpp/expected/enum/expected_output/include/dummy/verification.hpp b/dev/test_data/main/cpp/expected/enum/expected_output/include/dummy/verification.hpp
index 0dfe6262e..5090ea2a5 100644
--- a/dev/test_data/main/cpp/expected/enum/expected_output/include/dummy/verification.hpp
+++ b/dev/test_data/main/cpp/expected/enum/expected_output/include/dummy/verification.hpp
@@ -212,6 +212,15 @@ class RecursiveVerification : public IVerification {
const std::shared_ptr& instance_;
}; // class RecursiveVerification
+// region Verification functions
+
+/// \brief Negate \p result, returning an enumeration literal.
+types::Result Negated(
+ types::Result result
+);
+
+// endregion Verification functions
+
} // namespace verification
/**@}*/
diff --git a/dev/test_data/main/cpp/expected/enum/expected_output/src/verification.cpp b/dev/test_data/main/cpp/expected/enum/expected_output/src/verification.cpp
index 40ac2d582..3b582d19c 100644
--- a/dev/test_data/main/cpp/expected/enum/expected_output/src/verification.cpp
+++ b/dev/test_data/main/cpp/expected/enum/expected_output/src/verification.cpp
@@ -37,6 +37,19 @@ Error::Error(
// endregion struct Error
+// region Verification functions
+
+types::Result Negated(
+ types::Result result
+) {
+ if (result == types::Result::kOk) {
+ return types::Result::kNotOk;
+ }
+ return types::Result::kOk;
+}
+
+// endregion Verification functions
+
namespace {
/**
@@ -45,7 +58,7 @@ namespace {
* A shape tells which checks apply to a value, see \ref ChecksOf.
*/
enum class Shape : std::uint32_t {
-
+ kSomething = 0
}; // enum class Shape
/**
@@ -67,11 +80,33 @@ struct Check {
// region Checks
+bool Something_0(
+ const void* value
+) {
+ const types::ISomething* that = (
+ static_cast(value)
+ );
+ return verification::Negated(
+ verification::Negated(
+ that->some_result()
+ )
+ ) == that->some_result();
+}
+
/**
* Give out the checks of the values of the \p shape.
*/
const std::vector& ChecksOf(Shape shape) {
switch (shape) {
+ case Shape::kSomething: {
+ static const std::vector checks = {
+ {
+ &Something_0,
+ L"Negating the result twice must give the result."
+ }
+ };
+ return checks;
+ }
default:
throw std::logic_error(
common::Concat(
@@ -199,16 +234,87 @@ std::unique_ptr Empty() {
return common::make_unique();
}
+/**
+ * Iterate over a single value which lives in the model.
+ */
+class OneIterator : public IIterator {
+ public:
+ OneIterator(
+ const void* value,
+ Shape shape
+ ) :
+ value_(value),
+ shape_(shape),
+ done_(true) {
+ // Intentionally empty.
+ }
+
+ void Start() override {
+ done_ = false;
+ }
+
+ void Next() override {
+ done_ = true;
+ }
+
+ bool Done() const override {
+ return done_;
+ }
+
+ const void* Value() const override {
+ return value_;
+ }
+
+ Shape ShapeOf() const override {
+ return shape_;
+ }
+
+ void AppendToPath(iteration::Path&) const override {
+ // Intentionally empty, as the value itself is the end of the path.
+ }
+
+ std::unique_ptr Clone() const override {
+ return common::make_unique(*this);
+ }
+
+ private:
+ const void* value_;
+ Shape shape_;
+ bool done_;
+}; // class OneIterator
+
+std::unique_ptr One(
+ const void* value,
+ Shape shape
+) {
+ return common::make_unique(value, shape);
+}
+
+std::unique_ptr Over_Something(
+ const types::ISomething& that,
+ bool
+) {
+ return One(&that, Shape::kSomething);
+}
+
/**
* Iterate over the values of the \p instance, dispatched on its runtime type.
*/
std::unique_ptr DispatchOnModelType(
- const types::IClass&,
- bool
+ const types::IClass& instance,
+ bool recursive
) {
- // NOTE (mristin):
- // The instances of no class have anything to verify.
- return Empty();
+ switch (instance.model_type()) {
+ case types::ModelType::kSomething:
+ return Over_Something(
+ dynamic_cast(instance),
+ recursive
+ );
+ default:
+ // NOTE (mristin):
+ // The instances of the other classes have nothing to verify.
+ return Empty();
+ }
}
// endregion Iteration over the values
diff --git a/dev/test_data/main/csharp/expected/enum/expected_output/dummy/verification.cs b/dev/test_data/main/csharp/expected/enum/expected_output/dummy/verification.cs
index 4eb7b4d56..43396adec 100644
--- a/dev/test_data/main/csharp/expected/enum/expected_output/dummy/verification.cs
+++ b/dev/test_data/main/csharp/expected/enum/expected_output/dummy/verification.cs
@@ -31,6 +31,20 @@ namespace dummy
///
public static class Verification
{
+ ///
+ /// Negate , returning an enumeration literal.
+ ///
+ public static Result Negated(
+ Result result
+ )
+ {
+ if (result == Result.Ok)
+ {
+ return Result.NotOk;
+ }
+ return Result.Ok;
+ } // public static Result Negated
+
///
/// Hash allowed enum values for efficient validation of enums.
///
@@ -56,6 +70,14 @@ private class Transformer
Our.ISomething that
)
{
+ if (!(
+ Verification.Negated(Verification.Negated(that.SomeResult)) == that.SomeResult))
+ {
+ yield return new Reporting.Error(
+ "Invariant violated:\n" +
+ "Negating the result twice must give the result.");
+ }
+
foreach (var error in Verification.VerifyResult(that.SomeResult))
{
error.PrependSegment(
diff --git a/dev/test_data/main/golang/expected/enum/expected_output/verification/verification.go b/dev/test_data/main/golang/expected/enum/expected_output/verification/verification.go
index ae435ae87..331e689ac 100644
--- a/dev/test_data/main/golang/expected/enum/expected_output/verification/verification.go
+++ b/dev/test_data/main/golang/expected/enum/expected_output/verification/verification.go
@@ -44,6 +44,16 @@ func (ve *VerificationError) PathString() string {
return ourreporting.ToGolangPath(ve.Path)
}
+// Negate result, returning an enumeration literal.
+func Negated(
+ result ourtypes.Result,
+) ourtypes.Result {
+ if result == ourtypes.ResultOk {
+ return ourtypes.ResultNotOk
+ }
+ return ourtypes.ResultOk
+}
+
// Verify `that` instance of [ourtypes.ISomething].
//
// You have to supply the callback `onError` to iterate over the errors.
@@ -56,6 +66,17 @@ func VerifySomething(
) (abort bool) {
abort = false
+ if !(
+ Negated(Negated(that.SomeResult())) == that.SomeResult()) {
+ abort = onError(
+ newVerificationError(
+ "Negating the result twice must give the result.",),
+ )
+ if abort {
+ return
+ }
+ }
+
abort = VerifyResult(
that.SomeResult(),
func(err *VerificationError) bool {
diff --git a/dev/test_data/main/java/expected/enum/expected_output/src/main/java/dummy/verification/Verification.java b/dev/test_data/main/java/expected/enum/expected_output/src/main/java/dummy/verification/Verification.java
index 0db0aa043..ae184e937 100644
--- a/dev/test_data/main/java/expected/enum/expected_output/src/main/java/dummy/verification/Verification.java
+++ b/dev/test_data/main/java/expected/enum/expected_output/src/main/java/dummy/verification/Verification.java
@@ -29,6 +29,17 @@
import dummy.visitation.AbstractTransformer;
public class Verification {
+ /**
+ * Negate {@code result}, returning an enumeration literal.
+ */
+ public static Result negated(
+ Result result) {
+ if (result == Result.OK) {
+ return Result.NOT_OK;
+ }
+ return Result.OK;
+ }
+
/**
* Hash allowed enum values for efficient validation of enums.
*/
@@ -56,6 +67,14 @@ public Stream transformSomething(
ISomething that) {
Stream errorStream = Stream.empty();
+ if (!(
+ negated(negated(that.getSomeResult())) == that.getSomeResult())) {
+ errorStream = Stream.concat(errorStream,
+ Stream.of(new Reporting.Error(
+ "Invariant violated:\n" +
+ "Negating the result twice must give the result.")));
+ }
+
errorStream = Stream.concat(errorStream,
Stream.of(that.getSomeResult())
.flatMap(Verification::verifyResult)
diff --git a/dev/test_data/main/python/expected/enum/expected_output/dummy/verification.py b/dev/test_data/main/python/expected/enum/expected_output/dummy/verification.py
index b65816a9b..1ea972f5d 100644
--- a/dev/test_data/main/python/expected/enum/expected_output/dummy/verification.py
+++ b/dev/test_data/main/python/expected/enum/expected_output/dummy/verification.py
@@ -62,6 +62,16 @@
Error = our_reporting.Error
+def negated(
+ result: our_types.Result
+) -> our_types.Result:
+ """Negate :paramref:`result`, returning an enumeration literal."""
+ # pylint: disable=all
+ if result == our_types.Result.OK:
+ return our_types.Result.NOT_OK
+ return our_types.Result.OK
+
+
class _Transformer(
our_types.AbstractTransformer[
Iterator[Error]
@@ -72,12 +82,12 @@ def transform_something(
self,
that: our_types.Something
) -> Iterator[Error]:
- # No verification has been defined for Something.
- return
- # For this uncommon return-yield construction, see:
- # https://stackoverflow.com/questions/13243766/how-to-define-an-empty-generator-function
- # noinspection PyUnreachableCode
- yield
+ if not (
+ negated(negated(that.some_result)) == that.some_result
+ ):
+ yield Error(
+ 'Negating the result twice must give the result.'
+ )
_TRANSFORMER = _Transformer()
diff --git a/dev/test_data/main/typescript/expected/enum/expected_output/src/verification.ts b/dev/test_data/main/typescript/expected/enum/expected_output/src/verification.ts
index 94e8c5ff6..9dadc4613 100644
--- a/dev/test_data/main/typescript/expected/enum/expected_output/src/verification.ts
+++ b/dev/test_data/main/typescript/expected/enum/expected_output/src/verification.ts
@@ -189,6 +189,18 @@ export class VerificationError {
}
}
+/**
+ * Negate `result`, returning an enumeration literal.
+ */
+export function negated(
+ result: OurTypes.Result
+): OurTypes.Result {
+ if (result == OurTypes.Result.Ok) {
+ return OurTypes.Result.NotOk;
+ }
+ return OurTypes.Result.Ok;
+}
+
/**
* Verify an instance of the model recursively or non-recursively (depending on the context).
*/
@@ -197,12 +209,17 @@ class Verifier
boolean, IterableIterator
> {
*transformSomethingWithContext(
- // eslint-disable-next-line @typescript-eslint/no-unused-vars
that: OurTypes.Something,
// eslint-disable-next-line @typescript-eslint/no-unused-vars
context: boolean
): IterableIterator {
- // No verification has been defined for Something.
+ if (!(
+ negated(negated(that.someResult)) == that.someResult
+ )) {
+ yield new VerificationError(
+ "Negating the result twice must give the result."
+ )
+ }
}
}
diff --git a/dev/test_data/parse/common_meta_models/enum/expected_symbol_table.txt b/dev/test_data/parse/common_meta_models/enum/expected_symbol_table.txt
index 3acff5aab..71ec8a1a8 100644
--- a/dev/test_data/parse/common_meta_models/enum/expected_symbol_table.txt
+++ b/dev/test_data/parse/common_meta_models/enum/expected_symbol_table.txt
@@ -57,7 +57,34 @@ UnverifiedSymbolTable(
node=...,
arguments_by_name=...,
body=...)],
- invariants=[],
+ invariants=[
+ Invariant(
+ description='Negating the result twice must give the result.',
+ body=textwrap.dedent("""\
+ Comparison(
+ left=FunctionCall(
+ name='negated',
+ args=[
+ FunctionCall(
+ name='negated',
+ args=[
+ Member(
+ instance=Name(
+ identifier='self',
+ original_node=...),
+ name='some_result',
+ original_node=...)],
+ original_node=...)],
+ original_node=...),
+ op='EQ',
+ right=Member(
+ instance=Name(
+ identifier='self',
+ original_node=...),
+ name='some_result',
+ original_node=...),
+ original_node=...)"""),
+ node=...)],
serialization=None,
description=None,
node=...,
@@ -65,7 +92,70 @@ UnverifiedSymbolTable(
methods_by_name=...)],
named_unions=[],
constants=[],
- verification_functions=[],
+ verification_functions=[
+ UnderstoodMethod(
+ name='negated',
+ verification=True,
+ visibility='PUBLIC',
+ arguments=[
+ Argument(
+ name='result',
+ type_annotation=AtomicTypeAnnotation(
+ identifier='Result',
+ node=...),
+ default=None,
+ node=...)],
+ returns=AtomicTypeAnnotation(
+ identifier='Result',
+ node=...),
+ description=Description(
+ document=...,
+ node=...),
+ contracts=Contracts(
+ preconditions=[],
+ snapshots=[],
+ postconditions=[]),
+ non_mutating=False,
+ body=[
+ textwrap.dedent("""\
+ If(
+ branches=[
+ IfBranch(
+ condition=Comparison(
+ left=Name(
+ identifier='result',
+ original_node=...),
+ op='EQ',
+ right=Member(
+ instance=Name(
+ identifier='Result',
+ original_node=...),
+ name='Ok',
+ original_node=...),
+ original_node=...),
+ body=[
+ Return(
+ value=Member(
+ instance=Name(
+ identifier='Result',
+ original_node=...),
+ name='Not_ok',
+ original_node=...),
+ original_node=...)],
+ original_node=...)],
+ default=None,
+ original_node=...)"""),
+ textwrap.dedent("""\
+ Return(
+ value=Member(
+ instance=Name(
+ identifier='Result',
+ original_node=...),
+ name='Ok',
+ original_node=...),
+ original_node=...)""")],
+ node=...,
+ arguments_by_name=...)],
meta_model=MetaModel(
description=None,
version='dummy',