A multiparty multi-session logic
Laura Bocchi, Romain Demangeon, Nobuko Yoshida
-
update (improved version of the paper, e.g., with corrected
typos)
-
full report
-
On validating recursion: to validate a recursive process against a recursive assertion: (1) the
recursive assertion is unfolded, with the unfolding being a refinement of
the original assertion, (2) by refinement rule for
processes, say [Conseq], the original recursive process is validated against the unfolding,
(3) after applying rule
[Rec] the validation proceeds normally until a recursive call, (4) to
handle the recursive call the local assertion is unfolded again, rule
[Conseq] is used as before, and finally rule [Var] is applied.
It is the clause by which L_i[e/x] must be well-asserted that ensures
the invariant is not violated and that the new iteration is consistent.
For a full example with recursion with no state see here (page 22, Example 5.7). Adding state does not
add other challenges than the redefinition of well-assertedness.