I have this datatype newtype Dimension a b = MkDimension b Whenever it is properly formatted (e.g. satisfies the format constraint), I want to derive a set of classes. I do not want a Dimension which ...

I read that a function f is equivariant if f(P(x)) = P(f(x)) where P is a permutation So to check what means equivariant and permutation invariant I wrote the following code import torch import torch....

Say I have some simple struct, eg: struct SomeStruct { things: Vec<usize> recent_thing: Option<usize> } I'm trying to assert some invariant on this struct. For example, maybe we want ...

I wonder how to build correct hierarchy and where to cover invariants. There are following entities: Faculty, Course, Student, Teacher. Faculty consists of Courses. Course cannot exist without Faculty....

I've got a bit of a theoretical question surrounding DDD and aggregates. It really boils down to this: Yes, we all know that within an aggregate everything must stay consistent. But does that mean ...

method search(a: array<int>) returns (i : int) requires a.Length > 1 && a[0] == a[a.Length-1] ensures 0 <= i < a.Length-1 && a[i] >= a[i + 1] { i := ......; ...

The following code is the answer I came up with for the following problem. However, there are two main errors. By the way, this problem is problem 17 in Chapter 13 of the book "PROGRAM PROOFS&...

I've been reading up on AA-Trees. One of their invariants is that every non-leaf node has two children. How can that work whenever the total element count happens to not be one less than a power of ...

When using non-type template parameters, the non-type parameter must be 'structural' per the C++ standard. Classes with private data members are not structural. However, sometimes it is convenient to ...

I am struggling with Dafny's syntax, and I get an error that I don't know how to deal with. Here is the code: function pow(base: int, exp: nat): int { if exp == 0 then 1 else base * pow(base, exp -...

I have a contract in which I am emitting an event when a certain condition is met enum Type { One, Two } function _someFunc() internal { ... if (someVar != 0) { emit Abstain(Type.One) } ...

I would like to determine if there is a way to follow the type state pattern but allow invariants if there is an alternative. Suppose I have a builder pattern for a wrapper struct around a trait. ...

Our development team is currently exploring effective patterns to handle situations where concurrent updates might lead to data inconsistencies. We adhere to Domain-Driven Design (DDD) principles, ...

I need to implement an AutoDocs class that will contain information about the license plate number and driver's full name. It is necessary to implement the class with the following invariants: the ...

I'm working on a Dafny program that finds the maximum element in a sequence of integers. The method Strictmax should return the maximum element and its index. If the maximum element is not unique, the ...