3 ms·
Model checking is a pretty cool idea, except you really need to have it built into the language rather than as an annotation or seperate system. Maintaining a
by vegas 14y ago
Model checking is a pretty cool idea, except you really need to have it built into the language rather than as an annotation or seperate system. Maintaining a seperate model just gives you two places to make typos.
- jasomill 14y agoConversely, it gives two opportunities to avoid not only typos, but "thinkos". Simple declarative definitions can often define the results of complicated algorithms. Algebraic topology is actually a nice example. Presumably a surface has no holes if and only if any loop on the surface can be contracted to a point (given appropriate definitions of all these terms, of course). While this equivalence is easy to verify, def has_holes(s): for c in all_loops(s): try: contract(c) except: return True return False isn't an effective algorithm (e.g., "all loops" is an infinite set). But algebraic topology shows how one might instead reduce the problem to computationally tractable linear algebra. Suppose, then, that you've implemented an (presumably nontrivial and therefore error-prone) algorithm to carry out this reduction. Then your patently correct constraint on all loops might be a useful source of tests. (disclaimer: I know nothing at all about computational algebraic topology, except that it's fascinating. So please take my example with an unbounded grain of salt.)
- Darmani 14y agoIt's actually quite simple: A surface has no holes if its Euler Characteristic is 2. Since 3D objects are already expressed in a triangulated form, this is quite easy to check.