Interestingly, allowing the internal block structure can increase the difficulty of doing logic on the code to the point where building proof tools become NP-complete (or at least insanely hard). This is relevant if you're tying to use static analysis tools, not just if you're trying to prove theoroms (;-)) --dave (who proveth not, but analyzeth a lot) c-b
Copyright © 2017, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds