4 ms·
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 ?
by whitten 6y ago
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 ?
- rhencke 6y agoEiffel uses 'ensure' and 'require' for these meanings. .NET Code Contracts (may it rest in peace) uses 'Ensures' and 'Requires' for these meanings as well.
- whitten 6y agowhat about for invariants ?
- rhencke 6y agoEiffel uses 'invariant', and .NET Code Contracts uses 'Invariant'.
- skrebbel 6y agoassert() 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.
- judofyr 6y agoassert() 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.
- nimmer 6y agoPlus, assert() is commonly used for runtime checks, not static analysis.
- rurban 6y agoYou can use static_assert but compilers observe assert already. assume is another commonly used invariant.
- Someone 6y ago“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.
- dhekir 6y agoACSL (https://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language 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 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').