(Generalmente) come specificare l'azione asincrona con effetti collaterali usando equazioni logiche

Question

Supponi di avere questa sequenza di chiamate di funzione:

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

E dillo fn2 era asincrono e causato tutti i tipi di effetti collaterali:

var globalPacketCounter = 0

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

Qualcosa di complicato e con implementazione sconosciuta, sebbene sia possibile sminuirlo per determinare i tipi di comportamento che ha e leggere documenti, ecc.

Mi chiedo, in generale, cosa puoi fare per incorporarlo in un modello di controllo del modello o di valutazione simbolica o altro sistema di verifica come Hoare Logic o qualcosa del genere. Vorrei farlo:

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

Una sorta di affermazione logica. La domanda è (parzialmente) se questo è un approccio valido; cioè, trattare il fn2() come un singolo passaggio in un'equazione logica. La parte principale della domanda è però come farlo generalmente. Vorrei sostanzialmente trattare tutto come funzioni logiche, ma non sono sicuro di come applicarlo al caso "Async con effetti collaterali".