In JavaScript I want to create a log function:
function log(string) {
console.log(string)
}
Obviously this causes side effects; it prints to the screen. And I have no control over its implementation. Basically, I just trust that it works.
But I wonder what I can do to incorporate something like this into a formal verification system. Maybe I make it into some sort of Monad, but I have a hard time understanding how Monads work. It seems that I want to say something about an abstract global state
which goes from one state to another, as in
log(string) = state -> state'
But I'm not really sure what I can do from there, or what this even gives me. I would like to say something about how this function is verified
, but I'm not sure what that would take, if it is just tests of some degree, or if I can write a specification that doesn't require understanding the complete implementation.
Please let me know what I can do with this situation, how I can take this log
function and integrate it into an otherwise pure verification system.