Stream: general

Topic: meaning of "invariant"


Jake Goulding (Nov 20 2018 at 17:10, on Zulip):

not clear what this method's invariants are - i.e. when is the unsafe code actually not UB

I feel like this isn't a proper English use of the word "invariant", but it seems consistent in the compiler circles. What does "invariant" mean when it doesn't mean "something that doesn't change"?

/cc @eddyb

eddyb (Nov 20 2018 at 17:11, on Zulip):

it means precondition. it's always true (in the absence of UB), making it an invariant :P

eddyb (Nov 20 2018 at 17:11, on Zulip):

maybe a stretch but I think it makes sense on some level

QuietMisdreavus (Nov 20 2018 at 17:12, on Zulip):

sometimes in computing an "invariant" is something you can assume to be true at all times, or at least throughout a given function/module/scope/etc

eddyb (Nov 20 2018 at 17:13, on Zulip):

that's more eloquent than what I said, but I agree, that's how I see it as well :D

RalfJ (Nov 20 2018 at 17:16, on Zulip):

invariant != precondition

RalfJ (Nov 20 2018 at 17:16, on Zulip):

so I think "method's precondition" would be a better term here

eddyb (Nov 20 2018 at 17:16, on Zulip):

words are hard :(

RalfJ (Nov 20 2018 at 17:17, on Zulip):

true^^

RalfJ (Nov 20 2018 at 17:17, on Zulip):

to call it an invariant, you should at least have it both as pre- and postcondition

RalfJ (Nov 20 2018 at 17:18, on Zulip):

that's still stretching the term IMO, I assoicate invariants with something that several threads can rely on and that can be shared because it is true forever, but that may be just my niche^^

Jake Goulding (Nov 20 2018 at 17:23, on Zulip):

I think the combination of all this was useful, thank you.

Jake Goulding (Nov 20 2018 at 17:24, on Zulip):

It feels like if something is an invariant, you wouldn't actually perform a check for it, whereas I feel like pre/post conditions are actual checks in the code

Jake Goulding (Nov 20 2018 at 17:25, on Zulip):

e.g. an invariant of &str is that it's UTF-8. I might use a pre/post condition to enforce that at some boundary

Jake Goulding (Nov 20 2018 at 17:25, on Zulip):

and if I fail to enforce an invariant, then I might open myself up to UB

QuietMisdreavus (Nov 20 2018 at 17:32, on Zulip):

yeah, violation of invariants is where you start getting into awkward bugs, UB, etc

RalfJ (Nov 20 2018 at 18:26, on Zulip):

There is one particular invariant violating which is instantenous UB, the "validity invariant" as I call it

RalfJ (Nov 20 2018 at 18:26, on Zulip):

that's because the compiler knows about it

RalfJ (Nov 20 2018 at 18:27, on Zulip):

violating, for example, the loop invariant of your quicksort won't give you UB. So I wouldnt connect invariants and UB directly at all

RalfJ (Nov 20 2018 at 18:27, on Zulip):

invariants are just both useful for specification and for verification of programs

Jake Goulding (Nov 20 2018 at 18:30, on Zulip):

right, which is why I said "might open myself up to UB"

rkruppe (Nov 20 2018 at 18:38, on Zulip):

one thing to keep in mind is that all invariants, preconditions, postconditions, proof obligations, etc. are in service of a particular goal. e.g. the quicksort loop invariant is for the functional correctness of the sorting, while in rust development we typically implicitly refer to memory safety (or a particular aspect of it) as the goal. mixing these unstated contexts tends to cause confusion

Jake Goulding (Nov 20 2018 at 18:44, on Zulip):

unstated contexts tends to cause confusion

Sounds true in every case :smile_cat:

RalfJ (Nov 20 2018 at 18:51, on Zulip):

we also often rely on functional correctness for memory safety, so these contexts aren't even all that separate^^

Last update: Nov 22 2019 at 00:30UTC