Earlier quoted context omitted.
> Then imagined it is. Only in the most pedantic and useless sense of the term. Asserts are not just some random imagination, they are added based on the program's specifications and expected/desired functionality and constraints. The CS term for those kind of constraints are "invariants", and asserts are a way to be notified if those invariants are violated. > unless you make them become real. Only there are no assu…
> The CS term for those kind of constraints are "invariants", and asserts are a way to be notified if those invariants are violated. An “invariant” is a function of the process state whose value remains constant (hence “invariant”) in spite of changes to the process state. Perhaps you meant “precondition” or “postcondition”? > Only there are no assurances for that. If the invariants in your program were somehow guara…
No, I meant invariant. An invariant is something that is supposed to hold true, not just things that are guaranteed to hold true (e.g. a constant that can't ever change anyway). That's why the need for assertions to check that invariants hold.
From Wikipedia:
"In computer science, an invariant is a condition that can be relied upon to be true during execution of a program, or during some portion of it. It is a logical assertion that is held to always be true during a certain phase of execution. (...) Programmers often use assertions in their code to make invariants explicit."
Preconditions and postconditions are similar in concept, but are supposed/wanted to hold true before (pre) or after (post) a method runs.
>I absolutely don't need asserts. An assert merely describes what you want, but that's useless to me, unless you establish a relation between what you want and what your program actually does - with proof.
Well, asserts weren't created specifically for you. Feel free not to use them.
They are useful to me, and assuming from their widespread use, others, even if they don't formally prove the program does 100% that it needs to (which nobody expected them to anyway).
Until we all program in Coq or similar, they will be useful for all kinds of checks. A correct program is a spectrum, not a binary option.
>Of course. Assertions are expected to always be true.
No, they are also expected to be false -- that's why we add assertion statements to check whether our assertions hold. But we're splitting hairs twice or three times here.