3 ms·

In your experience, what properties makes a good invariant, and how does one find them in practice for a new system?

_a_a_a_ 3y ago
Anything that must be true. Taking a sqrt of a float f? Assert f is positive. Can't read from a closed file? Assert the file is open. The classic, transferring cash from account a to account b? Assert that a+b before = a+b after. Object should be in a given state after a certain method is invoked? Assert it. It is possible to assert some invariants at compile time using strong typing, that's pretty useful too and I'm learning to do that myself (nothing clever, it's just thinking of 2 different classes to represent 2 different states, or use phantom types). More complex compile-time assertions are possible using dependent types, but that's out of my pay grade at the moment. Edit: assertions can come before and/or after the thing is done. Technically if you're checking before then it's a pre-condition you want to ensure, if it's after, then it's a post-condition check you're doing. Let's take the square root example, and assume that you're actually implementing a sqrt function, not just calling a library function. The pre-condition is as before, that f must be positive, and the post-condition is that for the result r, r*r = f (if you've successfully taken the square root of a thing, squaring it should get you back to the original value, or at least very, very close). HTH
- qazxcvbnm 3y ago
  I have to say, the cases that you raise (e.g. square root function) seem quite a different nature than the systems that the author appears to consider (e.g. distributed garbage collector). Your considerations appear to enumerate some types of checks one would use in unit testing. As for taking as invariants anything that must be true, in a system very many things are true, and the most part of them would be utterly uninteresting. Understanding the process that one would use to pick insightful ones is rather the art which I'm intrigued by.
  - _a_a_a_ 3y ago
    Yes. I was trying to give you an easy introduction to the idea. And which are you more likely to be writing, a distributed garbage collector or a single-core library/application? Realistically, very much the latter. And if the former, much of that system will be made up of stuff running strictly on single cores, to which plain bog-standard assertions will be just as useful. > one would use to pick insightful ones is rather the art which I'm intrigued by. Well, it's not really an art, it's more straightforward than that (edit: think of them as basic sanity checks, not anything deep or profound), but if my overview of the idea isn't helpful you need to provide a more concrete example to discuss. I think your question as it stands is too ill-defined.
- layer8 3y ago
  Your examples are more postconditions than invariants. Invariants are usually assertions for a given state object that always hold for that object throughout its lifetime. For example, a mutable list implementation based on a resizable array might have the invariant that the value of the length field is always less than or equal the current array size. Or for a loop invariant, that a certain predicate on the state mutated in the loop is true for all iterations of the loop.
  - _a_a_a_ 3y ago
    A postcondition is an invariant[1]. Invariants must hold at the end of the operation however the intervening inconsistent state must be invisible (effectively, be atomic). They often are (maybe always are?) violated within the operation but must be patched up by the end. [1] Edit: no, a postcondition expresses an invariant in code - but that's a terminology thing. We may be disagreeing just on terminology here.
    - rcxdude 3y ago
      precondition is something which must be true before some code executes postcondition is something which must be true after some code executes invariant is both: something which must be true both before and after some code executes. So it's the other way around. An invariant is a postcondition, but a postcondition is not necessarily an invariant. (you can check all three with assertions, but they will generally exist whether you check them or not)
      - _a_a_a_ 3y ago
        A reasonable distinction. I accept it.

Anything that must be true. Taking a sqrt of a float f? Assert f is positive. Can't read from a closed file? Assert the file is open. The classic, transferring cash from account a to account b? Assert that a+b before = a+b after. Object should be in a given state after a certain method is invoked? Assert it. It is possible to assert some invariants at compile time using strong typing, that's pretty useful too and I'm learning to do that myself (nothing clever, it's just thinking of 2 different classes to represent 2 different states, or use phantom types). More complex compile-time assertions are possible using dependent types, but that's out of my pay grade at the moment. Edit: assertions can come before and/or after the thing is done. Technically if you're checking before then it's a pre-condition you want to ensure, if it's after, then it's a post-condition check you're doing. Let's take the square root example, and assume that you're actually implementing a sqrt function, not just calling a library function. The pre-condition is as before, that f must be positive, and the post-condition is that for the result r, r*r = f (if you've successfully taken the square root of a thing, squaring it should get you back to the original value, or at least very, very close). HTH

qazxcvbnm 3y ago
I have to say, the cases that you raise (e.g. square root function) seem quite a different nature than the systems that the author appears to consider (e.g. distributed garbage collector). Your considerations appear to enumerate some types of checks one would use in unit testing. As for taking as invariants anything that must be true, in a system very many things are true, and the most part of them would be utterly uninteresting. Understanding the process that one would use to pick insightful ones is rather the art which I'm intrigued by.
- _a_a_a_ 3y ago
  Yes. I was trying to give you an easy introduction to the idea. And which are you more likely to be writing, a distributed garbage collector or a single-core library/application? Realistically, very much the latter. And if the former, much of that system will be made up of stuff running strictly on single cores, to which plain bog-standard assertions will be just as useful. > one would use to pick insightful ones is rather the art which I'm intrigued by. Well, it's not really an art, it's more straightforward than that (edit: think of them as basic sanity checks, not anything deep or profound), but if my overview of the idea isn't helpful you need to provide a more concrete example to discuss. I think your question as it stands is too ill-defined.
layer8 3y ago
Your examples are more postconditions than invariants. Invariants are usually assertions for a given state object that always hold for that object throughout its lifetime. For example, a mutable list implementation based on a resizable array might have the invariant that the value of the length field is always less than or equal the current array size. Or for a loop invariant, that a certain predicate on the state mutated in the loop is true for all iterations of the loop.
- _a_a_a_ 3y ago
  A postcondition is an invariant[1]. Invariants must hold at the end of the operation however the intervening inconsistent state must be invisible (effectively, be atomic). They often are (maybe always are?) violated within the operation but must be patched up by the end. [1] Edit: no, a postcondition expresses an invariant in code - but that's a terminology thing. We may be disagreeing just on terminology here.
  - rcxdude 3y ago
    precondition is something which must be true before some code executes postcondition is something which must be true after some code executes invariant is both: something which must be true both before and after some code executes. So it's the other way around. An invariant is a postcondition, but a postcondition is not necessarily an invariant. (you can check all three with assertions, but they will generally exist whether you check them or not)
    - _a_a_a_ 3y ago
      A reasonable distinction. I accept it.