On Sunday, 5 June 2022 at 14:24:39 UTC, Ali Çehreli wrote:
void add(int i) { // <-- Both arrays always same size a ~= i; b ~= i * 10; }void foo() { assert(a.length == b.length); // <-- Invariant check // ... }
Maybe it would help if we can agree that this assert ought to be statically proven to hold and the assert would therefore never be evaluated in running code. Emitting asserts is just a sign of failed statical analysis (which is common, but that is the most sensible interpretation from a verification viewpoint).
The purpose of asserts is not to test the environment. The purpose is to "prove" that the specified invariant of the function holds for all legal input.
It follows that the goal of an assert is not to test if the program is in a legal state!
I understand why you say this, but if this was the case then we could not remove any asserts by statical analysis. :-/
