(Generally) How to specify asynchronous action with side effects using logic equations Say you have this function call sequence:

function all() {
  fn1()
  fn2()
  fn3()
}


And say that fn2 was asynchronous and caused all kinds of side effects:

var globalPacketCounter = 0

function fn2() {
  var httpRequest = ...
  httpRequest.on('data', function(){
    globalPacketCounter++
  })
  drawGraphicsToDisplay()
  ...
}


Something complicated and with unknown implementation, though you can probe it to determine the types of behavior it has, and read docs, etc.

I'm wondering, generally speaking, what you can do to incorporate this into a model checking or symbolic evaluation system, or other verification system like Hoare logic or something. I would like to do this:

all() =
  /\ fn1() in state 1
  /\ fn2() in state 2
  /\ fn3() in state 3
  /\ complete = true in state 4


Some sort of logical statement. The question is (partially) if this is a valid approach; that is, treating the fn2() as a single step in a logic equation. The main part of the question though is how to generally do this. I would like to basically treat everything as logic functions but am not sure how to apply it to the "async with side effects" case.
One way to model your example is through program graphs. (See chapter 2 in Principles of Model Checking.) What you can do is model all() as one program, which synchronizes on action 'data' with another program that runs concurrently to all(), let's call it listen(). listen() will have an initial state where it waits until it can synchronize with the all() on action 'data'.

Once you have these two models (or more for bigger examples) you can interleave them, which is a construction that contains all the possible states. Program graph interleaving also preserves shared variables (so globalPacketCounter will be updated correctly) unlike interleaving on transition systems. Though I would be careful about them, since atomicity is not implicit in the models. You can read more about critical actions in section 2.2.2. of the book.

After interleaving of PGs you construct a transition system, which you can transform to a logical equation. And there you have it.