Hacker News Reader

Comment by whitten | Hacker News Reader

How common in the industry is the use of 'invar' to signal an invariant, 'ensure' to signal a postcondition, and 'require' to signal a pre-condition ?

View on HN

Eiffel uses 'ensure' and 'require' for these meanings.

.NET Code Contracts (may it rest in peace) uses 'Ensures' and 'Requires' for these meanings as well.

what about for invariants ?

Eiffel uses 'invariant', and .NET Code Contracts uses 'Invariant'.

assert() is pretty much the industry standard for invariants, right? they're usually evaluated at runtime but it should be perfectly possible for a static analysis tool to "evaluate" them statically.

assert() by itself is typically not the same as "defining an invariant". An invariant is an expression which should be true for the whole life-time of the block/function/program/anything, but assert() only defines an assertion at a specific point.

Plus, assert() is commonly used for runtime checks, not static analysis.

You can use static_assert but compilers observe assert already. assume is another commonly used invariant.

“An invariant is an expression which should be true for the whole life-time of the block/function/program/anything”

It should hold at both entry and exit of a block, but practically always doesn’t for the entire block.

ACSL (https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Langu...) for C, which is based on JML (https://en.wikipedia.org/wiki/Java_Modeling_Language) for Java, both use 'requires' for preconditions, 'ensures' for postconditions, and 'invariant' for invariants. Some invariants are also written as assertions ('assert').

Reply on news.ycombinator.com