1
$\begingroup$

I have read that when programming it is good to identify relations -- invariants -- that should hold true throughout the program, and it is good to insert assertions throughout the code to check that the invariants are maintained.

I can see how programs that involve mathematics can have invariants, i.e., some mathematical relation must be true throughout the code's manipulations.

Are there invariants in non-mathematical problems?

Are there invariants in text processing programs?

Suppose the processing problem is to transform one terminology to another. Are there invariants in this problem?

Let's take a specific example. The first vocabulary has an item TYPE whose value is A, B, C, or D. The second vocabulary has an item airIndicator whose value is Civil, Joint, Military, or Private. After reading the documentation it is determined that the mapping is as follows:

A maps to Civil.
B maps to Joint.
C maps to Military.
D has a different meaning than Private so whenever D is encountered an error should be generated.

Here is pseudocode to do the mapping:

if TYPE = 'A' then "Civil"
else if TYPE = 'B' then "Joint"
else if TYPE = 'C' then "Military"
else if TYPE = 'D' then error("No mapping for D")
else error("Invalid TYPE value")

Is there an invariant in that mapping?

When you write text processing programs do you identify invariants and then insert assertions throughout your code to check that the invariants are maintained?

$\endgroup$

1 Answer 1

3
$\begingroup$

Yes. One can find invariants in any program. The notion is well-defined and meaningful in any program (whether it is useful in practice is a different question).

Normally identifying invariants is most useful whenever there are loops (or recursion). Straight-line code is usually easy to reason about, so there is usually no need to identify invariants, but when we have loops (or recursion), that's more challenging to reason about and so it can sometimes be more useful to identify invariants.

To learn more, see https://en.wikipedia.org/wiki/Loop_invariant, , and https://en.wikipedia.org/wiki/Hoare_logic.

$\endgroup$
1
  • 2
    $\begingroup$ Ah! Excellent. That is a key point, "Straight-line code is easy to reason about, so there is usually no need to identify invariants, but when we have loops (or recursion) ... useful to identify invariants." Thank you @D.W.! $\endgroup$ Apr 30 at 19:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.