Paper deep dive
A Reversible Semantics for Janus
Ivan Lanese, Germán Vidal
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 7/21/2026, 12:58:17 AM
Summary
The paper addresses the lack of reversibility in the small-step semantics of the Janus programming language, which previously lost information during forward execution (violating the Loop Lemma). The authors propose a novel small-step semantics that is fully reversible by utilizing a program counter and a stack to track subcomputations, allowing for both forward execution and backward inversion of steps without retaining a full history log.
Entities (8)
Relation Signals (6)
Novel Small-Step Semantics → usesmechanism → Program Counter
confidence 95% · our proposal is based on replacing in the configurations the component with the code to be executed with a 'program counter'
Novel Small-Step Semantics → satisfiesproperty → Loop Lemma
confidence 94% · We present here a novel small-step semantics which is actually reversible... satisfying the Loop Lemma
Novel Small-Step Semantics → usesmechanism → Stack
confidence 93% · we introduce a simple small-step semantics for Janus that uses a stack to model subcomputations
Janus → hasproblem → Irreversible Small-Step Semantics
confidence 92% · its current small-step semantics ... is not reversible, since it loses information while computing forwards.
Janus → hassemantics → Big-Step Semantics
confidence 90% · The semantics of [20, 21, 23] follows the so-called big-step style
Reversible Computation → isgovernedby → Landauer's principle
confidence 85% · according to Landauer’s principle [10], the erasure of one bit of information in an irreversible computation necessarily dissipates a minimum amount of heat.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it loses information while computing forwards. E.g., it does not satisfy the Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where a small-step semantics is commonly used. We present here a novel small-step semantics which is actually reversible, while remaining equivalent to the previous one. It involves the non-trivial challenge of defining a semantics based on a "program counter" for a high-level programming language.
Tags
Links
- Source: https://arxiv.org/abs/2602.16913v2
- Canonical: https://arxiv.org/abs/2602.16913v2
Trouble viewing inline? Open PDF directly →
Full Text
161,807 characters extracted from source content.
Expand or collapse full text
11institutetext: Olas Team, University of Bologna & Inria - Université Côte d’Azur, Bologna, Italy 22institutetext: VRAIN, Universitat Politècnica de València, Valencia, Spain A Reversible Semantics for Janus Ivan Lanese Germán Vidal Abstract Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it loses information while computing forwards. E.g., it does not satisfy the Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where a small-step semantics is commonly used. We present here a novel small-step semantics which is actually reversible, while remaining equivalent to the previous one. It involves the non-trivial challenge of defining a semantics based on a “program counter” for a high-level programming language. 1 Introduction Reversible computation has emerged as a promising framework for addressing a number of limitations of current computing paradigms [1]. On the one hand, according to Landauer’s principle [10], the erasure of one bit of information in an irreversible computation necessarily dissipates a minimum amount of heat. In contrast, Bennett [2] showed that, theoretically, a reversible computation—where no information is discarded—can be performed with less heat dissipation than an irreversible one. Thus, the development of reversible circuits could represent a revolution in reducing the energy consumption of large computing centers. At the programming level, the Janus language [12] represents one of the first attempts to formalize a reversible programming language. Janus performs (deterministic) computations in both forward and backward directions. The development of reversible programming languages like Janus may provide an excellent opportunity to explore the relationship between logical reversibility, energy conservation, and computational expressiveness. A formal semantics for the language was first presented in [20, 21, 23]. Unfortunately, the semantics of [20, 21, 23] follows the so-called big-step style, which is less appropriate for some applications, e.g., modeling stepwise execution, program debugging, designing an abstract machine for the language, modeling concurrency and interleaving (for a future concurrent extension of Janus), analyzing non-termination, etc. Recently, [9] has introduced a small-step semantics for Janus that is more appropriate for the applications mentioned above. This semantics employs contexts to identify the next statement to be executed. In particular, the configurations include the code to be executed, which is transformed as execution progresses. These features, however, make the semantics irreversible. E.g., a Janus conditional statement of the form “e1s2e2 if~e_1~ then~ skip~ else~s_2~ fi~e_2” is reduced to skip when the guard e2e_2 is true (in [9] the then branch is first reduced to skip when the condition e1e_1 is true before evaluating the guard). This step, however, is irreversible: we cannot obtain “e1s2e2 if~e_1~ then~ skip~ else~s_2~ fi~e_2” from skip. Janus is thus reversible at the level of programs (or statements), in the sense that we can execute any program backwards, recovering input data from results, but not at the level of semantics, since single reduction steps cannot be inverted. This is in strike contrast with the semantics of calculi and languages for concurrency, where the Loop Lemma ensures that single steps have a reverse, e.g., in RCCS [4, Lemma 6], CCSK [13, Proposition 5.1], or reversible Erlang [11, Lemma 11]. This prevents applications such as reversible debugging, the definition of backtracking strategies, etc. Therefore, in this work, we tackle the definition of a reversible small-step semantics for Janus. First, we introduce a simple small-step semantics for Janus that uses a stack to model subcomputations, and which is equivalent to previous semantics for the language. In order to make this semantics reversible, one could add a “history” to the configurations, as it has been done to define a reversible semantics for the concurrent calculi and languages mentioned above. This solution, however, is not very satisfactory, not only because of the cost in memory usage to store the history, but also because it is not strictly necessary when the considered language is reversible (the case of Janus). Thus, in this paper, we explore an alternative idea. Specifically, our proposal is based on replacing in the configurations the component with the code to be executed with a “program counter” that points to the next statement to be executed. At first glance, one might think that a step could be “undone” simply by moving the program counter back to the previous position. The actual definition of the reversible semantics, however, is far from trivial. In particular, given that Janus is a high-level language, in some cases it is not easy to determine how a program counter should be incremented. On the other hand, backward rules pose certain problems for determining the correct flow when there are several ways to go backwards from a given point in the execution, e.g., when undoing procedure calls. Our small-step semantics is made of a forward transition relation, which models normal execution (i.e., which is a conservative extension of the previous small-step semantics), and a backward transition relation, which can be used to “undo” the steps of a (forward) computation. 2 The Reversible Language Janus In this section, we introduce the syntax and semantics of Janus [20, 21, 23], a reversible (imperative) language in which statements can be inverted and executed in both forward and backward directions. p::=s(ids)+s::=x⊕=e∣x[e]⊕=e∣esse∣esse∣id∣id∣sse::=c∣x∣x[e]∣e⊙e⊕::=+∣−∣^c::=−2147483648∣…∣0∣…∣2147483647⊙::=⊕∣∗∣/∣%∣&∣&&∣∥∣′|′∣<∣>∣=∣!=∣<=∣>= array[]rcl@~~~~~~rcl@ p&::=&s~( procedure~id~s)^+&\\ s&::=&x =e\, \,x[e] =e\, if~e~ then~s~ else~s~ fi~e\\ & & from~e~ do~s~ loop~s~ until~e\, call~id\, \, uncall~id \, skip\, \,s~s\\ e&::=&c x x[e] e e ::=+ - ~\\ c&::=&-2147483648 … 0 … 2147483647\\ &::=& \, \,*\, \,/\, \,\%\, \,\&\, \,\&\&\, \,\|\, \, ~|~ \, \,<\, \,>\, \,=\, \,!=\, \,<=\, \,>=& array Figure 1: Language syntax The syntax of Janus is in Fig. 1. Janus is a simple imperative language with assignments, conditionals, loops, and procedure calls. A program consists of a statement (the main body) and a sequence of procedure declarations, introduced by the keyword procedure followed by the procedure name (an identifier). The reversible assignment instruction takes the form “x⊕=ex =e” (or “x[e1]⊕=e2x[e_1] =e_2” for array element assignments), which is equivalent to x=x⊕ex=x e (resp. x[e1]=x[e1]⊕e2x[e_1]=x[e_1] e_2), where ⊕ denotes an operator among plus, minus, and bitwise xor. Here, Janus requires that the left-hand side variable, x, does not occur in the expression e (resp. in the expressions e1e_1 and e2e_2). Reversible conditionals take the form “e1s1s2e2 if~e_1~ then~s_1~ else~s_2~ fi~e_2.” If the test e1e_1 evaluates to true, then s1s_1 is executed, and the assertion e2e_2 must also evaluate to truetrue. Similarly, if e1e_1 evaluates to false, then s2s_2 is executed, and the assertion e2e_2 must also be false. Reversible loops have the form “e1s1s2e2 from~e_1~ do~s_1~ loop~s_2~ until~e_2.” Initially, the assertion e1e_1 must evaluate to true. If so, s1s_1 is executed, followed by the evaluation of the test e2e_2. If e2e_2 is true, the loop terminates. Otherwise, s2s_2 is executed and control returns to e1e_1, which must evaluate to false in this case; execution then proceeds to execute s1s_1 and evaluate e2e_2 again, and so forth (until e2e_2 is true). Finally, we assume in this paper that procedures have neither parameters nor local variables. Consequently, a procedure call takes the form “ call~id” and simply executes the procedure body using the values of the program’s global variables. Similarly, “ uncall~id” invokes the inverse procedure. We now briefly describe the semantics of Janus. We primarily follow [23], except for loops, where we adopt the simplified version of [20, 21]. Con ⊢σ⇓c⟦c⟧ $ ~$ 26.35117pt $ σ c c $ Var ⊢σ⇓xσ(x) $ ~$ 26.98483pt $ σ x σ(x)$ Arr σ⊢⇓eσ⊢v ⊢σ⇓x[e]x[v] 28.14507pt $ σ e σ v$ 30.72559pt $ σ x[e] x[v]$ Bop ⊢σ⇓e1v1 ⊢σ⇓e2v2 =⟦⊙⟧(v1,v2)v ⊢σ⇓⊙e1e2v 101.56581pt $ σ e_1 v_1$ $ σ e_2 v_2$ $ (v_1,v_2)=v$ 29.88013pt $ σ e_1 e_2 v$ Figure 2: Semantics of expressions First, Figure 2 shows the rules for the evaluation of expressions. A judgement of the form σ⊢e⇓vσ e v denotes the evaluation of expression e under store σ, producing the value v. A store σ is a function from variable names and indexed variable names to values. We denote with σ[x↦v]σ[x v] the update of σ which assigns value v to variable x. For simplicity we assume that σ is defined for all the variables used in the program, and we omit the bindings of variables whose value is zero. We let ϵε denote an empty store, i.e., an store that maps every variable to zero. Here, ⟦_⟧ \_ denotes an interpretation function, e.g., ⟦+⟧(2,3)=2+3 + (2,3)=2+3, where “++” is the standard addition on integers. AssVar ⊢σ⇓ev ⊢σx⊕=e⇓σ[↦x⟦⊕⟧(σ(x),v)] $ σ e v$ 72.62889pt $ σ x~ =e σ[x (σ(x),v)]$ AssArr ⊢σ⇓elvl ⊢σ⇓ev ⊢σx[el]⊕=e⇓σ[↦x[vl]⟦⊕⟧(σ(x[vl]),v)] 50.59009pt $ σ e_l v_l$ $ σ e v$ 93.10057pt $ σ x[e_l]~ =e σ[x[v_l] (σ(x[v_l]),v)]$ Call ⊢σ⇓Γ(id)σ′ ⊢σ⇓callidσ′ 30.12234pt $ σ (id) σ $ 30.39844pt $ σ call~id σ $ UnCall ⊢σ⇓I⟦Γ(id)⟧σ′ ⊢σ⇓uncallidσ′ 38.03905pt $ σ (id) σ $ 35.56511pt $ σ uncall~id σ $ Seq ⊢σ⇓s1σ′ ⊢σ′⇓s2σ′ ⊢σ⇓s1s2σ′ 55.12952pt $ σ s_1 σ $ $ σ s_2 σ $ 29.38596pt $ σ s_1~s_2 σ $ IfTrue ⊢σ⇓e1v1 is_true?(v1) ⊢σ⇓s1σ′ ⊢σ′⇓e2v2 is_true?(v2) ⊢σ⇓ife1thens1elses2fie2σ′ 159.65271pt $ σ e_1 v_1$ $ is\_true?(v_1)$ $ σ s_1 σ $ $ σ e_2 v_2$ $ is\_true?(v_2)$ 68.17096pt $ σ if~e_1~ then~s_1~ else~s_2~ fi~e_2 σ $ IfFalse ⊢σ⇓e1v1 is_false?(v1) ⊢σ⇓s2σ′ ⊢σ′⇓e2v2 is_false?(v2) ⊢σ⇓ife1thens1elses2fie2σ′ 161.5416pt $ σ e_1 v_1$ $ is\_false?(v_1)$ $ σ s_2 σ $ $ σ e_2 v_2$ $ is\_false?(v_2)$ 68.17096pt $ σ if~e_1~ then~s_1~ else~s_2~ fi~e_2 σ $ LoopMain ⊢σ⇓e1v1 is_true?(v1) ⊢σ⇓s1σ′ ⊢σ′⇓(e1,s1,e2,s2)σ′ ⊢σ⇓frome1dos1loops2untile2σ′ 149.63179pt $ σ e_1 v_1$ $ is\_true?(v_1)$ $ σ s_1 σ $ $ σ (e_1,s_1,e_2,s_2) σ $ 80.19879pt $ σ from~e_1~ do~s_1~ loop~s_2~ until~e_2 σ $ LoopBase ⊢σ⇓e2v2 is_true?(v2) ⊢σ⇓(e1,s1,e2,s2)σ 58.82867pt $ σ e_2 v_2$ $ is\_true?(v_2)$ 46.25221pt $ σ (e_1,s_1,e_2,s_2) σ$ LoopRec ⊢σ⇓e2v2 is_false?(v2) ⊢σ⇓s2σ′ ⊢σ′⇓e1v1 is_false?(v1) ⊢σ′⇓s1σ′ ⊢σ′⇓(e1,s1,e2,s2)σ′ ⊢σ⇓(e1,s1,e2,s2)σ′ 186.04384pt $ σ e_2 v_2$ $ is\_false?(v_2)$ $ σ s_2 σ $ $ σ e_1 v_1$ $ is\_false?(v_1)$ $ σ s_1 σ $ $ σ (e_1,s_1,e_2,s_2) σ $ 49.96054pt $ σ (e_1,s_1,e_2,s_2) σ $ Skip ⊢σ⇓skipσ $ ~$ 22.74185pt $ σ skip σ$ Figure 3: Big-step semantics of sequential Janus Fig. 3 shows the (big-step) semantics for statements. A judgement σ⊢s⇓σ′σ s σ can be read as follows: the execution of statement s under store σ produces a new program state denoted by store σ′σ . Let us briefly describe the transition rules. Assignments are dealt with rules AssVar and AssArr. Here, (⊕=)( =) stands for (+=)(+=), (−=)(-=), and (^=)( ~=). Rule Call handles procedure calls, id call~id, by executing the body Γ(id) (id). We assume Γ maps procedure identifiers to their bodies. A procedure uncall (defined by rule UnCall) proceeds analogously but executes the inversion of Γ(id) (id), which is computed using the auxiliary function ℐI (defined in Fig. 4).111We note that, here, we consider rule Uncall as defined in [9], which is slightly different but equivalent to the original rule in citeJanusSem. The execution of sequences is dealt with in the obvious way by rule Seq. The execution of conditionals is defined by rules IfTrue and IfFalse, depending on whether the initial test (and, thus, the final asserion) is true or false. Auxiliary predicates _?(v) is\_true?(v) and _?(v) is\_false?(v) check the truth value of v. The execution of a loop is defined by three rules: a rule for entering the loop, LoopMain, a rule for exiting, LoopBase, and a rule for iteration, LoopRec. In order to enter the loop, rule LoopMain requires the initial assertion e1e_1 to be true. Then, s1s_1 is executed. Now, if the final test e2e_2 is true, the loop ends (rule LoopBase). Otherwise, rule LoopRec applies which executes s2s_2 and s1s_1, requiring both e2e_2 and e1e_1 to be false. Finally, rule Skip does not change the current store. For a deeper discussion, the interested reader is referred to [20, 21, 23]. ℐop⟦+⟧::=−ℐop⟦−⟧::=+ℐop⟦^⟧::=^ℐ⟦x⊕=e⟧::=xℐop⟦⊕⟧=eℐ⟦x[e1]⊕=e2⟧::=x[e1]ℐop⟦⊕⟧=e2ℐ⟦e1s1s2e2⟧::=e2ℐ⟦s1⟧ℐ⟦s2⟧e1ℐ⟦e1s1s2e2⟧::=e2ℐ⟦s1⟧ℐ⟦s2⟧e1ℐ⟦id⟧::=idℐ⟦id⟧::=idℐ⟦⟧::=ℐ⟦s1s2⟧::=ℐ⟦s2⟧ℐ⟦s1⟧ℐ⟦ids⟧::=id−1ℐ⟦s⟧ array[]rcl@~~~~~~rcl@ I_op + ::=- 42.67912ptI_op - &::=&+ 42.67912ptI_op ~ ::= ~\\ I x =e &::=&x~I_op =e\\ I x[e_1] =e_2 &::=&x[e_1]~I_op =e_2\\ I if~e_1~ then~s_1~ else~s_2~ fi~e_2 &::=& if~e_2~ then~I s_1 ~ else~I s_2 ~ fi~e_1\\ I from~e_1~ do~s_1~ loop~s_2~ until~e_2 &::=& from~e_2~ do~I s_1 ~ loop~I s_2 ~ until~e_1\\ I call~id &::=& uncall~id\\ I uncall~id &::=& call~id\\ I skip &::=& skip\\ I s_1~s_2 &::=&I s_2 ~I s_1 \\ I procedure~id~s &::=& procedure~id^-1~I s \\ array Figure 4: Inverter function for Janus statements 3 A Small-Step Semantics for Janus Now, we introduce a small-step semantics for Janus. Moving from a big-step semantics to a small-step one typically involves adding a stack to the configurations (see, e.g., [19, 14]). Alternatively, one can define a small-step semantics using contexts to specify where reductions can occur, as done in [9]. In this work, though, we prefer stacks, as they simplify the definition of a reversible version. Furthermore, they may help in clarifying the reason leading to an execution error, which could be useful in a potential extension of the semantics involving error handling. For the evaluation of expressions, we consider the same rules of the original big-step semantics [23], which are shown in Fig. 2.222Note that this means that the evaluation of expressions is not reversible (but considered a one-step evaluation). A configuration in our semantics has the form ⟨σ,s,π⟩ σ,s,π , where σ is a global store, s is a statement (the control of the configuration), and π is a stack, i.e., a list of expressions of the form (e2) seq(e_2), _(e2) if\_true(e_2), _(e2) if\_false(e_2), (e1,s1,e2,s2) loop1(e_1,s_1,e_2,s_2), and (e1,s1,e2,s2) loop2(e_1,s_1,e_2,s_2). Given a Janus program p=(sp1…pn)p=(s~p_1~…~p_n), an initial configuration has the form ⟨ϵ,s,[]⟩ ε,s,[\>] , where [][\>] is an empty list representing the initial, empty stack. AssVarS ⊢σ⇓ev →⟨=σ,x⊕e,π⟩⟨σ[↦x⟦⊕⟧(σ(x),v)],skip,π⟩ $ σ e v$ 95.63478pt $ σ,x~ =e,π → σ[x (σ(x),v)], skip,π $ AssArrS ⊢σ⇓elvl ⊢σ⇓ev →⟨=σ,x[el]⊕e,π⟩⟨σ[↦x[vl]⟦⊕⟧(σ(x[vl]),v)],skip,π⟩ 50.59009pt $ σ e_l v_l$ $ σ e v$ 116.10646pt $ σ,x[e_l]~ =e,π → σ[x[v_l] (σ(x[v_l]),v)], skip,π $ CallS →⟨σ,callid,π⟩⟨σ,Γ(id),π⟩ $ ~$ 56.31264pt $ σ, call~id,π → σ, (id),π $ UnCallS →⟨σ,uncallid,π⟩⟨σ,I⟦Γ(id)⟧,π⟩ $ ~$ 69.95155pt $ σ, uncall~id,π → σ,I (id) ,π $ Seq1 →⟨σ,s1s2,π⟩⟨:σ,s1,seq(s2)π⟩ $ ~$ 63.70435pt $ σ,s_1~s_2,π → σ,s_1, seq(s_2)\!:\!π $ Seq2 →⟨:σ,skip,seq(s2)π⟩⟨σ,s2,π⟩ $ ~$ 60.17134pt $ σ, skip, seq(s_2)\!:\!π → σ,s_2,π $ Figure 5: Small-step semantics: rules for basic constructs The small-step semantics is defined using a set of transition rules. We split them in two groups: basic statements (Fig. 5) and conditional and loop statements (Fig. 6). A transition step with the small-step semantics has the form ⟨σ,s,π⟩→⟨σ′,s′,π′⟩ σ,s,π → σ ,s ,π . Let us briefly explain the first set of rules (Fig. 5): • Rules AssVarS and AssArrS define the assignment. AssVarS evaluates the new value of the variable and updates the store, while AssArrS evaluates the index of the array and the new value and updates the value of the array in the store. • A procedure call (defined by rule CallS) reduces to the procedure body, denoted by Γ(id) (id). Similarly, a procedure uncall (defined by rule UnCallS) proceeds in much the same way, except that it reduces to the inversion ℐ⟦Γ(id)⟧I (id) of the body of procedure idid, retrieved using the mapping Γ . • Finally, the execution of a sequence is defined by rules Seq1 and Seq2. Here, we assume that the sequence operator is right-associative so that s1s2…sns_1~s_2~…~s_n is interpreted as s1(s2(…(sn−1sn)…))s_1~(s_2~(…(s_n-1~s_n)…)). Given a sequence s1s2s_1~s_2, rule Seq1 moves s2s_2 to the stack (adding an element of the form (s2) seq(s_2) on top of the stack) and starts the evaluation of s1s_1. Once s1s_1 is fully evaluated, rule Seq2 moves s2s_2 back to the control of the configuration. IfTrue1 ⊢σ⇓e1v1 is_true?(v1) →⟨σ,ife1thens1elses2fie2,π⟩⟨:σ,s1,if_true(e2)π⟩ 58.82867pt $ σ e_1 v_1$ $ is\_true?(v_1)$ 112.25151pt $ σ, if~e_1~ then~s_1~ else~s_2~ fi~e_2,π → σ,s_1, if\_true(e_2)\!:\!π $ IfTrue2 ⊢σ⇓e2v2 is_true?(v2) →⟨:σ,skip,if_true(e2)π⟩⟨σ,skip,π⟩ 58.82867pt $ σ e_2 v_2$ $ is\_true?(v_2)$ 70.94397pt $ σ, skip, if\_true(e_2)\!:\!π → σ, skip,π $ IfFalse1 ⊢σ⇓e1v1 is_false?(v1) →⟨σ,ife1thens1elses2fie2,π⟩⟨:σ,s2,if_false(e2)π⟩ 59.77312pt $ σ e_1 v_1$ $ is\_false?(v_1)$ 113.19595pt $ σ, if~e_1~ then~s_1~ else~s_2~ fi~e_2,π → σ,s_2, if\_false(e_2)\!:\!π $ IfFalse2 ⊢σ⇓e2v2 is_false?(v2) →⟨:σ,skip,if_false(e2)π⟩⟨σ,skip,π⟩ 59.77312pt $ σ e_2 v_2$ $ is\_false?(v_2)$ 71.88841pt $ σ, skip, if\_false(e_2)\!:\!π → σ, skip,π $ LoopMainS ⊢σ⇓e1v1 is_true?(v1) →⟨σ,frome1dos1loops2untile2,π⟩⟨:σ,s1,loop1(e1,s1,e2,s2)π⟩ 58.82867pt $ σ e_1 v_1$ $ is\_true?(v_1)$ 140.16302pt $ σ, from~e_1~ do~s_1~ loop~s_2~ until~e_2,π → σ,s_1, loop1(e_1,s_1,e_2,s_2)\!:\!π $ LoopBaseS ⊢σ⇓e2v2 is_true?(v2) →⟨:σ,skip,loop1(e1,s1,e2,s2)π⟩⟨σ,skip,π⟩ 58.82867pt $ σ e_2 v_2$ $ is\_true?(v_2)$ 87.98042pt $ σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ, skip,π $ Loop1 ⊢σ⇓e2v2 is_false?(v2) →⟨:σ,skip,loop1(e1,s1,e2,s2)π⟩⟨:σ,s2,loop2(e1,s1,e2,s2)π⟩ 59.77312pt $ σ e_2 v_2$ $ is\_false?(v_2)$ 125.8277pt $ σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ,s_2, loop2(e_1,s_1,e_2,s_2)\!:\!π $ Loop2 ⊢σ⇓e1v1 is_false?(v1) →⟨:σ,skip,loop2(e1,s1,e2,s2)π⟩⟨:σ,s1,loop1(e1,s1,e2,s2)π⟩ 59.77312pt $ σ e_1 v_1$ $ is\_false?(v_1)$ 125.8277pt $ σ, skip, loop2(e_1,s_1,e_2,s_2)\!:\!π → σ,s_1, loop1(e_1,s_1,e_2,s_2)\!:\!π $ Figure 6: Small-step semantics: rules for if and for loop The transition rules for conditionals and for loops are shown in Fig. 6. We distinguish the following cases: • For conditionals, first, either rule IfTrue1 or IfFalse1 is applied, depending on whether the condition e1e_1 evaluates to true or false, respectively. Rule IfTrue1 (resp. IfFalse1) pushes a new element of the form _(e2) if\_true(e_2) (resp. _(e2) if\_false(e_2)) onto the stack. • Once the corresponding statement is fully evaluated, rule IfTrue2 (resp. IfFalse2) applies if the assertion evaluates to the same value of the test. • Regarding loops, rule LoopMain enters the loop, requiring the assertion e1e_1 to be true and starting the execution of statement s1s_1. Furthermore, an element of the form (e1,s1,e2,s2) loop1(e_1,s_1,e_2,s_2) is added on top of the stack. • Each iteration of the loop is formalized using rules Loop1 and Loop2. The first rule, Loop1, applies when s1s_1 is fully evaluated and the condition e2e_2 evaluates to false. Here, s2s_2 is moved to the control of the configuration and (e1,s1,e2,s2) loop1(e_1,s_1,e_2,s_2) is replaced by (e1,s1,e2,s2) loop2(e_1,s_1,e_2,s_2) in the stack. Rule Loop2 is the counterpart of rule Loop1 but applies when s2s_2 is fully evaluated. In this case, e1e_1 must be evaluated to false. Then, s1s_1 is moved to the control of the configuration and (e1,s1,e2,s2) loop2(e_1,s_1,e_2,s_2) is changed back to (e1,s1,e2,s2) loop1(e_1,s_1,e_2,s_2) in the stack. • Finally, rule LoopBaseS applies when s1s_1 is fully evaluated and, moreover, the test e2e_2 is true, terminating loop execution. We denote with →∗→^* the reflexive and transitive closure of →. Now, we prove the equivalence between the big-step and the small-step semantics, when the program terminates without errors. For this purpose, we follow a proof scheme similar to that of [19]. In the following, we say that s is a proper statement if s≠(e1,s1,e2,s2)s≠(e_1,s_1,e_2,s_2). Our first lemma shows that the small-step semantics is complete, i.e., it can simulate all proof derivations with the natural semantics. Lemma 1 Let σ⊢s⇓σ′σ s σ be a proof with the big-step semantics of Figure 3. Then, we have (a) ⟨σ,s,π⟩→∗⟨σ′,,π⟩ σ,s,π → σ , skip,π if s is a proper statement, and (b) ⟨σ,,(e1,s1,e2,s2):π⟩→∗⟨σ′,,π⟩ σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ , skip,π if s=(e1,s1,e2,s2)s=(e_1,s_1,e_2,s_2), where π is an arbitrary stack. Proof We prove the claim by induction on the structure of the proof σ⊢s⇓σ′σ s σ . For simplicity, we implicitly assume that a sentence is proper unless otherwise stated. In particular, only rule LoopMain can introduce a non-proper statement, while only rules LoopBase and LoopRec can be applied to evaluate a non-proper statement. We distinguish the following cases depending on the applied rule: (AssVar) Then, we have σ⊢x⊕=e⇓σ[x↦⟦⊕⟧(σ(x),v)]σ x~ =e σ[x (σ(x),v)] by rule AssVar. Hence, ⟨σ,x⊕=e,π⟩→⟨σ[x↦⟦⊕⟧(σ(x),v)],,π⟩ σ,x~ =e,π → σ[x (σ(x),v)], skip,π by rule AssVarS. (AssArr) This case is perfectly analogous to the previous one by applying rule AssArrS instead. (Call) We have σ⊢id⇓σ′σ call~id σ , with σ⊢Γ(id)⇓σ′σ (id) σ . Then, the following derivation holds: ⟨σ,id,π⟩→⟨σ,Γ(id),π⟩(by rule CallS)→∗⟨σ′,,π⟩(by ind. hypothesis) array[]l& σ, call~id,π \\ →& σ, (id),π & (by rule CallS)\\ → & σ , skip,π & (by ind.\ hypothesis) array (UnCall) This case is perfectly analogous to the previous one by applying rule UnCallS instead. (Seq) We have σ⊢s1s2⇓σ′σ s_1~s_2 σ , with σ⊢s1⇓σ′σ s_1 σ and σ′⊢s2⇓σ′σ s_2 σ . Then, the following derivation holds: ⟨σ,s1s2,π⟩→⟨σ,s1,(s2):π⟩(by rule Seq1)→∗⟨σ′,,(s2):π⟩(by ind. hypothesis on the first premise)→⟨σ′,s2,π⟩(by rule Seq2)→∗⟨σ′,,π⟩(by ind. hypothesis on the second premise) array[]l& σ,s_1~s_2,π \\ →& σ,s_1, seq(s_2)\!:\!π & (by rule Seq1)\\ → & σ , skip, seq(s_2)\!:\!π & (by ind.\ hypothesis on the first premise)\\ →& σ ,s_2,π & (by rule Seq2)\\ → & σ , skip,π & (by ind.\ hypothesis on the second premise)\\ array (IfTrue) We have σ⊢e1s1s2e2⇓σ′σ if~e_1~ then~s_1~ else~s_2~ fi~e_2 σ with σ⊢e1⇓v1σ e_1 v_1, _?(v1) is\_true?(v_1), σ⊢s1⇓σ′σ s_1 σ , σ′⊢e2⇓v2σ e_2 v_2, and _?(v2) is\_true?(v_2). Then, the following derivation holds: ⟨σ,e1s1s2e2,π⟩→⟨σ,s1,_(e2):π⟩(by rule IfTrue1 since σ⊢e1⇓v1 and _?(v1))→∗⟨σ′,,_(e2):π⟩(by ind. hypothesis on σ⊢s1⇓σ′)→⟨σ′,s2,π⟩(by rule IfTrue2 since σ′⊢e2⇓v2 and _?(v2)) array[]l& σ, if~e_1~ then~s_1~ else~s_2~ fi~e_2,π \\ →& σ,s_1, if\_true(e_2)\!:\!π & (by rule IfTrue1 since $σ e_1 v_1$\\ && ~and $ is\_true?(v_1)$)\\ → & σ , skip, if\_true(e_2)\!:\!π & (by ind.\ hypothesis on $σ s_1 σ $)\\ →& σ ,s_2,π & (by rule IfTrue2 since $σ e_2 v_2$\\ && ~and $ is\_true?(v_2)$)\\ array (IfFalse) This case is perfectly analogous to the previous one by applying rules IfFalse1 and IfFalse2 from the small-step semantics. (LoopMain) We have σ⊢e1s1s2e2⇓σ′σ from~e_1~ do~s_1~ loop~s_2~ until~e_2 σ with σ⊢e1⇓v1σ e_1 v_1, _?(v1) is\_true?(v_1), σ⊢s1⇓σ′σ s_1 σ , and σ′⊢(e1,s1,e2,s2)⇓σ′σ (e_1,s_1,e_2,s_2) σ . Then, the following derivation holds: ⟨σ,e1s1s2e2,π⟩→⟨σ,s1,(e2,s1,s2,e2):π⟩(by rule LoopMainS since σ⊢e1⇓v1 and _?(v1))→∗⟨σ′,,(e2,s1,s2,e2):π⟩(by ind. hypothesis on σ⊢s1⇓σ′)→∗⟨σ′,,π⟩(by ind. hypothesis on σ′⊢(e1,s1,e2,s2)⇓σ′) array[]l& σ, from~e_1~ do~s_1~ loop~s_2~ until~e_2,π \\ →& σ,s_1, loop1(e_2,s_1,s_2,e_2)\!:\!π & (by rule LoopMainS since \\ && ~$σ e_1 v_1$ and $ is\_true?(v_1)$)\\ → & σ , skip, loop1(e_2,s_1,s_2,e_2)\!:\!π & (by ind.\ hypothesis on $σ s_1 σ $)\\ → & σ , skip,π & (by ind.\ hypothesis \\ && ~on $σ (e_1,s_1,e_2,s_2) σ $)\\ array (LoopBase) We have σ⊢(e1,s1,e2,s2)⇓σ (e_1,s_1,e_2,s_2) σ, with σ⊢e2⇓v2σ e_2 v_2 and _?(v2) is\_true?(v_2). Then, the derivation ⟨σ,,(e1,s1,e2,s2):π⟩→⟨σ,,π⟩ σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ, skip,π holds by applying rule LoopBaseS. (LoopRec) We have σ⊢(e1,s1,e2,s2)⇓σ′σ (e_1,s_1,e_2,s_2) σ , with σ⊢e2⇓v2σ e_2 v_2, _?(v2) is\_false?(v_2), σ⊢s2⇓σ′σ s_2 σ , σ′⊢e1⇓v1σ e_1 v_1, _?(v1) is\_false?(v_1), σ′⊢s1⇓σ′σ s_1 σ , and σ′⊢(e1,s1,e2,s2)⇓σ′σ (e_1,s_1,e_2,s_2) σ . Then, the following derivation holds: ⟨σ,,(e1,s1,e2,s2):π⟩→⟨σ,s2,(e1,s1,e2,s2):π⟩(by rule Loop1 since σ⊢e2⇓v2 and _?(v2))→∗⟨σ′,,(e1,s1,e2,s2):π⟩(by ind. hypothesis on σ⊢s2⇓σ′)→⟨σ′,s1,(e1,s1,e2,s2):π⟩(by rule Loop2 since σ⊢e1⇓v1 and _?(v1))→∗⟨σ′,,(e1,s1,e2,s2):π⟩(by ind. hypothesis on σ′⊢s1⇓σ′)→∗⟨σ′,,π⟩(by ind. hypothesis on σ′⊢(e1,s1,e2,s2)⇓σ′) array[]l& σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π \\ →& σ,s_2, loop2(e_1,s_1,e_2,s_2)\!:\!π & (by rule Loop1 since $σ e_2 v_2$ \\ && ~and $ is\_false?(v_2)$)\\ → & σ , skip, loop2(e_1,s_1,e_2,s_2)\!:\!π & (by ind.\ hypothesis on $σ s_2 σ $)\\ →& σ ,s_1, loop1(e_1,s_1,e_2,s_2)\!:\!π & (by rule Loop2 since $σ e_1 v_1$ \\ && ~and $ is\_false?(v_1)$)\\ → & σ , skip, loop1(e_1,s_1,e_2,s_2)\!:\!π & (by ind.\ hypothesis on $σ s_1 σ $)\\ → & σ , skip,π & (by ind. hypothesis \\ && ~on $σ (e_1,s_1,e_2,s_2) σ $) array (Skip) We have s=s= skip and σ⊢⇓σ skip σ. Thus, ⟨σ,,π⟩→∗⟨σ,,π⟩ σ, skip,π → σ, skip,π since →∗→ is reflexive. ∎ Let us now consider the soundness of the small-step semantics. For this purpose, we first introduce the notion of a balanced derivation: Definition 1(balanced derivation) A derivation ⟨σ,s,π⟩→∗⟨σ′,s′,π′⟩ σ,s,π → σ ,s ,π is balanced if π=π′π=π and every intermediate stack is equal or extends the initial one. In particular, any successful derivation of the form ⟨ϵ,s,[]⟩→∗⟨σ,,[]⟩ ε,s,[\>] → σ, skip,[\>] is trivially balanced. We also consider another type of derivations: Definition 2(loop derivation) A derivation ⟨σ,,(e1,s1,e2,s2):π⟩ σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π →∗⟨σ′,,π⟩→ σ , skip,π is called a loop derivation if every intermediate stack is equal or extends either (e1,s1,e2,s2):π loop1(e_1,s_1,e_2,s_2)\!:\!π or (e1,s1,e2,s2):π loop2(e_1,s_1,e_2,s_2)\!:\!π. Intuitively speaking, a loop derivation corresponds to sequences of steps with rules Loop1 and Loop2, ending with a final application of rule LoopBaseS. Definition 3(trace) The sequence of transition rules applied in a derivation is called its trace. A balanced (resp. loop) trace is the trace of a balanced (resp. loop) derivation. We have several possibilities for characterizing a trace as balanced. An empty trace, denoted by ϵε, is clearly balanced. For non-empty traces, we have several possibilities. In particular, a balanced trace cannot begin with the application of rules Seq2, IfTrue2, IfFalse2, or LoopBaseS, as these would produce an intermediate stack that does not extend the initial one. In summary, all balanced and loop traces can be derived from the following grammar: ::=ϵ∣AssVarS∣AssArrS∣CallS∣UnCallS∣Seq1Seq2∣IfTrue1IfTrue2∣IfFalse1IfFalse2∣LoopMainS::=LoopBaseS∣Loop1Loop2 array[]lbal&::=&ε AssVarS AssArrS CallS~bal UnCallS~bal\\ && Seq1~bal~ Seq2~bal\\ && IfTrue1~bal~ IfTrue2 IfFalse1~bal~ IfFalse2\\ && LoopMainS~bal~loop\\[4.30554pt] loop&::=& LoopBaseS Loop1~bal~ Loop2~bal~loop array The following lemma states the soundness of the small-step semantics. Lemma 2 Consider a derivation of the form ⟨σ,s,π1⟩→∗⟨σ′,,π2⟩ σ,s, _1 → σ , skip, _2 . • If the derivation is balanced, then s is a proper expression, π1=π2 _1= _2 and σ⊢s⇓σ′σ s σ . • If the derivation is a loop, then s=s= skip, π1=(e1,s1,e2,s2):π _1= loop1(e_1,s_1,e_2,s_2)\!:\!π, π2=π _2=π, and σ⊢(e1,s1,e2,s2)⇓σ′σ (e_1,s_1,e_2,s_2) σ . Proof We prove the claim by induction on length of the derivation, following the structure of balanced and loop traces, according to the grammar above: (ϵε) Then, s must be skip and the proof follows by applying rule Skip with σ=σ′σ=σ . (AssVarS) Then, we have ⟨σ,x⊕=e,π⟩→⟨σ[x↦⟦⊕⟧(σ(x),v)],,π⟩ σ,x~ =e,π → σ[x (σ(x),v)], skip,π , with σ⊢e⇓vσ e v. Hence, the proof σ⊢x⊕=e⇓σ[x↦⟦⊕⟧(σ(x),v)]σ x~ =e σ[x (σ(x),v)] follows by applying rule AssVar. (AssArrS) This case is perfectly analogous to the previous one by applying rule AssArr instead. (CallS bal) Then, ⟨σ,id,π⟩→⟨σ,Γ(id),π⟩→∗⟨σ′,,π⟩ σ, call~id,π → σ, (id),π → σ , skip,π . Now, since ⟨σ,Γ(id),π⟩→∗⟨σ′,,π⟩ σ, (id),π → σ , skip,π is balanced, by the ind. hypothesis, we have σ⊢Γ(id)⇓σ (id) σ. The claim thus follows by applying rule Call on σ⊢σ call~id. (UnCallS) This case is perfectly analogous to the previous one by applying rule UnCall instead. (Seq1 bal Seq2 bal) Then, we have a derivation of the following form: ⟨σ,s1s2,π⟩→⟨σ,s1,(s2):π⟩→∗⟨σ′,,(s2):π⟩⏞(1)→⟨σ′,s2,π⟩→∗⟨σ′,,π⟩⏟(2) array[]l σ,s_1~s_2,π &→& σ,s_1, seq(s_2)\!:\!π → σ , skip, seq(s_2)\!:\!π ^(1)\\ &→& σ ,s_2,π → σ , skip,π _(2)\\ array Since both (1) and (2) above are balanced, by the inductive hypothesis, we have σ⊢s1⇓σ′σ s_1 σ and σ′⊢s2⇓σ′σ s_2 σ . Therefore, the proof follows by applying rule Seq on σ⊢s1s2σ s_1~s_2. (IfTrue1 bal IfTrue2) Then, we have a derivation of the following form: ⟨σ,e1s1s2e2,π⟩→⟨σ,s1,_(e2):π⟩→∗⟨σ′,,_(e2):π⟩⏟(1)→⟨σ′,,π⟩ array[]l σ, if~e_1~ then~s_1~ else~s_2~ fi~e_2,π \\ → σ,s_1, if\_true(e_2)\!:\!π → σ , skip, if\_true(e_2)\!:\!π _(1)→ σ , skip,π array with σ⊢e1⇓v1σ e_1 v_1, _?(v1) is\_true?(v_1), σ′⊢e2⇓v2σ e_2 v_2, and _?(v2) is\_true?(v_2). Since (1) above is balanced, by the inductive hypothesis, we have σ⊢s1⇓σ′σ s_1 σ . Therefore, the proof follows by applying rule IfTrue on σ⊢e1s1s2e2σ if~e_1~ then~s_1~ else~s_2~ fi~e_2. (IfFalse1 bal IfFalse2) This case is perfectly analogous to the previous one by applying rule IfFalse instead. (LoopMainS bal loop) Then, we have a balanced derivation as follows: ⟨σ,e1s1s2e2,π⟩→⟨σ,s1,(e1,s1,e2,s2):π⟩→∗⟨σ′,,(e1,s1,e2,s2):π⟩⏟(1)→∗⟨σ′,,π⟩ array[]l σ, from~e_1~ do~s_1~ loop~s_2~ until~e_2,π \\ → σ,s_1, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ , skip, loop1(e_1,s_1,e_2,s_2)\!:\!π _(1)\\ → σ , skip,π array with σ⊢e1⇓v1σ e_1 v_1 and _?(v1) is\_true?(v_1). Since (1) above is balanced, by the ind. hypothesis, we have σ⊢s1⇓σ′σ s_1 σ . Moreover, since ⟨σ′,,(e1,s1,e2,s2):π⟩→∗⟨σ′,,π⟩ σ , skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ , skip,π is a loop derivation, by the inductive hypothesis, we have σ′⊢(e1,s1,e2,s2)⇓σ′σ (e_1,s_1,e_2,s_2) σ . Finally, the proof follows by applying rule LoopMain on σ⊢e1s1s2e2σ from~e_1~ do~s_1~ loop~s_2~ until~e_2. (LoopBaseS) Then, we have a one-step loop derivation of the following form: ⟨σ,,(e1,s1,e2,s2):π⟩→⟨σ,,π⟩ σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ, skip,π with σ⊢e2⇓v2σ e_2 v_2 and _?(v2) is\_true?(v_2). Trivially, we have σ⊢(e1,s1,e2,s2)⇓σ (e_1,s_1,e_2,s_2) σ by rule LoopBase. (Loop1 bal Loop2 bal loop) Then, we have a loop derivation as follows: ⟨σ,,(e1,s1,e2,s2):π⟩→⟨σ,s2,(e1,s1,e2,s2):π⟩→∗⟨σ′,,(e1,s1,e2,s2):π⟩⏟(1)→⟨σ′,s1,(e1,s1,e2,s2):π⟩→∗⟨σ′,,(e1,s1,e2,s2):π⟩⏟(2)→∗⟨σ′,,π⟩ array[]l σ, skip, loop1(e_1,s_1,e_2,s_2)\!:\!π \\ → σ,s_2, loop2(e_1,s_1,e_2,s_2)\!:\!π → σ , skip, loop2(e_1,s_1,e_2,s_2)\!:\!π _(1)\\ → σ ,s_1, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ , skip, loop1(e_1,s_1,e_2,s_2)\!:\!π _(2)\\ → σ , skip,π array with σ⊢e2⇓v2σ e_2 v_2, _?(v2) is\_false?(v_2), σ′⊢e1⇓v1σ e_1 v_1, and _?(v1) is\_false?(v_1). Since both (1) and (2) above are balanced, by the inductive hypothesis, we have σ⊢s2⇓σ′σ s_2 σ and σ′⊢s1⇓σ′σ s_1 σ . Moreover, since ⟨σ′,,(e1,s1,e2,s2):π⟩→∗⟨σ′,,π⟩ σ , skip, loop1(e_1,s_1,e_2,s_2)\!:\!π → σ , skip,π is a loop derivation, we have σ′⊢(e1,s1,e2,s2)⇓σ′σ (e_1,s_1,e_2,s_2) σ . Finally, the proof follows by applying rule LoopRec on σ⊢(e1,s1,e2,s2)σ (e_1,s_1,e_2,s_2). ∎ Now, we can proceed with the main result of correctness for the small-step semantics: Theorem 3.1 ϵ⊢s⇓σ iff ⟨ϵ,s,[]⟩→∗⟨σ,,[]⟩ε s σ iff ε,s,[\>] → σ, skip,[\>] Proof The “only if” part follows from Lemma 1. The “if” part follows from Lemma 2 and the fact that any derivation of the form ⟨ϵ,s,[]⟩→∗⟨σ,,[]⟩ ε,s,[\>] → σ, skip,[\>] is balanced. ∎ 4 A Reversible Semantics for Janus In this section, we propose a new reversible (small-step) semantics based on the use of a program counter. Here, the configurations do not include a piece of code to be executed, as in the small-step semantics of the previous section, but a label that points to the next “block” of the program to be executed. This greatly simplifies the definition of a reversible semantics for the language. Typically, semantics based on a program counter have been restricted to simple, assembly-like languages, where execution is modeled by simply incrementing a counter or updating it to perform jumps. In contrast, high-level language definitions rarely use an explicit program counter, favoring instead the use of evaluation contexts to manage control flow implicitly. We refer to related work (Section 5) for a more detailed discussion on this topic. p::=s(ids)+s::=[x⊕=e]ℓ∣[x[e]⊕=e]ℓ∣[e]ℓss[e]ℓ∣[e]ℓss[e]ℓ∣[id]ℓ∣[id]ℓ∣[]ℓ∣ss∣[]ℓ∣[]ℓ array[]rcl@~~~~~~rcl@ p&::=&s~( procedure~id~s)^+&\\ s&::=& [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[x =e [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \, \, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[x[e] =e [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \, if~ [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[e [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] ~ then~s~ else~s~ fi~ [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[e [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \\ & & from~ [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[e [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] ~ do~s~ loop~s~ until~ [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[e [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[ call~id [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \, \, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[ uncall~id [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[ skip [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0] \, \,s~s\\ & & [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[ start] \, \, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,0[ stop] array Figure 7: Extended language syntax (e,c,⊕e,c, and ⊙ are as in Fig. 1) In the following, we introduce a control-flow graph (CFG) to manage the evolution of the program counter. To this end, Fig. 7 introduces an extended syntax where elementary blocks (conditions, assignments, call, uncall, and skip) are now labeled. We consider a domain of labels ℒ L, where ℓ,ℓ1,… , _1,… range over the set ℒ L. All labels are unique in a program. We let (ℓ)=oblock( )=o if [o]ℓ[o] belongs to the considered program, where o is either a statement or a condition. [start]1 [n += 3]2 [call sumMul3]3 [stop]4 procedure sumMul3 [start]5 [i += 1]6 from [i == 1]7 do if [(i % 3) == 0]8 then [total += i]9 else [skip]10 fi [(i % 3) == 0]11 loop [i += 1]12 until [i >= n]13 [n += total]14 [stop]15 Figure 8: Sum3: a program computing the sum of the multiples of 3 up to n Furthermore, we assume all programs (and procedures) have an initial statement start and a final statement stop that simply mark the beginning and end (and is semantically equivalent to skip). A labeled Janus program, Sum3, is shown in Figure 8. ([e1]ℓ1s1s2[e2]ℓ2)=ℓ1(s1s2)=(s1)([e1]ℓ1s1s2[e2]ℓ2)=ℓ1([s]ℓ)=ℓ otherwise([e1]ℓ1s1s2[e2]ℓ2)=ℓ2(s1s2)=(s2)([e1]ℓ1s1s2[e2]ℓ2)=ℓ2([s]ℓ)=ℓ otherwise array[]rcl@~~~~~~rclentry( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)&=& _1&entry(s_1~s_2)&=&entry(s_1)\\ entry( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2)&=& _1&entry([s] )&=& ~ otherwise\\[4.30554pt] exit( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)&=& _2&exit(s_1~s_2)&=&exit(s_2)\\ exit( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2)&=& _2&exit([s] )&=& ~ otherwise array Figure 9: Entry and exit points Now, Figure 9 introduces the auxiliary function entry (resp. exit), which returns the entry (resp. exit) label of a program statement. Note that, in contrast to most (high level) programming languages, exit always returns a single label because of Janus conditionals with a single exit point. The definitions are self-explanatory. We also consider the following (partially defined) function, ctx, that identifies the statement where the label of a given expression (a test or assertion) occurs. E.g., if the sentence “[e1]ℓ1s1s2[e2]ℓ2 if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2” occurs in a program, then (ℓ1)=(ℓ2)=([e1]ℓ1s1s2[e2]ℓ2) ctx( _1)= ctx( _2)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2). Analogously, if the sentence “[e1]ℓ1s1s2[e2]ℓ2 from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2” occurs in the program, then (ℓ1)=(ℓ2)=([e1]ℓ1s1s2[e2]ℓ2) ctx( _1)= ctx( _2)=( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2). ([e1]ℓ1s1s2[e2]ℓ2)=(ℓ1,(s1)),((s1),ℓ2)∪(ℓ1,(s2),((s2),ℓ2)∪(s1)∪(s2)([e1]ℓ1s1s2[e2]ℓ2)=(ℓ1,(s1)),((s1),ℓ2)∪(ℓ2,(s2)),((s2),ℓ1)∪(s1)∪(s2)(s1s2)=((s1),(s2)∪(s1)∪(s2)(s)=∅otherwise array[]rclflow( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)&=&\( _1,entry(s_1)),(exit(s_1), _2)\\\ &&∪~\( _1,entry(s_2),(exit(s_2), _2)\\\ &&∪~flow(s_1) (s_2)\\ flow( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2)&=&\( _1,entry(s_1)),(exit(s_1), _2)\\\ &&∪~\( _2,entry(s_2)),(exit(s_2), _1)\\\ &&∪~flow(s_1) (s_2)\\ flow(s_1~s_2)&=&\(exit(s_1),entry(s_2)\ (s_1) (s_2)\\ flow(s)&=& otherwise array Figure 10: Control-flow graph of a Janus program Then, function flow (Fig. 10) computes the edges of the CFG of a Janus program. It is worth noting that we do not have edges for call/return (resp. uncall/return) in a CFG. The control flow for these cases will be dealt with dynamically in the corresponding transition rules. We represent an edge (ℓ1,ℓ2)( _1, _2) graphically as ℓ1⟶ℓ2 _1 _2. Now, we proceed as follows: • given a program, for each procedure “s procedure~id~s”, we introduce an inverse procedure of the form “−1ℐ⟦s⟧ procedure~id^-1~I s ”, where the definition of function ℐ⟦⟧I ~ from Fig. 4 is extended so that ℐ⟦⟧::=I start ::= stop and ℐ⟦⟧::=I stop ::= start; • then, we add labels to each elementary block; • finally, we compute the CFGs of the main program and of each procedure as well as its inverse version. For example, for program Sum3 (Fig. 8), function flow computes the following two CFGs (the graphical representation is shown in Fig. 11):333For simplicity, we do not show the CFG of sumMul3−1sumMul3^-1 since there is no uncall in the program and, thus, it will not be used. CFG=(1,2),(2,3),(3,4)CFGsumMul3=(5,6),(6,7),(7,8),(8,9),(8,10),(9,11),(10,11),(11,13),(13,12),(12,7),(13,14),(14,15) array[]rlCFG_main=\&(1,2),(2,3),(3,4)~\\\[4.30554pt] CFG_sumMul3=\&(5,6),(6,7),(7,8),(8,9),(8,10),(9,11),(10,11),\\ &(11,13),(13,12),(12,7),(13,14),(14,15)~\ array 1234Main program5678Procedure sumMul3sumMul39101113121415 Figure 11: CFGs for program Sum3 4.1 The Forward Rules → AssVar =block(ℓ′)(=x⊕e) ⊢σ⇓ev ⟶ℓ′ℓ′ ⇀⟨σ,ℓ,ℓ′,π⟩⟨σ[↦x⟦⊕⟧(σ(x),v)],ℓ′,ℓ′,π⟩ 98.25536pt $ ( )=(x~ =e)$ $ σ e v$ $ $ 91.83961pt $ σ, , ,π σ[x (σ(x),v)], , ,π $ → AssArr =block(ℓ′)(=x[el]⊕e) ⊢σ⇓elvl ⊢σ⇓ev ⟶ℓ′ℓ′ ⇀⟨σ,ℓ,ℓ′,π⟩⟨σ[↦x[vl]⟦⊕⟧(σ(x[vl]),v)],ℓ′,ℓ′,π⟩ 136.03136pt $ ( )=(x[e_l]~ =e)$ $ σ e_l v_l$ $ σ e v$ $ $ 105.67065pt $ σ, , ,π σ[x[v_l] (σ(x[v_l]),v)], , ,π $ → Call =block(ℓ′)(callid) ⟶entry(Γ(id))ℓ′ ⇀⟨σ,ℓ,ℓ′,π⟩⟨:σ,entry(Γ(id)),ℓ′,call(ℓ′)π⟩ 89.11476pt $ ( )=( call~id)$ $ ( (id)) $ 90.32544pt $ σ, , ,π σ,entry( (id)), , call( )\!:\!π $ Return1→ Return1 =block(ℓ′)stop ⟶ℓ′ℓ′ ⇀⟨:σ,ℓ,ℓ′,call(ℓ′)π⟩⟨σ,ℓ′,ℓ′,π⟩ 57.5055pt $ ( )= stop$ $ $ 71.56715pt $ σ, , , call( )\!:\!π σ, , ,π $ → UnCall =block(ℓ′)(uncallid) ⟶entry(Γ(id-1))ℓ′ ⇀⟨σ,ℓ,ℓ′,π⟩⟨:σ,entry(Γ(id-1)),ℓ′,uncall(ℓ′)π⟩ 97.87173pt $ ( )=( uncall~id)$ $ ( (id^-1)) $ 99.0824pt $ σ, , ,π σ,entry( (id^-1)), , uncall( )\!:\!π $ Return2→ Return2 =block(ℓ′)stop ⟶ℓ′ℓ′ ⇀⟨:σ,ℓ,ℓ′,uncall(ℓ′)π⟩⟨σ,ℓ′,ℓ′,π⟩ 57.5055pt $ ( )= stop$ $ $ 76.73383pt $ σ, , , uncall( )\!:\!π σ, , ,π $ → Skip =block(ℓ′)skip ⟶ℓ′ℓ′ ⇀⟨σ,ℓ,ℓ′,π⟩⟨σ,ℓ′,ℓ′,π⟩ 54.53328pt $ ( )= skip$ $ $ 53.4421pt $ σ, , ,π σ, , ,π $ Figure 12: Reversible forward semantics: rules for basic constructs Now, we introduce the transition relation, ⇀ , defining the forward direction of the reversible semantics. Here, configurations have the form ⟨σ,ℓ,ℓ′,π⟩ σ, , ,π , where the control of the configuration is determined by a pair of labels representing the last executed statement and the next statement to be executed, respectively. Actually, the transition rules of the forward semantics only use the latter. We include the former in the configurations since it will be used by the transition rules of the backward semantics, and in this way we have a single definition of configuration that works for both directions. The rules defining the basic constructs can be found in Fig. 12. These rules are quite similar to their counterpart in the small-step semantics of Fig. 5. The main differences are the following: • First, configurations no longer contain the next statement to be executed, but rather a label that identifies it (acting as a program counter). Thus, we use the auxiliary function block to identify the block pointed to by that label. Furthermore, in many cases, the rules increment the program counter according to the edges of the CFG. • Rule → Call updates the control of the configuration with the labels from the first two statements of the procedure. Specifically, the first label will point to the statement start (which is not executed), so the second label will point to the actual first statement of the procedure. Rule Return1→ Return1, on the other hand, is triggered when the next statement to be executed is stop. In this case, we update the control of the configuration so that the last executed statement is call, and the next statement to be executed is the one following it (according to the CFG). • Rules → UnCall and Return2→ Return2 proceed analogously, with the only difference being that, in this case, we consider the inverse procedure. • Finally, we introduce a new rule, → Skip, to deal with skip which just increments the program counter (according to the CFG). IfTrue1→ IfTrue1 =block(ℓ1)e1 =ctx(ℓ1)(if[e1]ℓ1thens1elses2fi[e2]ℓ2) ⊢σ⇓e1v1 is_true?(v1) ⇀⟨σ,ℓ,ℓ1,π⟩⟨:σ,ℓ1,entry(s1),if_true(ℓ1,ℓ2)π⟩ 199.33458pt $ ( _1)=e_1$ $ ctx( _1)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)$ $ σ e_1 v_1$ $ is\_true?(v_1)$ 99.26784pt $ σ, , _1,π σ, _1,entry(s_1), if\_true( _1, _2)\!:\!π $ IfTrue2→ IfTrue2 =block(ℓ2)e2 ⊢σ⇓e2v2 is_true?(v2) ⟶ℓ2ℓ′2 ⇀⟨:σ,ℓ,ℓ2,if_true(ℓ1,ℓ2)π⟩⟨σ,ℓ2,ℓ′2,π⟩ 121.7109pt $ ( _2)=e_2$ $ σ e_2 v_2$ $ is\_true?(v_2)$ $ _2 _2$ 83.80331pt $ σ, , _2, if\_true( _1, _2)\!:\!π σ, _2, _2,π $ IfFalse1→ IfFalse1 =block(ℓ1)e1 =ctx(ℓ1)(if[e1]ℓ1thens1elses2fi[e2]ℓ2) ⊢σ⇓e1v1 is_false?(v1) ⇀⟨σ,ℓ,ℓ1,π⟩⟨:σ,ℓ1,entry(s2),if_false(ℓ1,ℓ2)π⟩ 200.27902pt $ ( _1)=e_1$ $ ctx( _1)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)$ $ σ e_1 v_1$ $ is\_false?(v_1)$ 100.21228pt $ σ, , _1,π σ, _1,entry(s_2), if\_false( _1, _2)\!:\!π $ IfFalse2→ IfFalse2 =block(ℓ2)e2 ⊢σ⇓e2v2 is_false?(v2) ⟶ℓ2ℓ′2 ⇀⟨:σ,ℓ,ℓ2,if_false(ℓ1,ℓ2)π⟩⟨σ,ℓ2,ℓ′2,π⟩ 122.65535pt $ ( _2)=e_2$ $ σ e_2 v_2$ $ is\_false?(v_2)$ $ _2 _2$ 84.74776pt $ σ, , _2, if\_false( _1, _2)\!:\!π σ, _2, _2,π $ → LoopMain =block(ℓ1)e1 =ctx(ℓ1)(from[e1]ℓ1dos1loops2until[e2]ℓ2) ⊢σ⇓e1v1 is_true?(v1) ⇀⟨σ,ℓ,ℓ1,π⟩⟨:σ,ℓ1,entry(s1),loop1(ℓ1,s1,ℓ2,s2)π⟩ 170.2788pt $ ( _1)=e_1$ $ ctx( _1)=( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2)$ $ σ e_1 v_1$ $ is\_true?(v_1)$ 109.51088pt $ σ, , _1,π σ, _1,entry(s_1), loop1( _1,s_1, _2,s_2)\!:\!π $ → LoopBase =block(ℓ2)e2 ⊢σ⇓e2v2 is_true?(v2) ⟶ℓ2ℓ′2 ≠ℓ′2entry(s1) ⇀⟨:σ,ℓ,ℓ2,loop1(ℓ1,s1,ℓ2,s2)π⟩⟨σ,ℓ2,ℓ′2,π⟩ 158.731pt $ ( _2)=e_2$ $ σ e_2 v_2$ $ is\_true?(v_2)$ $ _2 _2$ $ _2 (s_1)$ 94.04636pt $ σ, , _2, loop1( _1,s_1, _2,s_2)\!:\!π σ, _2, _2,π $ Loop1→ Loop1 =block(ℓ2)e2 ⊢σ⇓e2v2 is_false?(v2) ⇀⟨:σ,ℓ,ℓ2,loop1(ℓ1,s1,ℓ2,s2)π⟩⟨:σ,ℓ2,entry(s2),loop2(ℓ1,s1,ℓ2,s2)π⟩ 99.70395pt $ ( _2)=e_2$ $ σ e_2 v_2$ $ is\_false?(v_2)$ 149.58736pt $ σ, , _2, loop1( _1,s_1, _2,s_2)\!:\!π σ, _2,entry(s_2), loop2( _1,s_1, _2,s_2)\!:\!π $ Loop2→ Loop2 =block(ℓ1)e1 ⊢σ⇓e1v1 is_false?(v1) ⇀⟨:σ,ℓ,ℓ1,loop2(ℓ1,s1,ℓ2,s2)π⟩⟨:σ,ℓ1,entry(s1),loop1(ℓ1,s1,ℓ2,s2)π⟩ 99.70395pt $ ( _1)=e_1$ $ σ e_1 v_1$ $ is\_false?(v_1)$ 149.58736pt $ σ, , _1, loop2( _1,s_1, _2,s_2)\!:\!π σ, _1,entry(s_1), loop1( _1,s_1, _2,s_2)\!:\!π $ Figure 13: Reversible forward semantics: rules for if and for loop The second group of rules, the rules for conditional and loop statements, can be seen in Figure 13. These rules are perfectly analogous to their counterpart in the small-step semantics of Fig. 6. The only relevant difference lies in the use of a program counter to identify the next block to be executed. Note also that the use of the auxiliary function ctx is necessary to determine whether the Boolean expression is part of a conditional statement or of a loop. On the other hand, observe that the stack elements _ if\_true and _ if\_false contain labels for both the test and the assertion of the conditional. In practice, only the second label is required (by either rule IfTrue2→ IfTrue2 and IfFalse2→ IfFalse2). However, the rules of the backward semantics will require the first label (that of the test). Hence, we include both labels in the elements of the stack so that they can be used by both the forward and the backward semantics. Also, when the program counter points to the test of the loop (ℓ2 _2), we can either terminate the loop and proceed to the next statement or execute s2s_2 and return to the initial assertion (ℓ1 _1). Consequently, ℓ2 _2 has two outgoing edges in the CFG. Therefore, we add the condition ℓ2′≠(s1) _2 (s_1) in rule → LoopBase in order to ensure that we are considering the right edge. Finally, the elements of the stack, loop1 and loop2, could in principle contain only four labels, (ℓ1,(s1),ℓ2,(s2))( _1,entry(s_1), _2,entry(s_2)). Indeed, this would be enough for the forward semantics. However, in the backward semantics, we will need to access (s1)exit(s_1) and (s2)exit(s_2). Therefore, we use (ℓ1,s1,ℓ2,s2)( _1,s_1, _2,s_2) as arguments of loop1 and loop2, so that they contain enough information for both semantics. Given a program p=(sp1…pn)p=(s~p_1~…~p_n), an initial configuration has now the form ⟨ϵ,(s),ℓ,[]⟩ ε,entry(s), ,[\>] , where (s)⟶ℓentry(s) belongs to the CFG of the program. Now, we will state the equivalence between the small-step semantics of the previous section and the reversible (forward) semantics just introduced. In what follows, we assume that program blocks are also labeled when applying the rules of small-step semantics of the previous section, which simply ignore the annotations. Furthermore, for simplicity, although we consider a single program in our correctness result, we assume that the additional statements start and stop only occur when considering the reversible semantics. Lemma 3 Let s be a statement where (s)⟶ℓentry(s) belongs to the CFG. Then, ⟨ϵ,s,[]⟩→∗⟨σ,,[]⟩ ε,s,[\>] → σ, skip,[\>] iff ⟨ϵ,(s),ℓ,[]⟩⇀∗⟨σ,ℓ′,ℓ′,[]⟩ ε,entry(s), ,[\>] σ, , ,[\>] with (ℓ′)=block( )= stop. ∼stack[][] 22.31946pt $ [\>] _stack[\>]$ ∼stackπ′ :seq(s)∼stackπ′ 21.64478pt $ π _stackπ $ 35.71077pt $ seq(s)\!:\!π _stackπ $ ∼stackπ′ :∼stackπcall(ℓ)π′ 21.64478pt $ π _stackπ $ 35.74203pt $ π _stack call( )\!:\!π $ ∼stackπ′ :∼stackπuncall(ℓ)π′ 21.64478pt $ π _stackπ $ 40.9087pt $ π _stack uncall( )\!:\!π $ =ctx(ℓ2)(if[e1]ℓ1thens1elses2fi[e2]ℓ2) ∼stackπ′ if_true([e2]ℓ2):∼stackπif_true(ℓ1,ℓ2):π′ 122.21983pt $ ctx( _2)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)$ $ π _stackπ $ 83.32724pt $ if\_true([e_2] _2)\!:\!π _stack if\_true( _1, _2)\!:\!π $ =ctx(ℓ2)(if[e1]ℓ1thens1elses2fi[e2]ℓ2) ∼stackπ′ if_false([e2]ℓ2):∼stackπif_false(ℓ1,ℓ2):π′ 122.21983pt $ ctx( _2)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)$ $ π _stackπ $ 85.21613pt $ if\_false([e_2] _2)\!:\!π _stack if\_false( _1, _2)\!:\!π $ ∼stackπ′ loop1([e1]ℓ1,s1,[e2]ℓ2,s2):∼stackπloop1(ℓ1,s1,ℓ2,s2):π′ 21.64478pt $ π _stackπ $ 117.25958pt $ loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π _stack loop1( _1,s_1, _2,s_2)\!:\!π $ ∼stackπ′ loop2([e1]ℓ1,s1,[e2]ℓ2,s2):∼stackπloop2(ℓ1,s1,ℓ2,s2):π′ 21.64478pt $ π _stackπ $ 117.25958pt $ loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π _stack loop2( _1,s_1, _2,s_2)\!:\!π $ Figure 14: Equivalence relation on stacks “∼ _stack” In order to prove this result, we begin by introducing an equivalence relation, ∼ _stack, between the stacks of the small-step semantics configurations and those of the reversible semantics (shown in Fig. 14). Moreover, we also introduce the following auxiliary function, cont, that returns the label of the first block to be executed once the current statement in the control of the configuration (of the small-step semantics) is completed: ((s):π)=(s)(_([e]ℓ):π)=ℓ(_([e]ℓ):π)=ℓ(([e1]ℓ1,s1,[e2]ℓ2,s2):π)=ℓ2(([e1]ℓ1,s1,[e2]ℓ2,s2):π)=ℓ1 array[]rcl cont( seq(s)\!:\!π)&=&entry(s)\\ cont( if\_true([e] )\!:\!π)&=& \\ cont( if\_false([e] )\!:\!π)&=& \\ cont( loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π)&=& _2\\ cont( loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π)&=& _1\\ array In the following, to distinguish them, we denote the configurations of the small-step semantics of the previous section with c,c′,c1,…c,c ,c_1,… and the configurations of the reversible semantics with k,k′,k1,…k,k ,k_1,… We say that two configurations, c=⟨σ,s,π⟩c= σ,s,π and k=⟨σ′,ℓ1,ℓ2,π′⟩k= σ , _1, _2,π , are equivalent, denoted c∼kc _confk, if and only if 1. σ=σ′σ=σ , 2. π∼π′π _stackπ , and 3. either ℓ2=(s) _2=entry(s), or s=s= skip and ℓ2=(π) _2= cont(π). Note that ℓ1 _1 is not relevant when considering only the forward rules. Let us now proceed with the proof of Lemma 3. Proof (⇒)( ) We consider two configurations, c1c_1 and k1k_1, with c1∼k1c_1 _confk_1. We will show that if c1→c2c_1→ c_2, then k1⇀∗k2k_1 k_2 and c2∼k2c_2 _confk_2, since the claim follows trivially from this result. We distinguish the following cases depending on the rule applied: (AssVarS) Then c1=⟨σ,[x⊕=e]ℓ′,π⟩→⟨σ[x↦⟦⊕⟧(σ(x),v),,π⟩=c2c_1= σ,[x~ =e] ,π → σ[x (σ(x),v), skip,π =c_2, with σ⊢e⇓vσ e v. Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ′,π′⟩k_1= σ, , ,π with π∼π′π _stackπ . By rule → AssVar, we have k2=⟨σ[x↦⟦⊕⟧(σ(x),v),ℓ′,ℓ′,π′⟩k_2= σ[x (σ(x),v), , ,π , with ℓ′⟶ℓ′ . Since the top element of the stack π contains the next statement to be executed, and assuming that the CFG correctly represents the control flow of the program, we have ℓ′=(π) = cont(π) and, thus, c2∼k2c_2 _confk_2. (AssArrS) This case is perfectly analogous to the previous one. (CallS) Here, we assume that Γ() (id) returns the body of procedure id, as usual, and Γ′() (id) returns the same statement but excluding the additional statements start and stop that are not considered by the small-step semantics. Then c1=⟨σ,[]ℓ′,π⟩→⟨σ,Γ′(),π⟩=c2c_1= σ,[ call~id] ,π → σ, (id),π =c_2. Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ′,π′⟩k_1= σ, , ,π with π∼π′π _stackπ . By rule → Call, we have k2=⟨σ,(Γ()),ℓ′,(ℓ′):π′⟩k_2= σ,entry( (id)), , call( )\!:\!π , with (Γ())⟶ℓ′entry( (id)) . Trivially, ℓ′ points to the first statement in Γ() (id) which is different from start, i.e., ℓ′=(Γ′()) =entry( (id)). Moreover, since call elements do not affect to the stack equivalence, we have π∼(ℓ′):π′π _stack call( )\!:\!π and, thus, c2∼k2c_2 _confk_2. (UnCallS) This case is perfectly analogous to the previous one. (Seq1) Then c1=⟨σ,s1s2,π⟩→⟨σ,s1,(s2):π⟩=c2c_1= σ,s_1~s_2,π → σ,s_1, seq(s_2)\!:\!π =c_2. Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ′,π′⟩k_1= σ, , ,π with ℓ′=(s1s2)=(s1) =entry(s_1~s_2)=entry(s_1) and π∼π′π _stackπ . Hence, the claim follows by applying zero steps in the reversible semantics since (s2):π∼π′ seq(s_2)\!:\!π _stackπ and, thus, c2∼k1=k2c_2 _confk_1=k_2. (Seq2) Then c1=⟨σ,,(s2):π⟩→⟨σ,s2,π⟩=c2c_1= σ, skip, seq(s_2)\!:\!π → σ,s_2,π =c_2. Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ′,π′⟩k_1= σ, , ,π with ℓ′=(s2) =entry(s_2) and (s2):π∼π′ seq(s_2)\!:\!π _stackπ (thus, π∼π′π _confπ ). Hence, the claim follows by applying zero steps in the reversible semantics since c2∼k1=k2c_2 _confk_1=k_2. (IfTrue1) Then c1=⟨σ,[e1]ℓ1s1s2[e2]ℓ2,π⟩→⟨σ,s1,_([e2]ℓ2):π⟩=c2c_1= σ, if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2,π → σ,s_1, if\_true([e_2] _2)\!:\!π =c_2 with σ⊢e1⇓v1σ e_1 v_1 and _?(v1) is\_true?(v_1). Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ1,π′⟩k_1= σ, , _1,π with π∼π′π _stackπ . By applying rule IfTrue1→ IfTrue1, we have k2=⟨σ,ℓ2,(s1),_(ℓ1,ℓ2):π′⟩k_2= σ, _2,entry(s_1), if\_true( _1, _2)\!:\!π . Hence, c2∼k2c_2 _confk_2 follows trivially since _([e2]ℓ2):π∼_(ℓ1,ℓ2):π′ if\_true([e_2] _2)\!:\!π _stack if\_true( _1, _2)\!:\!π . (IfTrue2) Then c1=⟨σ,,_([e2]ℓ2):π⟩→⟨σ,,π⟩=c2c_1= σ, skip, if\_true([e_2] _2)\!:\!π → σ, skip,π =c_2. Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ2,_(ℓ1,ℓ2):π′⟩k_1= σ, , _2, if\_true( _1, _2)\!:\!π with π∼π′π _stackπ . By rule IfTrue2→ IfTrue2, we have k2=⟨σ,ℓ2,ℓ2′,π′⟩k_2= σ, _2, _2 ,π with ℓ2⟶ℓ2′ _2 _2. Since the top element of the stack π contains the next statement to be executed, assuming that the CFG correctly represents the control flow of the program, we have ℓ2′=(π) _2= cont(π) and, thus, c2∼k2c_2 _confk_2. (IfFalse1) and (IfFalse2) These cases are perfectly analogous to the previous two cases. (LoopMainS) Then, we have c1=⟨σ,[e1]ℓ1s1s2[e2]ℓ2),π⟩→⟨σ,s1,([e1]ℓ1,s2,[e2]ℓ2,s2):π⟩=c2c_1= σ, from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2),π → σ,s_1, loop1([e_1] _1,s_2,[e_2] _2,s_2)\!:\!π =c_2 with σ⊢e1⇓v1σ e_1 v_1 and _?(v1) is\_true?(v_1). Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ1,π′⟩k_1= σ, , _1,π with π∼π′π _stackπ . By rule → LoopMain, we have k2=⟨σ,ℓ1,(s1),(ℓ1,s1,ℓ2,s2):π′⟩k_2= σ, _1,entry(s_1), loop1( _1,s_1, _2,s_2)\!:\!π . Hence, ([e1]ℓ1,s1,[e2]ℓ2,s2):π∼(ℓ1,s1,ℓ2,s2):π′ loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π _stack loop1( _1,s_1, _2,s_2)\!:\!π and, thus, c2∼k2c_2 _confk_2. (LoopBaseS) Then c1=⟨σ,,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩→⟨σ,,π⟩=c2c_1= σ, skip, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π → σ, skip,π =c_2, with σ⊢e2⇓v2σ e_2 v_2 and _?(v2) is\_true?(v_2). Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ2,(ℓ1,s1,ℓ2,s2):π′⟩k_1= σ, , _2, loop1( _1,s_1, _2,s_2)\!:\!π and, moreover, ([e1]ℓ1,s1,[e2]ℓ2,s2):π∼(ℓ1,s1,ℓ2,s2):π′ loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π _stack loop1( _1,s_1, _2,s_2)\!:\!π (and thus π∼π′π _stackπ ). By rule → LoopBase, we have k2=⟨σ,ℓ2,ℓ2′,π′⟩k_2= σ, _2, _2 ,π with ℓ2⟶ℓ2′ _2 _2 and ℓ2′≠(s1) _2 (s_1). Since the top element of the stack π contains the next statement to be executed once the loop is completed, assuming that the CFG correctly represents the control flow of the program, we have ℓ2′=(π) _2= cont(π) and, thus, c2∼k2c_2 _confk_2. (Loop1) Then, we have the step c1=⟨σ,,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩→⟨σ,s2,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩=c2c_1= σ, skip, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π → σ,s_2, loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π =c_2, with σ⊢e2⇓v2σ e_2 v_2 and _?(v2) is\_false?(v_2). Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ2,(ℓ1,s1,ℓ2,s2):π′⟩k_1= σ, , _2, loop1( _1,s_1, _2,s_2)\!:\!π , where ([e1]ℓ1,s1,[e2]ℓ2,s2):π∼(ℓ1,s1,ℓ2,s2):π′ loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π _stack loop1( _1,s_1, _2,s_2)\!:\!π . By rule Loop1→ Loop1, we have k2=⟨σ,ℓ2,(s2),(ℓ1,s1,ℓ2,s2):π′⟩k_2= σ, _2,entry(s_2), loop2( _1,s_1, _2,s_2)\!:\!π and c2∼k2c_2 _confk_2 holds. (Loop2) Then, we have the step c1=⟨σ,,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩→⟨σ,s1,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩=c2c_1= σ, skip, loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π → σ,s_1, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π =c_2, with σ⊢e1⇓v1σ e_1 v_1 and _?(v1) is\_false?(v_1). Since c1∼k1c_1 _confk_1, we have k1=⟨σ,ℓ,ℓ1,(ℓ1,s1,ℓ2,s2):π′⟩k_1= σ, , _1, loop2( _1,s_1, _2,s_2)\!:\!π , where ([e1]ℓ1,s1,[e2]ℓ2,s2):π∼(ℓ1,s1,ℓ2,s2):π′ loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π _stack loop2( _1,s_1, _2,s_2)\!:\!π . By rule Loop2→ Loop2, we have k2=⟨σ,ℓ1,(s1),(ℓ1,s1,ℓ2,s2):π′⟩k_2= σ, _1,entry(s_1), loop1( _1,s_1, _2,s_2)\!:\!π and c2∼k2c_2 _confk_2 holds. (⇐ ) Again, we consider two configurations, c1c_1 and k1k_1, with c1∼k1c_1 _confk_1. Now, we will show that if k1⇀k2k_1 k_2, then c1→∗c2c_1→ c_2 and c2∼k2c_2 _confk_2, since the claim follows trivially from this result. We distinguish the following cases depending on the rule applied: (→ AssVar) Then, k1=⟨σ,ℓ,ℓ′,π′⟩⇀⟨σ[x↦⟦⊕⟧(σ(x),v)],ℓ′,ℓ′,π′⟩=k2k_1= σ, , ,π σ[x (σ(x),v)], , ,π =k_2, with (ℓ′)=(x⊕=e)block( )=(x~ =e), σ⊢e⇓vσ e v, and ℓ′⟶ℓ′ . Since c1∼k1c_1 _confk_1, we have that c1=⟨σ,s,π⟩c_1= σ,s,π where π∼π′π _stackπ and, thus, s can be either [x⊕=e]ℓ′[x~ =e] , a sequence whose first statement is [x⊕=e]ℓ′[x~ =e] , or skip with ℓ′=(π) = cont(π). W.l.o.g, let us consider the second case (the other two cases would be similar). Then, we have a derivation of the form c1→∗⟨σ,x⊕=e,π2⟩=c1′c_1→ σ,x~ =e, _2 =c _1 such that π2∼π′ _2 _stackπ since only seq elements have been added to the stack. Now, by rule AssVarS, we have c1′→⟨σ[x↦⟦⊕⟧(σ(x),v)],,π2⟩c _1→ σ[x (σ(x),v)], skip, _2 and the claim follows since the top element of the stack π2 _2 contains the next statement to be executed and, assuming that the CFG correctly represents the control flow of the program, we have ℓ′=(π2) = cont( _2). (→ AssArrS) This case is perfectly analogous to the previous one. (→ Call) As in the proof above, we assume that Γ′() (id) returns the body of procedure id excluding the statements start and stop. Then, we have k1=⟨σ,ℓ,ℓ′,π′⟩⇀⟨σ,(Γ(id)),ℓ′,(ℓ′):π′⟩=k2k_1= σ, , ,π σ,entry( (id)), , call( )\!:\!π =k_2, with (ℓ′)=(id)block( )=( call~id) and (Γ(id))⟶ℓ′entry( (id)) . Since c1∼k1c_1 _confk_1, we have that c1=⟨σ,,π⟩c_1= σ, call~id,π with π∼π′π _stackπ .444For simplicity, in this case and subsequent ones, we will ignore the possibility of the configuration having a sequence in the control. Otherwise, we would have to proceed as in the first case and perform a number of steps with rules Seq1 and/or Seq2. By rule CallS, we have c1→⟨σ,Γ′(id),π⟩=c2c_1→ σ, (id),π =c_2. Trivially, ℓ′ points to the first statement in Γ() (id) which is different from start, i.e., ℓ′ points to (Γ′())entry( (id)). Moreover, since call elements do not affect to the stack equivalence, we have c2∼k2c_2 _confk_2. (Return1→ Return1) Then, we have k1=⟨σ,ℓ,ℓ′,(ℓ′):π′⟩⇀⟨σ,ℓ′,ℓ′,π′⟩=k2k_1= σ, , , call( )\!:\!π σ, , ,π =k_2, with (ℓ′)=block( )= stop and ℓ′⟶ℓ′ in the CFG. Then, since c1∼k1c_1 _confk_1, we have c1=⟨σ,,π⟩c_1= σ, skip,π with π∼π′π _stackπ and (π) cont(π) pointing to the next statement after the call. In the small-step semantics, there is no rule to model the return of a procedure since, once the execution of the procedure body is completed, execution simply continues with the next statement after the corresponding call. Assuming that call was part of a sequence (otherwise, execution is done), π will have the form (s):π2 seq(s)\!:\! _2, where s is the next statement to be executed after the call. Therefore, applying rule Seq2, we have c1→⟨σ,s,π2⟩c_1→ σ,s, _2 and the claim follows since ℓ′=(s) =entry(s), and π2∼π′ _2 _stackπ also holds since seq elements are not considered by the relation “∼ _stack”. (→ UnCall and Return2→ Return2) These cases are perfectly analogous to the previous two cases. (→ Skip) Then, we have k1=⟨σ,ℓ,ℓ′,π′⟩⇀⟨σ,ℓ′,ℓ′,π′⟩=k2k_1= σ, , ,π σ, , ,π =k_2, with (ℓ′)=block( )= skip and ℓ′⟶ℓ′ in the CFG. Since c1=k1c_1=k_1, we have c1=⟨σ,,π⟩c_1= σ, skip,π with π∼π′π _stackπ . We note that rule → Skip is needed in the reversible semantics only in case there is a statement skip in the program. In contrast, within the small-step semantics, a similar rule is not necessary since it will simply be dealt with as any other “finished” statement (the execution of all statements ends with skip). Therefore, we consider a zero-step derivation with c1=c2c_1=c_2, and c2∼k2c_2 _confk_2 holds since c1∼k1c_1 _confk_1 and, thus, ℓ′=ℓ′=(π) = = cont(π). (IfTrue1→ IfTrue1 Then, k1=⟨σ,ℓ,ℓ1,π′⟩⇀⟨σ,ℓ1,(s1),_(ℓ1,ℓ2):π′⟩=k2k_1= σ, , _1,π σ, _1,entry(s_1), if\_true( _1, _2)\!:\!π =k_2, with (ℓ1)=e1block( _1)=e_1, (ℓ1)=([e1]ℓ1s1s2[e2]ℓ2) ctx( _1)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2), σ⊢e1⇓v1σ e_1 v_1, and _?(v1) is\_true?(v_1). Since c1∼k1c_1 _confk_1 holds, we have that c1=⟨σ,[e1]ℓ1s1s2[e2]ℓ2,π⟩c_1= σ, if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2,π with π∼π′π _stackπ . By rule IfTrue1, we derive c2=⟨σ,s1,_(e2):π⟩c_2= σ,s_1, if\_true(e_2)\!:\!π and the claim follows. (IfTrue2→ IfTrue2) Then, we have k1=⟨σ,ℓ,ℓ2,_(ℓ1,ℓ2):π′⟩⇀⟨σ,ℓ2,ℓ2′,π′⟩=k2k_1= σ, , _2, if\_true( _1, _2)\!:\!π σ, _2, _2,π =k_2, with (ℓ2)=e2block( _2)=e_2, σ⊢e2⇓v2σ e_2 v_2, _?(v2) is\_true?(v_2), and ℓ2⟶ℓ2′ _2 _2. Since c1∼k1c_1 _confk_1, we have that c1=⟨σ,,_([e2]ℓ2):π⟩c_1= σ, skip, if\_true([e_2] _2)\!:\!π with π∼π′π _stackπ . By rule IfTrue2, we have c1→⟨σ,,π⟩=c2c_1→ σ, skip,π =c_2. Hence, assuming that the CFG correctly represents the control flow of the program, we have that ℓ2′=(π) _2= cont(π) points to the next statement in the stack to be executed after the conditional and, thus, c2∼k2c_2 _confk_2. (IfFalse1→ IfFalse1 and IfFalse2→ IfFalse2) These cases are perfectly analogous to the previous two cases. (→ LoopMain) Then, k1=⟨σ,ℓ,ℓ1,π′⟩⇀⟨σ,ℓ1,(s1),(ℓ1,s1,ℓ2,s2):π′⟩=k2k_1= σ, , _1,π σ, _1,entry(s_1), loop1( _1,s_1, _2,s_2)\!:\!π =k_2, with (ℓ1)=e1block( _1)=e_1, (ℓ1)=([e1]ℓ1s1s2[e2]ℓ2) ctx( _1)=( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2), σ⊢e1⇓v1σ e_1 v_1, and _?(v1) is\_true?(v_1). Since c1∼k1c_1 _confk_1 holds, we have that c1=⟨σ,[e1]ℓ1s1s2[e2]ℓ2,π⟩c_1= σ, from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2,π with π∼π′π _stackπ . By rule LoopMainS, we derive c2=⟨σ,s1,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩c_2= σ,s_1, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π and the claim follows. (→ LoopBase) Then, k1=⟨σ,ℓ,ℓ2,(ℓ1,s1,ℓ2,s2):π′⟩⇀⟨σ,ℓ2,ℓ2′,π′⟩=k2k_1= σ, , _2, loop1( _1,s_1, _2,s_2)\!:\!π σ, _2, _2,π =k_2, with (ℓ2)=e2block( _2)=e_2, σ⊢e2⇓v2σ e_2 v_2, _?(v2) is\_true?(v_2), ℓ2⟶ℓ2′ _2 _2 in the CFG, and ℓ2′≠(s1) _2 (s_1). Since c1∼k1c_1 _confk_1, we have c1=⟨σ,,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩c_1= σ, skip, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π with π∼π′π _stackπ . By rule LoopBaseS, we have c1→⟨σ,,π⟩=c2c_1→ σ, skip,π =c_2. Hence, assuming that the CFG correctly represents the control flow of the program, we have that ℓ2′=(π) _2= cont(π) points to the next statement in the stack to be executed after the loop and, thus, c2∼k2c_2 _confk_2. (Loop1→ Loop1) Then, we have the following step k1=⟨σ,ℓ,ℓ2,(ℓ1,s1,ℓ2,s2):π′⟩⇀⟨σ,ℓ2,(s2),(ℓ1,s1,ℓ2,s2):π′⟩=k2k_1= σ, , _2, loop1( _1,s_1, _2,s_2)\!:\!π σ, _2,entry(s_2), loop2( _1,s_1, _2,s_2)\!:\!π =k_2, with (ℓ2)=e2block( _2)=e_2, σ⊢e2⇓v2σ e_2 v_2, and _?(v2) is\_false?(v_2). Since c1∼k1c_1 _confk_1 holds, we have that c1=⟨σ,,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩c_1= σ, skip, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π with π∼π′π _stackπ . By rule Loop1, we derive c2=⟨σ,s2,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩c_2= σ,s_2, loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π and the claim follows. (Loop2→ Loop2) Then, we have the following step k1=⟨σ,ℓ,ℓ1,(ℓ1,s1,ℓ2,s2):π′⟩⇀⟨σ,ℓ1,(s1),(ℓ1,s1,ℓ2,s2):π′⟩=k2k_1= σ, , _1, loop1( _1,s_1, _2,s_2)\!:\!π σ, _1,entry(s_1), loop1( _1,s_1, _2,s_2)\!:\!π =k_2, with (ℓ1)=e1block( _1)=e_1, σ⊢e1⇓v1σ e_1 v_1, and _?(v1) is\_false?(v_1). Since c1∼k1c_1 _confk_1 holds, we have that c1=⟨σ,,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩c_1= σ, skip, loop2([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π with π∼π′π _stackπ . By rule Loop2, we derive c2=⟨σ,s1,([e1]ℓ1,s1,[e2]ℓ2,s2):π⟩c_2= σ,s_1, loop1([e_1] _1,s_1,[e_2] _2,s_2)\!:\!π and the claim follows. ∎ Example 1 Given the program in Fig. 8 (and the CFG in Fig. 11), we have the forward derivation shown in Figure 15, where we highlight in red the “active” label in each step (i.e., the label that represents the next statement to be executed by the forward reversible semantics). ⟨ϵ,1,2,[]⟩→⟨n↦3,2,3,[]⟩→⟨n↦3,5,6,(3):[]⟩→⟨n↦3,i↦1,6,7,(3):[]⟩→⟨n↦3,i↦1,7,8,(7,s1,13,s2):(3):[]⟩IfFalse1→⟨n↦3,i↦1,8,10,_(8,11):(7,s1,13,s2):(3):[]⟩→⟨n↦3,i↦1,10,11,_(8,11):(7,s1,13,s2):(3):[]⟩IfFalse2→⟨n↦3,i↦1,11,13,(7,s1,13,s2):(3):[]⟩Loop1→⟨n↦3,i↦1,13,12,(7,s1,13,s2):(3):[]⟩→⟨n↦3,i↦2,12,7,(7,s1,13,s2):(3):[]⟩Loop2→⟨n↦3,i↦2,7,8,(7,s1,13,s2):(3):[]⟩IfFalse1→⟨n↦3,i↦2,8,10,_(8,11):(7,s1,13,s2):(3):[]⟩→⟨n↦3,i↦2,10,11,_(8,11):(7,s1,13,s2):(3):[]⟩IfFalse2→⟨n↦3,i↦2,11,13,(7,s1,13,s2):(3):[]⟩Loop1→⟨n↦3,i↦2,13,12,(7,s1,13,s2):(3):[]⟩→⟨n↦3,i↦3,12,7,(7,s1,13,s2):(3):[]⟩Loop2→⟨n↦3,i↦3,7,8,(7,s1,13,s2):(3):[]⟩IfTrue1→⟨n↦3,i↦3,8,9,_(8,11):(7,s1,13,s2):(3):[]⟩→⟨n↦3,i↦3,total↦3,9,11,_(8,11):(7,s1,13,s2):(3):[]⟩IfTrue2→⟨n↦3,i↦3,total↦3,11,13,(7,s1,13,s2):(3):[]⟩→⟨n↦3,i↦3,total↦3,13,14,(3):[]⟩→⟨n↦6,i↦3,total↦3,14,15,(3):[]⟩Return1→⟨n↦6,i↦3,total↦3,3,4,[]⟩ array[]rl& ε,1, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,02,[\>] \\ _ AssVar& \n 3\,2, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,03,[\>] \\ _ Call& \n 3\,5, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,06, call(3)\!:\![\>] \\ _ AssVar& \n 3,i 1\,6, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,07, call(3)\!:\![\>] \\ _ LoopMain& \n 3,i 1\,7, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,08, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse1& \n 3,i 1\,8, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,010, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Skip& \n 3,i 1\,10, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,011, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse2& \n 3,i 1\,11, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,013, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop1& \n 3,i 1\,13, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,012, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ AssVar& \n 3,i 2\,12, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,07, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop2& \n 3,i 2\,7, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,08, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse1& \n 3,i 2\,8, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,010, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Skip& \n 3,i 2\,10, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,011, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse2& \n 3,i 2\,11, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,013, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop1& \n 3,i 2\,13, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,012, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ AssVar& \n 3,i 3\,12, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,07, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop2& \n 3,i 3\,7, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,08, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfTrue1& \n 3,i 3\,8, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,09, if\_true(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ AssVar& \n 3,i 3,total 3\,9, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,011, if\_true(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfTrue2& \n 3,i 3,total 3\,11, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,013, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ LoopBase& \n 3,i 3,total 3\,13, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,014, call(3)\!:\![\>] \\ _ AssVar& \n 6,i 3,total 3\,14, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,015, call(3)\!:\![\>] \\ _ Return1& \n 6,i 3,total 3\,3, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,04,[\>] \\ array Figure 15: Forward derivation with the reversible semantics 4.2 The Backward Rules This section introduces the rules of the backward reversible semantics. Basically, a backward rule operates as follows: it first identifies the statement referenced by the first label within the configuration control (i.e., the label corresponding to the last executed statement), then undoes its effects, and finally updates the labels accordingly (mainly traversing the original CFG backwards). In the following, −1flow^-1 denotes the function that computes the inverse CFG of a program: −1(s)=(ℓ′,ℓ)∣(ℓ,ℓ′)∈(s)flow^-1(s)=\( , ) ( , ) (s)\. For clarity, in the transition rules of the backward semantics, we denote the edges (ℓ,ℓ′)∈−1(s)( , ) ^-1(s) of the inverse CFG as ℓ⟶-1ℓ′ -1 ; i.e., ℓ⟶-1ℓ′ -1 is equivalent to ℓ′⟶ℓ in the original CFG. The following result states the equivalence between computing the inverse CFG of a statement and a standard CFG of the corresponding inverse statement: Lemma 4 Given a statement s, we have −1(s)=(ℐ⟦s⟧)flow^-1(s)=flow(I s ). Proof We prove the claim by structural induction on the considered statement. For elementary blocks, the proof follows trivially. Let us now consider the remaining cases: • Let s=([e1]ℓ1s1s2[e2]ℓ2)s=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2). Then, we have (ℐ⟦s⟧)=([e2]ℓ2ℐ⟦s1⟧ℐ⟦s2⟧[e1]ℓ1)=(ℓ2,(ℐ⟦s1⟧)),((ℐ⟦s1⟧),ℓ1),(ℓ2,(ℐ⟦s2⟧)),((ℐ⟦s2⟧),ℓ1)∪(ℐ⟦s1⟧)∪(ℐ⟦s2⟧)=(ℓ2,(s1)),((s1),ℓ1),(ℓ2,(s2)),((s2),ℓ1)∪(ℐ⟦s1⟧)∪(ℐ⟦s2⟧)=(ℓ2,(s1)),((s1),ℓ1),(ℓ2,(s2)),((s2),ℓ1)∪−1(s1)∪−1(s2)(by ind. hypothesis)=−1(s) array[]lflow(I s )&=&flow( if~[e_2] _2~ then~I s_1 ~ else~I s_2 ~ fi~[e_1] _1)\\ &=&\( _2,entry(I s_1 )),(exit(I s_1 ), _1),\\ &&~~( _2,entry(I s_2 )),(exit(I s_2 ), _1)\\\ &&~~ (I s_1 ) (I s_2 )\\ &=&\( _2,exit(s_1)),(entry(s_1), _1),( _2,exit(s_2)),(entry(s_2), _1)\\\ &&~~ (I s_1 ) (I s_2 )\\ &=&\( _2,exit(s_1)),(entry(s_1), _1),( _2,exit(s_2)),(entry(s_2), _1)\\\ &&~~ ^-1(s_1) ^-1(s_2)~~~ (by ind.\ hypothesis)\\ &=&flow^-1(s) array assuming that (ℐ⟦s⟧)=(s)entry(I s )=exit(s) and that (ℐ⟦s⟧)=(s)exit(I s )=entry(s), which is straightforward. • Let s=([e1]ℓ1s1s2[e2]ℓ2)s=( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2). Then, we have (ℐ⟦s⟧)=([e2]ℓ2ℐ⟦s1⟧ℐ⟦s2⟧[e1]ℓ1)=(ℓ2,(ℐ⟦s1⟧)),((ℐ⟦s1⟧),ℓ1),(ℓ1,(ℐ⟦s2⟧)),((ℐ⟦s2⟧),ℓ2)∪(ℐ⟦s1⟧)∪(ℐ⟦s2⟧)=(ℓ2,(s1)),((s1),ℓ1),(ℓ1,(s2)),((s2),ℓ2)∪(ℐ⟦s1⟧)∪(ℐ⟦s2⟧)=(ℓ2,(s1)),((s1),ℓ1),(ℓ1,(s2)),((s2),ℓ2)∪−1(s1)∪−1(s2)(by ind. hypothesis)=−1(s) array[]lflow(I s )&=&flow( from~[e_2] _2~ do~I s_1 ~ loop~I s_2 ~ until~[e_1] _1)\\ &=&\( _2,entry(I s_1 )),(exit(I s_1 ), _1),\\ &&~~( _1,entry(I s_2 )),(exit(I s_2 ), _2)\\\ &&~~ (I s_1 ) (I s_2 )\\ &=&\( _2,exit(s_1)),(entry(s_1), _1),( _1,exit(s_2)),(entry(s_2), _2)\\\ &&~~ (I s_1 ) (I s_2 )\\ &=&\( _2,exit(s_1)),(entry(s_1), _1),( _1,exit(s_2)),(entry(s_2), _2)\\\ &&~~ ^-1(s_1) ^-1(s_2)~~~ (by ind.\ hypothesis)\\ &=&flow^-1(s) array • Finally, let s=(s1s2)s=(s_1~s_2). Then, we have (ℐ⟦s1s2⟧)=(ℐ⟦s2⟧ℐ⟦s1⟧)=((ℐ⟦s2⟧),(ℐ⟦s1⟧))∪(ℐ⟦s2⟧)∪(ℐ⟦s1⟧)=((s2),(s1))∪(ℐ⟦s2⟧)∪(ℐ⟦s1⟧)=((s2),(s1))∪−1(s2)∪−1(s1)(by IH)=−1(s1s2) array[]lflow(I s_1~s_2 )&=&flow(I s_2 ~I s_1 )\\ &=&\(exit(I s_2 ),entry(I s_1 ))\ (I s_2 ) (I s_1 )\\ &=&\(entry(s_2),exit(s_1))\ (I s_2 ) (I s_1 )\\ &=&\(entry(s_2),exit(s_1))\ ^-1(s_2) ^-1(s_1)~~~ (by IH)\\ &=&flow^-1(s_1~s_2)\\ array ∎ ← AssVar =block(ℓ′)(=x⊕e) ⊢σ⇓ev ⟶-1ℓ′ℓ′ ↽⟨σ,ℓ′,ℓ′,π⟩⟨σ[↦xIop⟦⊕⟧(σ(x),v)],ℓ,ℓ′,π⟩ 99.74849pt $ ( )=(x~ =e)$ $ σ e v$ $ -1 $ 96.5411pt $ σ, , ,π σ[x _op (σ(x),v)], , ,π $ ← AssArr =block(ℓ′)(=x[el]⊕e) ⊢σ⇓elvl ⊢σ⇓ev ⟶-1ℓ′ℓ′ ↽⟨σ,ℓ′,ℓ′,π⟩⟨σ[↦x[vl]Iop⟦⊕⟧(σ(x[vl]),v)],ℓ,ℓ′,π⟩ 137.52449pt $ ( )=(x[e_l]~ =e)$ $ σ e_l v_l$ $ σ e v$ $ -1 $ 110.37215pt $ σ, , ,π σ[x[v_l] _op (σ(x[v_l]),v)], , ,π $ ← Call =block(ℓs)start ⟶-1ℓ′ℓ ↽⟨:σ,ℓs,ℓ′,call(ℓ′)π⟩⟨σ,ℓ,ℓ′,π⟩ 55.56635pt $ ( _s)= start$ $ -1 $ 68.8432pt $ σ, _s, , call( )\!:\!π σ, , ,π $ Return1← Return1 =block(ℓ′)(callid) ⟶-1exit(Γ(id))ℓ ↽⟨σ,ℓ′,ℓ′,π⟩⟨:σ,ℓ,exit(Γ(id)),call(ℓ′)π⟩ 84.08572pt $ ( )=( call~id)$ $ ( (id)) -1 $ 90.05324pt $ σ, , ,π σ, ,exit( (id)), call( )\!:\!π $ ← UnCall =block(ℓs)start ⟶-1ℓ′ℓ ↽⟨:σ,ℓs,ℓ′,uncall(ℓ′)π⟩⟨σ,ℓ,ℓ′,π⟩ 55.56635pt $ ( _s)= start$ $ -1 $ 74.00987pt $ σ, _s, , uncall( )\!:\!π σ, , ,π $ Return2← Return2 =block(ℓ′)(uncallid) ⟶-1exit(Γ(id-1))ℓ ↽⟨σ,ℓ′,ℓ′,π⟩⟨:σ,ℓ,exit(Γ(id-1)),uncall(ℓ′)π⟩ 92.8427pt $ ( )=( uncall~id)$ $ ( (id^-1)) -1 $ 98.8102pt $ σ, , ,π σ, ,exit( (id^-1)), uncall( )\!:\!π $ ← Skip =block(ℓ′)skip ⟶-1ℓ′ℓ′ ↽⟨σ,ℓ′,ℓ′,π⟩⟨σ,ℓ,ℓ′,π⟩ 56.02641pt $ ( )= skip$ $ -1 $ 53.4421pt $ σ, , ,π σ, , ,π $ Figure 16: Reversible backward semantics: rules for basic constructs Let us now present the transition relation, ↽ , defining the backward direction of the reversible semantics. The backward rules for basic constructs are shown in Figure 16. In principle, each rule ← Rule represents the inverse version of the corresponding forward rule Rule→ Rule from Fig. 12, executing the inverse of the last executed statement (pointed to by the first label in the control of the configuration) and advancing in the inverse CFG (equivalently, moving backwards in the standard CFG). In particular, note that the rules ← Call and ← Uncall are triggered upon reaching the statement start, whereas in the forward rules Return1→ Return1 and Return2→ Return2, the trigger was reaching the stop statement. IfTrue1← IfTrue1 =block(ℓ1)e1 ⊢σ⇓e1v1 is_true?(v1) ⟶-1ℓ1ℓ ↽⟨:σ,ℓ1,ℓ′1,if_true(ℓ1,ℓ2)π⟩⟨σ,ℓ,ℓ1,π⟩ 131.80128pt $ ( _1)=e_1$ $ $ $ σ e_1 v_1$ $ is\_true?(v_1)$ $ _1 -1 $ 83.80331pt $ σ, _1, _1, if\_true( _1, _2)\!:\!π σ, , _1,π $ IfTrue2← IfTrue2 =block(ℓ2)e2 =ctx(ℓ2)(if[e1]ℓ1thens1elses2fi[e2]ℓ2) ⊢σ⇓e2v2 is_true?(v2) ↽⟨σ,ℓ2,ℓ′2,π⟩⟨:σ,exit(s1),ℓ2,if_true(ℓ1,ℓ2)π⟩ 159.40375pt $ ( _2)=e_2$ $ ctx( _2)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)$ $ σ e_2 v_2$ $ is\_true?(v_2)$ 97.17621pt $ σ, _2, _2,π σ,exit(s_1), _2, if\_true( _1, _2)\!:\!π $ IfFalse1← IfFalse1 =block(ℓ1)e1 ⊢σ⇓e1v1 is_false?(v1) ⟶-1ℓ1ℓ ↽⟨:σ,ℓ1,ℓ′1,if_false(ℓ1,ℓ2)π⟩⟨σ,ℓ,ℓ1,π⟩ 132.74573pt $ ( _1)=e_1$ $ $ $ σ e_1 v_1$ $ is\_false?(v_1)$ $ _1 -1 $ 84.74776pt $ σ, _1, _1, if\_false( _1, _2)\!:\!π σ, , _1,π $ IfFalse2← IfFalse2 =block(ℓ2)e2 =ctx(ℓ2)(if[e1]ℓ1thens1elses2fi[e2]ℓ2) ⊢σ⇓e2v2 is_false?(v2) ↽⟨σ,ℓ2,ℓ′2,π⟩⟨:σ,exit(s2),ℓ2,if_false(ℓ1,ℓ2)π⟩ 160.34819pt $ ( _2)=e_2$ $ ctx( _2)=( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2)$ $ σ e_2 v_2$ $ is\_false?(v_2)$ 98.12065pt $ σ, _2, _2,π σ,exit(s_2), _2, if\_false( _1, _2)\!:\!π $ ← LoopMain =block(ℓ1)e1 ⊢σ⇓e1v1 is_true?(v1) ⟶-1ℓ1ℓ ≠ℓexit(s2) ↽⟨:σ,ℓ1,ℓ′,loop1(ℓ1,s1,ℓ2,s2)π⟩⟨σ,ℓ,ℓ1,π⟩ 155.31303pt $ ( _1)=e_1$ $ σ e_1 v_1$ $ is\_true?(v_1)$ $ _1 -1 $ $ (s_2)$ 94.04636pt $ σ, _1, , loop1( _1,s_1, _2,s_2)\!:\!π σ, , _1,π $ ← LoopBase =block(ℓ2)e2 =ctx(ℓ2)(from[e1]ℓ1dos1loops2until[e2]ℓ2) ⊢σ⇓e2v2 is_true?(v2) ↽⟨σ,ℓ2,ℓ′2,π⟩⟨:σ,exit(s1),ℓ2,loop1(ℓ1,s1,ℓ2,s2)π⟩ 170.2788pt $ ( _2)=e_2$ $ ctx( _2)=( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2)$ $ σ e_2 v_2$ $ is\_true?(v_2)$ 107.41925pt $ σ, _2, _2,π σ,exit(s_1), _2, loop1( _1,s_1, _2,s_2)\!:\!π $ Loop1← Loop1 =block(ℓ2)e2 ⊢σ⇓e2v2 is_false?(v2) ↽⟨:σ,ℓ2,ℓ′,loop2(ℓ1,s1,ℓ2,s2)π⟩⟨:σ,exit(s1),ℓ2,loop1(ℓ1,s1,ℓ2,s2)π⟩ 99.70395pt $ ( _2)=e_2$ $ σ e_2 v_2$ $ is\_false?(v_2)$ 147.49573pt $ σ, _2, , loop2( _1,s_1, _2,s_2)\!:\!π σ,exit(s_1), _2, loop1( _1,s_1, _2,s_2)\!:\!π $ Loop2← Loop2 =block(ℓ1)e1 ⊢σ⇓e1v1 is_false?(v1) ↽⟨:σ,ℓ1,ℓ′,loop1(ℓ1,s1,ℓ2,s2)π⟩⟨:σ,exit(s2),ℓ1,loop2(ℓ1,s1,ℓ2,s2)π⟩ 99.70395pt $ ( _1)=e_1$ $ σ e_1 v_1$ $ is\_false?(v_1)$ 147.49573pt $ σ, _1, , loop1( _1,s_1, _2,s_2)\!:\!π σ,exit(s_2), _1, loop2( _1,s_1, _2,s_2)\!:\!π $ Figure 17: Reversible backward semantics: rules for if and for loop The backward rules for conditional and loop statements are in Figure 17. As before, each rule ← Rule represents the inverse version of the corresponding forward rule Rule→ Rule from Fig. 13. Let us emphasize only that conditionals and loops are now undone from end to start; consequently, the rules IfTrue2← IfTrue2 and IfFalse2← IfFalse2 now inspect the context of the label to determine whether it corresponds to a conditional assertion or a loop test, and push a new element onto the stack (while this was done in the forward semantics in rules IfTrue1→ IfTrue1 and IfFalse1→ IfFalse1). Similarly, for loops, it is rule ← LoopBase that now inspects the context (and push a new element onto the stack). Conversely, the loop now terminates with the rule ← LoopMain. Here, we verify that ℓ≠(s2) (s_2), since there are two outgoing edges in the inverse CFG: one that backtracks to the statement preceding the loop (the one of interest), and another one that reverses a further iteration by jumping to the exit of s2s_2. This condition ensures that the correct path is followed. Example 2 Consider the derivation shown in Example 1. Starting from the last configuration, we have the backward derivation shown in Figure 18. As in the previous example, we highlight in red the “active” label in each step (i.e., the label that represents the last executed statement). ⟨n↦6,i↦3,total↦3,3,4,[]⟩Return1←⟨n↦6,i↦3,total↦3,14,15,(3):[]⟩←⟨n↦3,i↦3,total↦3,13,14,(3):[]⟩←⟨n↦3,i↦3,total↦3,11,13,(7,s1,13,s2):(3):[]⟩IfTrue2←⟨n↦3,i↦3,total↦3,9,11,_(8,11):(7,s1,13,s2):(3):[]⟩←⟨n↦3,i↦3,8,9,_(8,11):(7,s1,13,s2):(3):[]⟩IfTrue1←⟨n↦3,i↦3,7,8,(7,s1,13,s2):(3):[]⟩Loop2←⟨n↦3,i↦3,12,7,(7,s1,13,s2):(3):[]⟩←⟨n↦3,i↦2,13,12,(7,s1,13,s2):(3):[]⟩Loop1←⟨n↦3,i↦2,11,13,(7,s1,13,s2):(3):[]⟩IfFalse2←⟨n↦3,i↦2,10,11,_(8,11):(7,s1,13,s2):(3):[]⟩←⟨n↦3,i↦2,8,10,_(8,11):(7,s1,13,s2):(3):[]⟩IfFalse1←⟨n↦3,i↦2,7,8,(7,s1,13,s2):(3):[]⟩Loop2←⟨n↦3,i↦2,12,7,(7,s1,13,s2):(3):[]⟩←⟨n↦3,i↦1,13,12,(7,s1,13,s2):(3):[]⟩Loop1←⟨n↦3,i↦1,11,13,(7,s1,13,s2):(3):[]⟩IfFalse2←⟨n↦3,i↦1,10,11,_(8,11):(7,s1,13,s2):(3):[]⟩←⟨n↦3,i↦1,8,10,_(8,11):(7,s1,13,s2):(3):[]⟩IfFalse1←⟨n↦3,i↦1,7,8,(7,s1,13,s2):(3):[]⟩←⟨n↦3,i↦1,6,7,(3):[]⟩←⟨n↦3,5,6,(3):[]⟩←⟨n↦3,2,3,[]⟩←⟨ϵ,1,2,[]⟩ array[]rl& \n 6,i 3,total 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,03,4,[\>] \\ _ Return1& \n 6,i 3,total 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,014,15, call(3)\!:\![\>] \\ _ AssVar& \n 3,i 3,total 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,013,14, call(3)\!:\![\>] \\ _ LoopBase& \n 3,i 3,total 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,011,13, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfTrue2& \n 3,i 3,total 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,09,11, if\_true(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ AssVar& \n 3,i 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,08,9, if\_true(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfTrue1& \n 3,i 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,07,8, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop2& \n 3,i 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,012,7, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ AssVar& \n 3,i 2\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,013,12, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop1& \n 3,i 2\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,011,13, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse2& \n 3,i 2\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,010,11, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Skip& \n 3,i 2\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,08,10, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse1& \n 3,i 2\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,07,8, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop2& \n 3,i 2\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,012,7, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ AssVar& \n 3,i 1\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,013,12, loop2(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Loop1& \n 3,i 1\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,011,13, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse2& \n 3,i 1\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,010,11, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ Skip& \n 3,i 1\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,08,10, if\_false(8,11)\!:\! loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ IfFalse1& \n 3,i 1\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,07,8, loop1(7,s_1,13,s_2)\!:\! call(3)\!:\![\>] \\ _ LoopMain& \n 3,i 1\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,06,7, call(3)\!:\![\>] \\ _ AssVar& \n 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,05,6, call(3)\!:\![\>] \\ _ Call& \n 3\, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,02,3,[\>] \\ _ AssVar& ε, [rgb]1,0,0 [named]pgfstrokecolorrgb1,0,01,2,[\>] \\ array Figure 18: Backward derivation with the reversible semantics In order to prove the loop lemma below, stating that each forward step can be undone by a backward step and vice versa, we need to restrict our attention to reachable configurations. Definition 4(reachable configuration) A configuration ⟨σ,ℓ1′,ℓ2′,π⟩ σ, _1, _2,π is reachable if it can be obtained by applying the rules of the semantics starting from an initial configuration, namely ⟨ϵ,ℓ1,ℓ2,[]⟩(⇀∪↽)∗⟨σ,ℓ1′,ℓ2′,π⟩ ε, _1, _2,[\>] ( ∪ )^* σ, _1, _2,π for some initial configuration ⟨ϵ,ℓ1,ℓ2,[]⟩ ε, _1, _2,[\>] . This rules out, e.g., the case of configurations ⟨σ,ℓ,ℓ′,π⟩ σ, , ,π where ℓ and ℓ′ are not the two ends of an edge of the CFG. Lemma 5(loop lemma) Let ⟨σ,ℓ1,ℓ2,π⟩ σ, _1, _2,π be a reachable configuration. Then, ⟨σ,ℓ1,ℓ2,π⟩⇀⟨σ′,ℓ1′,ℓ2′,π′⟩ σ, _1, _2,π σ , _1, _2,π iff ⟨σ′,ℓ1′,ℓ2′,π′⟩↽⟨σ,ℓ1,ℓ2,π⟩ σ , _1, _2,π σ, _1, _2,π . Proof We prove the claim by a case distinction on the applied rule: (AssVar and AssArr) In both cases, the forward rule performs the inverse function of the backward rule, and vice versa. In the case of AssVar, we observe that if σ(x)=v0σ(x)=v_0 and it becomes v1=⟦⊕⟧(σ(x),v)v_1= (σ(x),v) after the forward step, where σ⊢e⇓vσ e v, yielding the store σ′=σ[x↦v1]σ =σ[x v_1], it is straightforward to see that updating variable x in σ′σ with ℐop⟦⊕⟧(σ′(x),v)I_op (σ (x),v), as the backward rule does, will restore the original value v0v_0 of x and store σ since σ′⊢e⇓vσ e v too (because Janus requires x not to occur in e). Moreover, ℓ′⟶ℓ′ iff ℓ′⟶-1ℓ′ -1 since this case involves an assignment, so there exists only a single outgoing edge in the CFG.555Note that the only statements whose associated nodes in the CFG may have two incoming or two outgoing edges are the conditions (tests or assertions) of a conditional or a loop. All other nodes always have a single incoming and outgoing edge. The case of rule AssArr is analogous. (Call and Return1Return1) Consider the configuration ⟨σ,ℓ,ℓ′,π⟩ σ, , ,π . Then, to apply a forward step with rule → Call we must have (ℓ′)=()block( )=( call~id), with ℓ⟶ℓ′ in the CFG. Hence, after the forward step, the control becomes ℓs,ℓ′ _s, , with (ℓs)=block( _s)= start (i.e., (Γ())entry( (id))) and ℓs⟶ℓ′ _s in the CFG. Moreover, the rule also pushes an element of the form (ℓ′) call( ) onto the stack. The backward step with rule ← Call performs exactly the inverse actions: checks that (ℓs)=block( _s)= start and, then, recovers the control where ℓ′ points to the original call and ℓ to its previous statement, also removing the top element of the stack. The case for rules Return1→ Return1 and Return1← Return1 is similar. Now, the forward rule triggers when the next statement is stop. In this case, removes the element call from the stack and recovers as control of the configuration the label of the original call and that of the next statement. Conversely, the backward rule triggers when when the last statement points to a call, and then pushes a new call element onto the stack and recovers the labels of the last two statements of the procedure called. (UnCall and Return2Return2) The case for these rules is perfectly analogous to the previous one. (Skip) This case is trivial. (IfTrue1IfTrue1 and IfTrue2IfTrue2) As for IfTrue1IfTrue1, the forward rule is triggered when the label of the next statement to be executed, ℓ1 _1, points to the test of a conditional of the form ([e1]ℓ1s1s2[e2]ℓ2)( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2). Then, if the condition e1e_1 evaluates to truetrue, it updates the control to ℓ1,ℓ1′ _1, _1, where ℓ1′=(s1) _1=entry(s_1). Additionally, it pushes an element of the form _(ℓ1,ℓ2) if\_true( _1, _2) onto the stack. Conversely, the backward rule considers a configuration in which the label of the last executed statement, ℓ1 _1, is the test of a conditional (the same one appearing in the _(ℓ1,ℓ2) if\_true( _1, _2) element at the top of the stack); if it evaluates to truetrue, the rule backtracks to the previous statement and pops the _ if\_true element from the stack, thereby restoring the original configuration. Regarding IfTrue2IfTrue2, the forward rule is triggered when the label of the next statement to be executed, ℓ2 _2, points to the assertion of a conditional ([e1]ℓ1s1s2[e2]ℓ2)( if~[e_1] _1~ then~s_1~ else~s_2~ fi~[e_2] _2) and an element of the form _(ℓ1,ℓ2) if\_true( _1, _2) is at the top of the stack. In this case, it pops the element from the stack and updates the control to advance to the next statement. Conversely, the backward rule considers a configuration in which the label of the last executed statement, ℓ2 _2, is the assertion of a conditional (verified via the auxiliary function ctx); it then backtracks to the previous statement, (s1)exit(s_1), and pushes the element _(ℓ1,ℓ2) if\_true( _1, _2) back onto the stack, thereby restoring the original configuration. (IfFalse1IfFalse1 and IfFalse2IfFalse2) The case for these rules is perfectly analogous to the previous one. (LoopMain and LoopBase) Regarding LoopMain, the forward rule is triggered when the label of the next statement to be executed, ℓ1 _1, points to the assertion e1e_1 of a loop of the form ([e1]ℓ1s1s2[e2]ℓ2)( from~[e_1] _1~ do~s_1~ loop~s_2~ until~[e_2] _2). In this case, the derived configuration updates the label of the next statement to point to (s1)entry(s_1) and pushes the element (ℓ1,s1,ℓ2,s2) loop1( _1,s_1, _2,s_2) onto the stack. Conversely, the backward rule proceeds inversely when the element at the top of the stack has the form (ℓ1,s1,ℓ2,s2) loop1( _1,s_1, _2,s_2), the label of the last executed statement is ℓ1 _1 (pointing to the loop assertion e1e_1), and, furthermore, it evaluates to true. In this case, the backward rule pops the loop1 element from the stack and updates the control to include the label ℓ of the statement preceding the loop, i.e., ℓ1⟶-1ℓ _1 -1 with ℓ≠(s2) (s_2). Regarding LoopBase, the situation is similar to the previous case but now focus on the loop test e2e_2. While the forward rule pops the element loop1 from the stack and updates the control to the statement following the loop when e2e_2 evaluates to true, the backward rule pushes the loop1 element back and updates the control such that the last executed statement is (s1)exit(s_1), the statement executed immediately before the evaluation of e1e_1. (Loop1Loop1 and Loop2Loop2) These cases are straightforward. ∎ 5 Related Work, Conclusion and Future Work We proposed a small-step semantics for Janus based on a notion of program counter and established its equivalence to a classical small-step semantics based on a notion of stack. They are also equivalent to Janus semantics from the literature [20, 21, 23, 9]. The Janus literature also covers extensions of Janus with other constructs, such as local variables [20, 21] and stacks [20, 21]. As immediate next step, we will extend our approach to cover such constructs as well. We also plan to apply our approach to define small-step semantics to other pure reversible languages in the literature. These include object-oriented languages such as ROOPL [7, 17] and Joule [15], and functional languages such as RFun [22] and CoreFun [8], which are all equipped with big-step semantics. The only small-step reversible semantics we are aware of are for domain-specific languages for specifying assembly sequences in industrial robots [18, 16]. However, their semantics is quite different from the one of Janus or functional or object-oriented reversible languages, since it involves the position and actions of the robot in the real world. Hence the relation with our work is quite limited. As mentioned above, the literature has few semantics of high-level languages based on a program counter. A notable exception is Gurevich and Huggins’ semantics of C [6] based on an Abstract State Machine (see also [5]). A similar pattern is found in some intermediate representations like the Static Single Assignment (SSA), which rely on explicit control-flow graphs—effectively reintroducing a program counter—to facilitate data flow analysis [3] A promising area for future exploration is the integration of concurrency support into Janus. By enabling the creation of processes and enabling them to exchange messages, such an extension could allow one to write concurrent reversible programs. The definition of the reversible small-step semantics provided in this paper is a relevant first step in this direction. References [1] Aman, B., Ciobanu, G., Glück, R., Kaarsgaard, R., Kari, J., Kutrib, M., Lanese, I., Mezzina, C.A., Mikulski, L., Nagarajan, R., Phillips, I.C.C., Pinna, G.M., Prigioniero, L., Ulidowski, I., Vidal, G.: Foundations of reversible computation. In: Ulidowski, I., Lanese, I., Schultz, U.P., Ferreira, C. (eds.) Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405, Lecture Notes in Computer Science, vol. 12070, p. 1–40. Springer (2020). https://doi.org/10.1007/978-3-030-47361-7_1 [2] Bennett, C.H.: Logical reversibility of computation. IBM Journal of Research and Development 17(6), 525–532 (1973) [3] Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991). https://doi.org/10.1145/115372.115320 [4] Danos, V., Krivine, J.: Reversible communicating systems. In: International Conference on Concurrency Theory. p. 292–307. Springer (2004) [5] Dömer, R., Gerstlauer, A., Müller, W.: The formal execution semantics of specc. In: Aboulhamid, E.M., Nakamura, Y. (eds.) Proceedings of the 15th International Symposium on System Synthesis (ISSS 2002). p. 150–155. ACM / IEEE Computer Society (2002). https://doi.org/10.1109/ISSS.2002.1227168 [6] Gurevich, Y., Huggins, J.K.: The semantics of the C programming language. In: Börger, E., Jäger, G., Büning, H.K., Martini, S., Richter, M.M. (eds.) Computer Science Logic, 6th Workshop, CSL ’92, Selected Papers. Lecture Notes in Computer Science, vol. 702, p. 274–308. Springer (1992). https://doi.org/10.1007/3-540-56992-8_17 [7] Haulund, T.: Design and implementation of a reversible object-oriented programming language (2017) [8] Jacobsen, P.A.H., Kaarsgaard, R., Thomsen, M.K.: Corefun: a typed functional reversible core language. In: International Conference on Reversible Computation. p. 304–321. Springer (2018) [9] Lami, P., Lanese, I., Stefani, J.: A small-step semantics for janus. In: Mogensen, T.Æ., Mikulski, L. (eds.) Reversible Computation - 16th International Conference, RC 2024, Toruń, Poland, July 4-5, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14680, p. 105–123. Springer (2024). https://doi.org/10.1007/978-3-031-62076-8_8 [10] Landauer, R.: Irreversibility and heat generation in the computing process. IBM Journal of Research and Development 5(3), 183–191 (1961). https://doi.org/10.1147/rd.53.0183 [11] Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. J. Log. Algebraic Methods Program. 100, 71–97 (2018). https://doi.org/10.1016/J.JLAMP.2018.06.004, https://doi.org/10.1016/j.jlamp.2018.06.004 [12] Lutz, C., Derby, H.: Janus: a time-reversible language. Letter to R. Landauer 2 (1986) [13] Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1-2), 70–96 (2007) [14] Sansom, P.M., Jones, S.L.P.: Formally based profiling for higher-order functional languages. ACM Trans. Program. Lang. Syst. 19(2), 334–385 (1997). https://doi.org/10.1145/244795.244802 [15] Schultz, U.P.: Reversible object-oriented programming with region-based memory management. In: Reversible Computation. p. 322–328. Springer (2018) [16] Schultz, U.P.: Reversible control of robots. Reversible Computation: Extending Horizons of Computing: Selected Results of the COST Action IC1405 12 p. 177–186 (2020) [17] Schultz, U.P., Axelsen, H.B.: Elements of a reversible object-oriented language. In: RC 2016. p. 153–159. Springer (2016) [18] Schultz, U.P., et al.: Towards a domain-specific language for reversible assembly sequences. In: Proceedings of the International Conference on Robotics (2015) [19] Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231–264 (1997). https://doi.org/10.1017/S0956796897002712 [20] Yokoyama, T.: Reversible computation and reversible programming languages. Electronic Notes in Theoretical Computer Science 253(6), 71–81 (2010). https://doi.org/https://doi.org/10.1016/j.entcs.2010.02.007, https://w.sciencedirect.com/science/article/pii/S1571066110000204 [21] Yokoyama, T., Axelsen, H.B., Glück, R.: Principles of a reversible programming language. In: Proceedings of the 5th Conference on Computing Frontiers. p. 43–54. CF ’08, ASCM (2008). https://doi.org/10.1145/1366230.1366239, https://doi.org/10.1145/1366230.1366239 [22] Yokoyama, T., Axelsen, H.B., Glück, R.: Towards a reversible functional language. In: International Conference on Compiler Construction. p. 15–29. Springer (2011) [23] Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: PEPM. p. 144–153. ACM Press (2007)