Instead of a code library author providing both the library code and the specification and the proof of correctness according to the specification, we have the user of the library write the formal specification according to how the user understands the library to work: how the user is using the library in the user's code. Then, automated or manual theorem proving to see if the user's understanding matches up with what the library actually does.
Theorem proving as a tool for code understanding.
Requires open source, and libraries be written in a way amenable to theorem proving.
No comments :
Post a Comment