How can the `log` function be used for formal verification
https://softwareengineering.stackexchange.com/questions/388364
-
21-02-2021 - |
Domanda
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.
Soluzione
Formal verification needs to have a goal: what precisely do you want to prove?
For example, if you merely want to prove that a program terminates than you can treat built-in functions like console.log()
as a given and declare an axiom that the function terminates. You can then use that axiom to prove whether user-defined functions that call console.log()
also terminate.
If you want to prove more complicated properties such as multiple outputs are written in a specific order, then using things like an IO monad could be helpful. The monad properties themselves are not useful here, simply because JavaScript has no such built-in concept. Instead, it would be useful to model every function as taking a “state of the world” token as an implicit parameter. Each token can be used exactly once; and I/O functions consume a token and produce an new token. You can then use data flow analysis, SSA, or something like C++'s or Rust's ownership system to track these tokens and consequently the ordering of operations.
For many other kinds of formal verification, for example when trying to address the question whether a function returns the correct result, you can simply ignore console.log()
as it returns no value.
So: first determine your goals, then find an appropriate formal verification framework, then (if necessary) find a way to model this function within your formal semantics.