Ancestors

Written by Per Vognsen on 2024-12-29 at 16:36

I was idly thinking about verification for mutation-based linked structures. A nice thing about bidirectional/doubly-linked structures is that you have an inverse function to work with as opposed to merely an injectivity and surjectivity property, so you don't need a Cantor-Schröder-Bernstein-like argument to pass between the two. More prosaically this also lets you catch functional correctness/memory corruption bugs by checking local invariants like next[prev[x]] = x and prev[next[x]] = x.

=> More informations about this toot | More toots from pervognsen@mastodon.social

Toot

Written by Per Vognsen on 2024-12-29 at 17:02

I think this would mostly help in formal verification if you're relying on model checking of data-type invariants or something like that. If you're doing deductive verification with a proof assistant I don't think it would make really help (or hurt) the proof if your data structure carries an inverse witness as opposed to an injectivity/surjectivity property.

=> More informations about this toot | More toots from pervognsen@mastodon.social

Descendants

Written by Wolf480pl on 2024-12-29 at 19:23

@pervognsen reminds me of how in TLA+, inveraints are much faster to model-check than temporal properties. Would the difference between "not exists two list elements with the same next" and "next[prev[x]] = x" be of similar magnitude?

=> More informations about this toot | More toots from wolf480pl@mstdn.io