3

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.

4

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.

1
  • That was key for me, knowing that you can define an axiom like that. Thank you. Mar 12 '19 at 3:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.