S ¸tefan Ciobâcȃ

Dorel Lucanu

Vlad Rusu

Grigore Roşu

A Language-Independent Proof System for Mutual Program Equivalence

Keywords: = Var | Int | ExpI + ExpI Stmt ::= Var := ExpI | skip | Stmt ; Stmt | if ExpI then Stmt else Stmt | while ExpI do Stmt Code ::= ExpI | Stmt CfgI ::= Code, Map{Var, Int} ExpF ::= Var | Val | ExpF + ExpF | ExpF ExpF Int | λ Var . ExpF CfgF ::= ExpF

Two programs are mutually equivalent if they both diverge or they end up in similar states. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a statesimilarity relation. The proof system is sound: if it terminates then it establishes the mutual equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence.

Introduction

Two terminating programs are equivalent if the final states that they reach are similar. Nontermination can be incorporated in equivalence in several ways. In this article, we explore mutual equivalence, an equivalence relation that is also known in the literature as full equivalence [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF]. Two programs are said to be mutually equivalent iff they either both diverge or they both terminate and then the final states that they reach are similar. Mutual equivalence is thus an adequate notion of equivalence for programs written in deterministic sequential languages and is useful, e.g., in compiler verification.

In this paper we formalize the notion of mutual equivalence and propose a logic with a deductive system for stating and proving mutual equivalence of two programs that are written in two possibly different different languages. The deductive system is language-independent, in the sense that it is parametric in the semantics of the two-languages. We prove that the proposed system is sound: when it succeeds it proves the mutual equivalence of the programs given to it as input. The key idea is to use the proof system to build a relation on configurations that is closed under the transition relations given by the corresponding operational semantics. This involves constructing a single language that is capable of executing pairs of programs written in the two languages. The challenge is how to achieve that generically, where the two languages are given by their formal semantics, without relying on the specifics of any particular language. The aggregated language must be capable of independently "executing" pairs of programs in the original languages. Once the aggregated language constructed, the most import rule in our proof system for mutual equivalence is the Circularity rule, which incrementally postulates synchronization points in the two programs. We illustrate the proof system on two programs (Fig. 6 on page 14) that both compute the Collatz sequence, but in different ways: one is written in an imperative language and the other one in a functional language. We prove with our system that they are mutually equivalent without, of course, knowing whether they terminate.

In Section 2 we introduce the preliminaries needed in the rest of the paper. This includes many-sorted first-order signatures, their models, and the amalgamation theorem that relates the models of pushouts of two first-order signatures with the models of the individual signatures. Section 3 presents matching logic, a specialization of many-sorted first-order logic, and shows how it can be used to give operational semantics to programming languages. Section 4 then shows how to aggregate matching logic semantics, a core operation for the mutual equivalence of programs from possibly distinct languages. Section 5 shows how our formalism can be used to specify equivalent programs and Section 6 presents our proof system for mutual equivalence and applies it to two programs computing the Collatz sequence. Section 7 discusses related work and concludes. Proofs not included due to space constraints can be found in the technical report [START_REF] Ciobaca | A language independent proof system for mutual program equivalence[END_REF].

Preliminaries

In this section, we recall notions and notations that used throughout the paper. We present the syntax and semantics of many-sorted first-order logic, which is used to define matching logic later in the paper. We then state the amalgamation theorem for many-sorted first-order logic, a known result that allows us to construct a model for the pushout construction of two first-order signatures, from the the models of the two signatures, even when the two signature share function symbols. We use the amalgamation result later in the article in order to construct the aggregated semantics of two languages from their individual semantics.

Many-sorted First Order Logic

Let S be a set of sorts, Σ an S-sorted algebraic signature (i.e., an indexed set Σ = ∪ w∈S * ,s∈S Σ w,s , where Σ w,s is the set of function symbols of arity w with a result of sort s) and Π an indexed set Π = ∪ w∈S * Π w of predicate symbols. Then Φ = (S, Σ, Π) is called a many-sorted FOL signature. We write x ∈ Φ instead of x ∈ S ∪ Σ ∪ Π. By T Σ,s (Var ) we denote the set of terms of sort s built over the variables Var with function symbols in Σ. We sometimes omit Σ if it is clear from the context and we write T s (Var ) instead of T Σ,s (V ar). The difference between the operators + , * , etc. and their correspondants + Int , * Int, etc. is that the former are the syntactic language constructs for addition, multiplication, etc. (i.e. they take language expressions as arguments), while the later are the actual function symbols for denoting integer addition, multiplication, etc. (they take integers as arguments).

Σ I = { + , * , -, + Int , -Int , * Int , := , skip, ; , if then else , while do , , }in IMP and Σ F = { + , * , -, + Int , -Int , * Int , , letrec = in , if then else , µ . , λ . , } in FUN.
The function symbols above are written using Maude-like notation, where the underscore ( ) denotes the position of an argument. Althought not written explicitly above, the signatures also include the one-argument injections needed to inject sorts like Int and Var into ExpI. Definition 2. Let Φ = (S, Σ, Π) and Φ ′ = (S ′ , Σ ′ , Π ′ ) be two many-sorted FOL signatures and let h be a function from S ∪ Σ ∪ Π to S ′ ∪ Σ ′ ∪ Π ′ . The function h is a morphism between Φ and Φ ′ if it preserves sort compatibility:

1. h(S) ⊆ S ′ , 2. if f ∈ Σ s1...sn,s then h(f ) ∈ Σ ′ h(s1
(SL, ΣL, ΠL) (S ′ , Σ ′ , Π ′ ) h R h L h ′ L h ′ R Fig. 2.
Push-out diagram assumed throughout the paper.

Definition 3. Let h be a morphism from Φ = (S, Σ, Π) to Φ ′ = (S ′ , Σ ′ , Π ′ ) and T ′ be a model of Φ ′ = (S ′ , Σ ′ , Π ′ ). We define T ′ ↾ h (the reduct of T ′ through h) to be the model of Φ such that:

1. s T ′ ↾ h = h(s) T ′ for all s ∈ S. 2. f T ′ ↾ h (e 1 , . . . , e n ) = h(f ) T ′ (

The Amalgamation Theorem

Theorem 1 (Pushout). Let Φ R , Φ L and Φ 0 be three FOL signatures, h R a morphism from Φ 0 to Φ R and h L a morphism from Φ 0 to Φ L . There exists a tuple

(h ′ L , Φ ′ , h ′ R ), called the pushout of Φ L h L ←-Φ 0 h R -→ Φ R , where h ′ L is a morphism from Φ L to Φ ′ and h ′ R a morphism from Φ R to Φ ′ such that the following conditions hold: 1. (commutativity) h ′ L (h L (x)) = h ′ R (h R (x)
) for all x ∈ Φ 0 and 2. (minimality) if there exist Φ ′′ and morphisms h ′′ L (from

Φ L to Φ ′′ ) and h ′′ R (from Φ R to Φ ′′ ) such that h ′′ L (h L (x)) = h ′′ R (h R (x)
) for all x ∈ Φ 0 then there exists a morphism h from Φ ′ to Φ ′′ . Furthermore, the pushout is unique (up to renaming).

See, e.g., [START_REF] Haxthausen | Pushouts of order-sorted algebraic specifications[END_REF], for a proof. The push-out is summarised in Figure 2, which is used throughout the paper. Proposition 1. In the push-out in Figure 2

, if x ′ ∈ Φ ′ = (S ′ , Σ ′ , Π ′ ) such that there exist x L ∈ Φ L and x R ∈ Φ R with h ′ R (x R ) = x ′ = h ′ L (x L ), then there exists x ∈ Φ such that h L (x) = x L and h R (x) = x R .
See, e.g. [START_REF] Haxthausen | Pushouts of order-sorted algebraic specifications[END_REF], for the proof.

Theorem 2. If T R , T L and T 0 are models of Φ R = (S R , Σ R , Π R ), Φ L = (S L , Σ L , Π L ) and respectively Φ 0 = (S 0 , Σ 0 , Π 0 ) such that T R ↾ h R = T L ↾ h L = T 0 , there exists a unique model T ′ of Φ ′ such that T ′ ↾ h ′ L = T L and T ′ ↾ h ′ R = T R .
The proof can be found in our accompanying technical report ([3]).

Matching Logic Syntax and Semantics

We introduce notation used throughout the paper and discuss the recently introduced matching logic [START_REF] Roşu | Checking reachability using matching logic[END_REF][START_REF] Roşu | Matching logic: An alternative to Hoare/Floyd logic[END_REF], a language-parametric logic for reasoning about program configurations, and its use in language semantics. Matching logic extends FOL with basic patterns, which are open terms (i.e., terms with variables) that can be used as basic formulae in the logic.

We first introduce matching logic signatures (ML signatures), which extend FOL signatures by fixing a sort of program configurations. Note that x and y (written in teletype font) are program variables (therefore constant symbols in Σ I , while x and y (written in italics) are variables. Intuitively, and as we will see later on, the formula above denotes IMP configurations that have terminated (only the instruction skip is left in the code to execute) and in which the program variable x is mapped to an integer strictly greater than 10 and the program variable y is mapped to an integer y that is unconstrained. Models of ML signatures are simply FOL models: Definition 6. We say that T is a matching logic model of (Cfg, S, Σ, Π) if T is a first order model of (S, Σ, Π). In what follows, we fix a model T of (Cfg, S, Σ, Π). Elements of Cfg T are called concrete configurations. We represent concrete configurations by γ, γ ′ , γ 1 and variations thereof. Valuations ρ : Var → T of matching logic are simply valuations of the corresponding first order logic. The satisfaction relation of matching logic is defined between pairs (γ, ρ) of configurations and valuations and ML formulae ϕ as follows:

Definition 7. The matching logic satisfaction relation |= (written as (γ, ρ) |= ϕ and read as (γ, ρ) is a model of ϕ) is defined inductively as follows: Example 7. We continue Example 5, where we defined ϕ = skip, x → x, y → y ∧ x > Int 10. Let ρ be a valuation where ρ(x) = 12 and ρ(y) = 3. Let γ = skip, x → 12, y → 3 . We have that (γ, ρ) |= ϕ. Considering γ ′ = skip, x → 3, y → 13 and a valuation ρ ′ with ρ ′ (x) = 3 and ρ ′ (y) = 13, we have that (γ ′ , ρ ′ ) |= ϕ because the condition x > Int 10 is not satisfied. Furthermore, if γ ′′ = skip, x → 3, y → 13 and ρ ′′ is a valuation with ρ ′′ (x) = 7 and ρ ′′ (y) = 13, we have that (γ ′′ , ρ ′′ ) |= ϕ because γ ′′ will not match against the basic pattern skip, x → x, y → y with the valuation ρ ′′ (the valuation ρ ′′ assigns 7 to the variable x, while x should be 3 due to matching). Definition 8. A matching logic semantic domain for a language is a tuple (Cfg, S , Σ , Π , T ), where (Cfg, S , Σ , Π ) is a matching logic signature and T a matching logic model of (Cfg, S , Σ , Π ). Note that the matching logic semantic domain fixes the abstract syntax of the language (programs are first-order terms of sort Cfg) and the configuration space (given by the model T ). However, the matching logic semantic domain does not say anything about the dynamic behavior of configurations. This is the role of the matching logic semantics. A matching logic semantics for a programming language extends the matching logic semantic domain by the addition of several reachability rules: Definition 9. A reachability rule is a pair ϕ ⇒ ϕ ′ of matching logic formulae. Example 9. Let us consider the rule skip;s, m ⇒ s, m . In the rule above, s is a variable of sort Stmt and m is a variable of sort Map{Var,Int}. It describes what happens in the IMP language when the code to execute is a sequence composed of the skip instruction and another statement s. The skip instruction is simply dissolved and the sequence is simply replaced by s. The environment (captured in the variable m) is not changed during this step. Definition 10. A matching logic semantics for a language is a tuple (Cfg, Σ , Π , T , A, T ), where (Cfg, Σ , Π , T ) is matching logic semantic domain, A a set of reachability rules and T is the transition system generated by A on T , that is,

1. (γ, ρ) |= ¬ϕ ′ if it is not true that (γ, ρ) |= ϕ ′ 2. (γ, ρ) |= ϕ 1 ∧ ϕ 2 if (γ, ρ) |= ϕ 1 and (γ, ρ) |= ϕ 2 3. (γ, ρ) |= ∃x.ϕ ′ ,
T ⊆ T Cfg × T Cfg with γ T γ ′ iff there exist ϕ ⇒ ϕ ′ ∈ A and ρ such that (γ, ρ) |= ϕ and (γ ′ , ρ) |= ϕ ′ . x, env ⇒ env(x), env ∈ AI i1 op i2, env ⇒ i1 op Int i2, env ∈ AI x := i, env ⇒ skip, env[x → i] ∈ AI skip;s, env ⇒ s, env ∈ AI if i then s1 else s2, env ∧ i = 0 ⇒ s1, env ∈ AI if 0 then s1 else s2, env ⇒ s2, env ∈ AI while e do s, env ⇒ if e then s while e do s else skip, env ∈ AI C[code], env ⇒ C[code ′ ], env ′ ∈ AI if code, env ⇒ code ′ , env ′ ∈ AI
where

C ::= | C op e | i op C | if C then s1 else s2 | v := C | C s Fig. 3.
Matching logic semantics of IMP as a set AI of reachability rules (schemata). op ranges over the binary function symbols and op Int is their denotation in TI . As discussed in [START_REF] Roşu | Checking reachability using matching logic[END_REF], conventional operational semantics of programming languages can be regarded as matching logic semantics: Σ includes the abstract syntax of the language as well as the syntax of the various operations in the needed mathematical domains; A is the (possibly infinite) set of operational semantics rules of the language; T is the model of configurations of the language merged together with the needed mathematical domains, and the relation T is precisely the transition relation defined by the operational semantics. Fig. 3 and Fig. 4 show matching logic semantics of the IMP and FUN languages, respectively, obtained by mechanically representing conventional operational semantics of these languages based on reduction semantics with evaluation contexts into matching logic. The only observable difference between the original semantics of these languages and their matching logic semantics is that the side conditions have been conjuncted with the left-hand-side patterns in the positive case of the conditionals. Note that A IMP and A FUN are infinite, as the rules in Figs. 3 and4 are schemata in meta-variable C (the evaluation context).

i1op i2 ⇒ i1op Int i2 ∈ AF if i then e1 else e2 ∧ i = 0 ⇒ e1 ∈ AF if 0 then e1 else e2 ⇒ e2 ∈ AF letrec f x = e in e ′ ⇒ e ′ [f → (µf.λx.e)] ∈ AF (λx.e) v ⇒ e[x → v] ∈ AF µx.e ⇒ e[x → (µx.e)] ∈ AF C[c] ⇒ C[c ′ ] ∈ AF if c ⇒ c ′ ∈ AF where C ::= | C op e | if C then e1 else e2 | C e | v C
Given a matching logic language semantics given as a set of reachability rules, it is possible to derive other reachability rules that "hold" as consequences of the initial set of rules. This is captured by the following definition.

Definition 11. Given a matching logic semantics (Cfg, Σ , Π , T , A, T ), we say that ϕ → * ϕ ′ (resp. ϕ → + ϕ ′ ) is a semantic consequence of A, and we write

A |= ϕ → * ϕ ′ (resp. A |= ϕ → + ϕ ′ ), if for any γ, γ ′ ∈ Cfg T , for any valuation ρ such that (γ, ρ) |= ϕ and (γ, ρ) |= ϕ ′ , we have that γ → * T γ ′ (resp. γ → + T γ ′ ).
Example 11. In the set of rateability rules A I for the IMP languages (given in Figure 3), if we let SUM ≡ while i <= n do (s := s + i; i := i + 1) be the program that computes the sum of all numbers between i and n, then we have

A I |= SUM, n → n, i → 0; s → 0 ∧ n ≥ Int 0 → + skip, [n → n; i → n + 1; s → n(n+ Int 1)/ Int 2] .
Intuitively the above reachability rule that is a semantic consequence of the IMP set of leachability rules claims that the program SUM indeed computes the sum of the numbers 1 upto n.

We have previously shown (see [START_REF] Roşu | Checking reachability using matching logic[END_REF] and subsequent papers) that there exists a sound and (relatively) complete proof system for establishing semantic consequences such as the above. In this article, we assume that such a system is available as an oracle to our proof system for program equivalence.

Aggregation of Matching Logic Semantic Domains

In this section we show how, given the matching logic semantic domains for two languages, we can construct a matching logic semantic domain for the aggregation of the two languages. The aggregation of two languages is a new language in which programs consists of pairs of programs in the two languages. The challenge is how to construct the domain such that sorts that are common in the two languages (i.e. the sort of integers) has a common interpretation in the aggregated domain. We rely on pushout construction in Section 2 (Theorem 1) and the amalgamation theorem (Theorem 2) in order to perform the aggregation as expected. This construction involves significant technical and conceptual difficulties and, to our knowledge, it has not been described before.

Let S i = (Cfg i , S i , Σ i , Π i , T i ), i ∈ {L, R} be the matching logic semantic domains of two languages, (S 0 , Σ 0 , Π 0 ) a matching logic signature, h L and h R morphisms from (S 0 , Σ 0 , Π 0 ) to (S L , Σ L , Π L ) and from (S 0 , Σ 0 , Π 0 ) to (S R , Σ R , Π R ). Let T L , T R , T 0 be models of (S L , Σ L , Π L ), (S R , Σ R , Π R ) and respectively (S 0 , Σ 0 , Π 0 ) such that

T L ↾ h L = T 0 = T R ↾ h R . Let (h ′ L , (S ′ , Σ ′ , Π ′ ), h ′ R ) be the pushout of (S L , Σ L , Π L ) h L ←-(S 0 , Σ 0 , Π 0 ) h R -→ (S R , Σ R , Π R ). By Theorem 2, there exists a unique (S ′ , Σ ′ , Π ′ )-model T ′ such that T ′ ↾ h ′ L = T L and T ′ ↾ h ′ R = T R .
We define now the aggregation of the two matching logic semantic domains. We let S = (Cfg, S , Σ , Π , T ), where

-Cfg is a new distinguished sort; -S = S ′ ∪ {Cfg} -Σ = Σ ′ ∪{ , : h L (Cfg L )×h R (Cfg R ) → Cfg, pr i : Cfg → Cfg i , i ∈ {L, R}}; -Π = Π ′ ; -T Cfg = T ′ h ′ L (CfgL) × T ′ h ′ R (CfgR) -T , (γ L , γ R ) = (γ L , γ R ), T pr L ((γ L , γ R )) = γ L , T pr R ((γ L , γ R )) = γ R . -T o = T ′ o for any other object o ∈ S ∪ Σ ∪ Π.
We define a new matching logic semantic domain

S ′ i = (h ′ i (Cfg i ), S ′ , Σ ′ , Π ′ , T ′ ) for each i ∈ {L, R}.
The matching logic semantic domain S ′ i is the embedding of S i into S. The main difference between S i and S ′ i is that S ′ i works in a slightly larger algebra that contains symbols from the other language. However, since the matching logic semantics rules do no mention these additional symbols, executions of programs in S i coincide with executions of programs in S ′ i . In the rest of this section we formally show that this is indeed the case and we establish relations between executions of the aggregate language and the individual languages. Remark 1. Let i ∈ {L, R}. For every valuation ρ : Var → T i , we define h(ρ) to be the valuation h(ρ) : h(Var ) → T i , with h(ρ)(x) = ρ(x) for all x ∈ Var .

We first show that applying the morphism h ′ i on both the matching logic formula and valuation does not change the matching logic satisfaction relation. Proposition 2. For any pattern π and any valuation ρ, ρ(π) = h(ρ)(h(π)).

Let γ i ∈ h ′ i (Cfg i )
T ′ be a configuration and ϕ i a matching logic formula over (S i , Σ i , Π i ) and the set of variables Var , for each i ∈ {L, R}. Note that the same set of variables Var is used for both semantic domains S L and S R . Lemma 1. For all valuations ρ :

Var → T i , (γ i , h ′ i (ρ)) |= h ′ i (ϕ i ) iff (γ i , ρ) |= ϕ i (where i ∈ {L, R}).
The above lemma allow us to conclude that executions in S i and S ′ i coincide:

Proposition 3. If γ i , γ ′ i ∈ h ′ i (Cfg i ) T ′ , then γ i S ′ i γ ′ i iff γ i Si γ ′ i .
We now establish the connection between matching logic formulae over the aggregate language and the two individual languages. We first define the leftand right-projection of matching logic formulae. Definition 12. Let ϕ be a (S, Σ, Π)-matching logic formula. For i ∈ {L, R}, we define the (S ′ i , Σ ′ i , Π ′ i )-matching logic formula pr i (ϕ) (for i = L, the leftprojection and for i = R, the right-projection) to be ϕ where every term t L , t R of sort Cfg is replaced by t i .

We now distinguish a class of matching logic formulae which behave well with respect to the aggregate semantics. Definition 13. A (S, Σ, Π)-matching logic formula is pure if no term of sort Cfg in the formula appears under a negation.

For such pure formulae, we establish the following proposition, which connects satisfaction of matching logic formulae over the aggregate language with satisfaction of matching logic formulae over the individuals languages: Proposition 4. Let (γ L , γ R ) ∈ Cfg T be a configuration. Let ϕ be a pure matching logic formula with no variables of sort Cfg. For any valuation ρ : Var → T , we have that

((γ L , γ R ), ρ) |= S ϕ iff (γ L , ρ) |= S ′ L pr L (ϕ) and (γ R , ρ) |= S ′ R pr R (ϕ).
Note that all of the matching logic formulae that we have used so far are pure. In fact, in order to define programming language semantics, which have been shown to be written as sets of rewrite rules of the form a ⇒ b if c [START_REF] Roşu | Checking reachability using matching logic[END_REF], only pure matching logic formulae are needed. In the rest of this article, we will assume that we only deal with such formulae.

Specifying Equivalent Programs

Aggregate matching logic patterns can be used to specify pairs of configurations of the two involved languages: Definition 14. The denotation of an aggregated matching logic pattern ϕ, written ϕ , is the set of all pairs of configurations that satisfy it:

ϕ = {( γ L , γ R | there exists a valuation ρ such that ( γ L , γ R , ρ) |= ϕ}.
This notation extends to sets E of patterns, written E , as expected:

E = ∪ ϕ∈E ϕ .
Example 12. The following set

E = {∃i. skip, (x → i, ) , j ∧ i = Int j} (1)
containing one matching logic formula, captures in its denotation all pairs of IMP and respectively FUN configurations that have terminated (since there is no more code to execute) and where the IMP variable x holds the same integer as the result of the FUN program. Note that in the above pattern, is an anonymous variable meant to capture all of the variable bindings other than x. Suppose we have an IMP program that computes its result in a variable x and suppose we want to show it computes the same integer result as a FUN program. Then the denotation E of set E above holds exactly the set of pairs of terminal configurations in which the two programs should end in order for them to compute the same result.

When trying to prove that two programs compute the same result, it is tempting to say that the two programs should reach the same configuration at the end. However, this is not feasible since the configuration might contain additional information (such as temporary variables) that was used in the computation but is not part of the result. When testing if the final configurations are the same in the two programs, it is important to ignore such additional information. In the example above, only the variable x is inspected (the values of all other variables are ignored) when comparing final configurations. Another aspect is that, when working in a general setting where we are comparing programs from two arbitrary programming languages, the configurations of the two languages might be significantly different. This is the case above, with the configuration for IMP holding code and an environment and the configuration for FUN holding only (extended) lambda expressions. Therefore, in general, to show that two programs end up with the same result there is a need to design such a set E of "base" pairs which are known to be equivalent.

Proving Mutual Program Equivalence

Here we provide a language-parametric foundation for showing equivalence of programs written in possibly different languages. Like in the previous section, we generically assume that the two languages are given as matching logic semantics

S L = (Cfg L , Σ L , Π L , A L ,T L , T L ) and S R = (Cfg R , Σ R , Π R , A R ,T R , T R ) with aggregation S = (Cfg, Σ , Π , A, T , T
), but when we discuss examples we assume them to be the semantics S IMP and S FUN of, respectively, IMP and FUN.

Two programs are then considered mutually equivalent when, for all inputs, they both diverge or they both reach a pair in the base equivalence E . This intuition is captured by the following definition: Definition 15. We write |= ϕ ⇓ ∞ E, and say that ϕ reaches E, iff for all configurations γ L , γ R and for all valuations ρ such that ( γ L , γ R , ρ) |= ϕ we have that at least one of the following conditions holds:

1. both γ L and γ R diverge (i.e. γ C → T γ 1 C → T . . . → T γ i C → T for any natural num- ber i and any C ∈ {L, R}); 2. there are configurations γ ′ L , γ ′ R with γ L * T γ ′ L , γ R * T γ ′ R and (γ ′ L , γ ′ R ) ∈ E . Example 13. Let E = {∃i. skip, (X → i, ) , i } and let ϕ 1 = ∃n. code 1 , n → n , exp 1 (n) ϕ 2 = while 1 do skip, ∅ , letrec f x = f(x + 1) in f(1) ϕ 3 = ∃n. code 3 , n → n , exp 3 (n) .
where code 1 ≡ i:=1; x:=0; while i<=n do (x:=x+i; i:=i+1) is the IMP program that computes the sum of the numbers from 1 to n, where exp 1 (n) ≡ letrec f x = if x=1 then 1 else x+f(x-1) in f(n) is the FUN program computing the same sum, and where code 3 ≡ PGM L and, resp., exp 3 (n) ≡ PGM R (n) are the IMP and FUN programs in Fig. 6 that compute the Collatz function.

We have that |= ϕ 1 ⇓ ∞ E since both programs end up in a pair from E : code 1 , n → n * T skip, x → 1+2+. . .+n and exp 1 (n) * T 1+2+. . .+n . We also have that |= ϕ 2 ⇓ ∞ E, since both configurations in ϕ 2 clearly diverge. We also have that |= ϕ 3 ⇓ ∞ E, but this is more difficult to establish. In fact, it is currently only conjectured (not proven) that the programs terminate no matter what the input value n is. But it can be proven that if one does not terminate, the other does not terminate either and therefore |= ϕ 3 ⇓ ∞ E holds independently of the Collatz conjecture. However, |= ϕ 3 ⇓ ∞ E is more difficult to show than the previous examples since it is not clear if both programs terminate or diverge. We next propose a proof system that allows us to derive such properties.

Proof System

In this section, we introduce a proof system that is able to derive sequents of the form ⊢ ϕ ⇓ ∞ E denoting mutual equivalences that are sound in the sense that ⊢ ϕ ⇓ ∞ E implies |= ϕ ⇓ ∞ E. Fig. 5 contains the 5-rule proof system for proving mutual equivalence of programs.

The first rule is Axiom. There is nothing suprizing about this rule; it simply states that if an equivalence is known to be true, then it can be derived.

The second rule is Step. It allows to take an arbitrary finite number of steps (zero, one or more steps) in each of the two programs. If by taking such steps from ϕ to ϕ ′ , we reach an equivalence ϕ ′ that is derivable, then we conclude that ϕ must also be derivable. The Step rule requires an oracle to reason about reachability in operational semantics. This oracle can be, for example, the reachability proof system in [START_REF] Roşu | Checking reachability using matching logic[END_REF], but any other valid reasoning will also work.

Axiom ϕ ∈ E ⊢ ϕ ⇓ ∞ E Step ϕ ⇒ * ϕ ′ ⊢ ϕ ′ ⇓ ∞ E ⊢ ϕ ⇓ ∞ E Conseq |= ϕ → ϕ ′ ⊢ ϕ ′ ⇓ ∞ E ⊢ ϕ ⇓ ∞ E Case Analysis ⊢ ϕ ⇓ ∞ E ⊢ ϕ ′ ⇓ ∞ E ⊢ ϕ ∨ ϕ ′ ⇓ ∞ E Circularity ⊢ ϕ ′ ⇓ ∞ E ∪ {ϕ} ϕ ⇒ + ϕ ′ ⊢ ϕ ⇓ ∞ E Fig. 5. Mutual Equivalence Proof System. We use ϕ ⇒ * ϕ ′ as syntactic sugar for AL |= pr L (ϕ) → * pr L (ϕ ′ ) and AR |= pr R (ϕ) → * pr R (ϕ ′ ) and ϕ ⇒ + ϕ ′ as syntactic sugar for AL |= pr L (ϕ) → + pr L (ϕ ′ ) and AL |= pr R (ϕ) → + pr R (ϕ ′ ).
The third rule is Conseq(uence). This rule states that if an equivalence formula ϕ implies another equivalence formula ϕ ′ (which means that ϕ ′ is more general than ϕ) and the formula ϕ ′ is derivable, then ϕ must also be derivable. The required implication might seem surprizing at first (we might expect it in reverse), but the intuition is that ϕ ′ is more general than ϕ. Therefore if we are able to prove the equivalence ϕ ′ , then ϕ must also hold. This rule is used in the example proof tree below (in Fig. 6) to rearrange a formula of the form (n > 0 ∨ n = 0) ∧ . . . into n ≥ 0 ∧ . . .. Another possible use of Conseq would be, for example, to transform a more particular case, like "n = 20", into a more general case "n is even" in order to be able to apply other rules.

The fourth case is Case Analysis. This allows to branch the proof depending on the different cases to consinder. Typically, Case Analysis is used to branch the proof when the two programs also branch. In the proof tree below (in Fig. 6), this rule is used to perform a case analysis between the case where both programs end (because of reaching the termination condition n = 0) and where the programs continue (n > 0).

The fifth rule is Circularity. This rule is used to handle repetitive program structures such as loops or recursive functions. Circularity allows to postulate that the equivalence being proven (ϕ) holds, make progress (ϕ ⇒ + ϕ ′ ) in both programs that we want to show equivalent, and then derive ϕ ′ possibly using ϕ as an axiom, i.e., ⊢ ϕ ′ ⇓ ∞ E ∪ {ϕ}. We use this rule in the proof tree below to assume that at the start of the repetitive behavior (the loop for the program on the left and the recursive call for the program on the right) the two programs are equivalent; we make progress by executing the body of the loop on the left and the body of the recursive call on the right and end up with the equivalence that we assumed to hold. The rule is sound because we require both programs to make progress. Therefore, intuitively, when ⊢ ϕ ′ ⇓ ∞ E ∪ {ϕ} is derivable, either both programs diverge because ϕ is applied as an axiom in the proof tree or the programs end up in E. As for the first rule, an oracle to reason about reachability in operational semantics is also needed here.

Theorem 3 (Soundness). For any set of aggregated matching logic patterns E and for any aggregated matching logic pattern ϕ, if the sequent ⊢ ϕ ⇓ ∞ E is derivable using the proof system given in Fig. 5 then |= ϕ ⇓ ∞ E.

In order to prove the above theorem, we need several intermediate steps that follow. In the following, we let c ∈ {L, R} denote either left or right. By c we denote the single element of the set {L, R} \ {c}.

Let E be a set of mutual matching logic formulae. Let A L and A R be a set of reachability formulae which describe the semantics of two languages: A L the "left" language and A R the "right" language. We extend the definition of |= ϕ ⇓ ∞ E to sets of mutual matching logic formulae as expected: Definition 16. If F is a set of mutual matching logic formulae, then we write

|= F ⇓ ∞ E if |= ϕ ⇓ ∞ E for all ϕ ∈ F.
The following definitions will be useful in the proof of soundness. Let G denote a set of pairs of configurations. Definition 17. We say that a pair

(γ L , γ R ) reaches G, written (γ L , γ R ) → * G, if there exist configurations γ ′ L and γ ′ R such that γ L * A L γ ′ L , γ R * A R γ ′ R and (γ ′ L , γ ′ R ) ∈ G. Definition 18.
We say that a pair (γ L , γ R ) diverges, written (γ L , γ R )↑ ∞ , if both γ L and γ R diverge (in A L and respectively A R ).

Definition 19. We say that a pair (γ L , γ R ) co-reaches G, written (γ L , γ R ) → * ,∞ G, if at least one of the following conditions holds:

1. (γ L , γ R ) diverges (i.e. (γ L , γ R )↑ ∞ ), 2. (γ L , γ R ) reaches G (i.e. (γ L , γ R ) → * G).
The following utility lemma establishes the link between models of mutual matching logic formulae and the notion of co-reachability introduced above. Its proof following trivially by unrolling the above definitions. Lemma 2. For all sets of mutual matching logic formulae E and for any mutual matching logic formula ϕ, we have that:

|= ϕ ⇓ ∞ E iff for all γ L , γ R such that (γ L , γ R ) ∈ ϕ , (γ L , γ R ) → * ,∞ E .
The next lemma is the core of our soundness proof. Lemma 3 (Circularity Principle).

Let F be a set of mutual matching formulae. If for each

(γ L , γ R ) ∈ F there exist γ ′ L , γ ′ R such that γ L + A L γ ′ L , γ R + A R γ ′ R , and (γ ′ L , γ ′ R ) → * ,∞ E ∪ F , then |= F ⇓ ∞ E.
It lies at the core of the proof for Theorem 3, which can be found in our accompanying technical report [START_REF] Ciobaca | A language independent proof system for mutual program equivalence[END_REF].

Example

We next show the proof tree for the equivalence of the two Collatz programs in Fig. 6. As we have already discussed, in order to talk about mutual equivalence, we have to establish a "base" equivalence that contains programs that are clearly equivalent. For this case study, for the "base" equivalence, we choose to equate FUN programs that terminate by returning an integer i with IMP programs that terminate with the same integer i in the variable c. The set E = {∃i. skip, (c → i, ) , i } defined in Equation 1 captures the intuition above. It says that an IMP configuration skip, (c → i, ) (describing programs that stopped (because the code cell contains skip) and that have the integer i in the c memory cell) is equivalent to a FUN configuration that contains exactly the integer i. The proof tree in Fig. 6 shows that the two programs are equivalent.

:= letrec f n = LOOPR in f(n) LOOPR := 1 + if (n != 1) then if (n % 2 != 0) then f(3 * n + 1) else f(n / 2) else 0 ϕ := ∃i, n.(n > 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) 1. ⊢ ( skip, c → i, , i ) ⇓ ∞ E Axiom 2. ⊢ ( skip, c → i, , i ) ⇓ ∞ E ∪ {ϕ} Axiom 3. ⊢ ( skip, n → n, c → i , i ) ⇓ ∞ E Conseq(1) 4. ⊢ ( skip, n → n, c → i , i ) ⇓ ∞ E ∪ {ϕ} Conseq(2) 5. ⊢ (n = 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) ⇓ ∞ E Step(3) 6. ⊢ ∃i, n.(n = 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) ⇓ ∞ E ∪ {ϕ}
Step(4)

7. ⊢ ∃i, n.(n > 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) ⇓ ∞ E ∪ {ϕ} Axiom 8. ⊢ ∃i, n.(n ≥ 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) ⇓ ∞ E ∪ {ϕ} Conseq(CA(6, 7)) 9. ⊢ ∃i, n.(n > 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) ⇓ ∞ E Circularity (8) 10. ⊢ ∃i, n.(n ≥ 0 ∧ LOOPL, n → n, c → i , i + LOOPR ) ⇓ ∞ E Conseq(CA(5, 9)) 11. ⊢ ∃i, n.(n ≥ 0 ∧ PGML, n → n , PGMR(n) ) ⇓ ∞ E
Step (10) Fig. 6. Formal proof showing that the two Collatz programs are mutually equivalent. CA stands for Case Analysis. Conseq is used in the proof tree above to show that n > 0 ∨ n = 0 implies n ≥ 0. For simplicity, letrec is not desugared into µ. To make reading easier, the existential quantifiers (∃i, n.) in each step (1 to 11) are skipped for brevity.

Discussion, Related Work and Conclusion

We have introduced mutual matching logic, a 5-rule proof system for proving mutual equivalence of programs. Mutual equivalence is a natural equivalence between programs: two programs are mutually equivalent if either they both diverge or if they eventually reach the same state. Mutual equivalence can be used, for example, to prove that compiler transformations preserve behavior. Our approach is language independent. The proof system takes as input two language semantics (in the form of reachability rules) that share certain domains such as integers and produces sequents of the form ⊢ ϕ ⇓ ∞ E whose semantics is that for any pair of programs that matches ϕ, both programs diverge or they reach a state in E. Note that in our running example (the two Collatz programs), both programs have a parameter n that is left unspecified. This shows that our approach allows parameterized programs. Although because of space limitations we do not explicitly state this, our approach can handle symbolic programs as well. For example, we can show using our proof system that in IMP extended with a for loop, the two programs: i := 1; while (i <= n) do s; i := i + 1;

for i := 1 to n do s;

are equivalent for a symbolic statement s. We specify the symbolic statement s as an additional statement in the signature of IMP and we render explicit the constraints on s in its semantics using reachability rules.This kind of symbolic programs are also considered in [START_REF] Lucanu | Program equivalence by circular reasoning[END_REF] but for a different notion of bisimulationbased program equivalence. Related Work. It was first remarked by Hoare in [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] that program equivalence might be easier than program correctness. Among the recent works on equivalence we mention [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF][START_REF] Godlin | Regression verification: proving the equivalence of similar programs[END_REF][START_REF] Chaki | Regression verification for multithreaded programs[END_REF]. The first one targets programs that include recursive procedures, the second one exploits similarities between single-threaded programs in order to prove their equivalence, and the third one extends the equivalence-verification to multi-threaded programs. They use operational semantics (of a specific language they designed, called LPL) and proof systems, and formally prove their proof system's soundness. In [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF] a classification of equivalence relations used in program-equivalence research is given, one of which is mutual equivalence (called full equivalence there). The main difference with our approach is that our proof system is language-independent, i.e., it is parametric in the semantics of the two languages in which candidate equivalent programs are written; whereas the deductive system of [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF] proves equivalence for LPL programs. On the other hand, [START_REF] Godlin | Inference rules for proving the equivalence of recursive procedures[END_REF] propose deductive systems for several kinds of equivalences, whereas we focus on mutual (a.k.a. full) equivalence only. In [START_REF] Kundu | Proving optimizations correct using parameterized program equivalence[END_REF], an implementation of a parametrized equivalence prover is presented.

A lot of work on program equivalence arise from the verification of compilation in a broad sense. One approach is full compiler verification (e.g. Com-pCert [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]), which is incomparable to our work since it produces computerchecked proofs of equivalence for a particular language, while our own work produces proofs (not computer-checked) of equivalence for any language. Another approach is the individual verification of each compilation [START_REF] Necula | Translation validation for an optimizing compiler[END_REF] (we only cite two of the most relevant recent works). Other work targets specific classes of languages: functional [START_REF] Pitts | Operational semantics and program equivalence[END_REF], microcode [START_REF] Arons | Formal verification of backward compatibility of microcode[END_REF], CLP [START_REF] Craciunescu | Proving the equivalence of CLP programs[END_REF]. In order to be less languagespecific some approaches advocate the use of intermediate languages, such as [START_REF] Lahiri | Symdiff: A languageagnostic semantic diff tool for imperative programs[END_REF], which works on the Boogie intermediate language. However, our approach is better, since our proof system works directly with the language semantics; therefore there is no need to trust the compiler from the original language to Boogie. Finally, our own related work [START_REF] Lucanu | Program equivalence by circular reasoning[END_REF] gives a proof system for another equivalence relation between programs that is based on bisimulation and an observation relation and that uses other technical mechanisms. We believe that the equivalence relation that we consider in this article in more natural for certain classes of applications such as proving compilers. Further Work. Our definition (Definition 15) of mutual equivalence is existential in the sense that two programs are equivalent when there exists execution paths in each of the programs such that the paths diverge or end in configurations that are known to be equivalent. Although for deterministic languages this cannot constitute a problem (there exists exactly one execution path for each program), for non-deterministic languages stronger equivalences might be desirable. We leave such stronger equivalences as object of further study. Another issue is completeness. Although relative completeness results have been shown for matching logic based proof systems for showing partial correctness [START_REF] Roşu | Checking reachability using matching logic[END_REF], it is less clear how a relevant relative-completeness result can be obtained for equivalence, since the problem is known to be Π 0 2 -complete. Another issue that we leave for further study is compositionality. Our goal here was just to obtain a sound and useful language independent proof system for reasoning about equivalence.

Example 1 .

 1 The signatures Φ I = (S I , Σ I , Π I ) and Φ F = (S F , Σ F , Π F ) in Figure 1 model the syntax of an imperative and a functional programming language, with sorts S I = {Int, Var, ExpI, Stmt, Code, CfgI} in IMP and sorts S F = {Var, Int, ExpF, Val, CfgF} in FUN, function symbols

Fig. 1 .

 1 Fig. 1. ΦI = (SI , ΣI , ΠI ) and ΦF = (SF , ΣF , ΠF ), the signatures of IMP and FUN, written using BNF notation and detailed in Example 1. Only the function symbols are detailed in the figure and the predicates for the two languages consist of the arithmetic comparison operators: ΠI = ΠF = {=Int, <Int, ≤Int}.The difference between the operators + , * , etc. and their correspondants + Int , * Int, etc. is that the former are the syntactic language constructs for addition, multiplication, etc. (i.e. they take language expressions as arguments), while the later are the actual function symbols for denoting integer addition, multiplication, etc. (they take integers as arguments).

Definition 1 .T

 1 We say that T = ( ) is a model of a many-sorted signature Φ = (S, Σ, Π) if: 1. s S T , the interpretation of the sort s in the model T , is a set for each s ∈ S 2. f F T , read as the interpretation of the function symbol f in the model T , is a function defined on s 1 T × . . . × s n T with values in s T , for every function symbol f ∈ Σ s1,...,sn,s . 3. p P T , read as the interpretation of the predicate symbol p in the model T , is a subset of s 1 T × . . . × s n T for every predicate symbol p ∈ Π s1,...,sn . From now on, we write • T instead of • S T , • F T and • P T when the type of the argument (sort, function symbol or predicate symbol), is clear from context. Example 2. We consider T I to be a model of Φ I = (S I , Σ I , Π I ) where the interpretation Var T I of the sort Var is the set of strings, the interpretation Int T I of the sort Int is the set of integers and the function symbols are interpreted syntactically (as terms). The predicates = Int , < Int , ≤ Int are interpreted as the respective comparison relations between integers.

  Definition 4. A matching logic signature is a tuple (Cfg, S, Σ, Π), where (S, Σ, Π) is a FOL signature and Cfg ∈ S . Example 4. Recall the first-order signature Φ I = (S I , Σ I , Π I ) in Example 1. We have that (CfgI, S I , Σ I , Π I ) is a matching logic signature. Note that ground instances of sort CfgI represent actual configurations of IMP programs. Matching logic formulae extend FOL formulae with terms of sort Cfg as atomic formulae called basic patterns: Definition 5. Given a matching logic signature (Cfg, S, Σ, Π), the following are matching logic formulae (ML formulae) over (Cfg, S, Σ, Π) and the set of sorted variables Var : ϕ ::= ¬ϕ, ϕ ∧ ϕ, ∃x.ϕ, π where π ∈ T Cfg (Var ), x ∈ Var . Example 5. Continuing Example 4, ϕ = skip, x → x, y → y ∧ x > Int 10 is a matching logic formula over the matching logic signature (CfgI, S I , Σ I , Π I ).

Example 6 .

 6 The model T defined in Example 2 is also a model of the matching logic signature (CfgI, S I , Σ I , Π I ).

  where x is of sort s, if there exists e ∈ s T such that (γ, ρ[e/x]) |= ϕ ′ (where ρ[e/x] is the valuation obtained from ρ by updating the value of x to be e). 4. (γ, ρ) |= π, where π is a basic pattern if ρ(π) = e.

Example 8 .

 8 Assuming T I is the model in Example 6, we have that (CfgI, S I , Σ I , Π I , T I ) is a matching logic semantic domain for the IMP language.

Fig. 4 .

 4 Matching logic semantics of FUN as a set AF of reachability rules schemata. op ranges over the binary function symbols and op Int is their denotation in TF Example 10. Figures3 and 4presents the set of reachability rules A I and A F required to define the IMP and, respectively, the FUN languages.

  e 1 , . . . , e n ) for all f ∈ Σ s1,...,sn,s and for all e 1 ∈ s 1 T ′ ↾ h , . . ., e n ∈ s n T ′ ↾ h . 3. (e 1 , . . . , e n ) ∈ p T ′ ↾ h iff (e 1 , . . . , e n ) ∈ h(p) T ′ for all p ∈ Π s1,...,sn and for all e 1 ∈ h(s 1 ) T ′ , . . . , e n ∈ h(s n ) T ′ . Example 3. Let Φ = ({Int}, {op Int | op ∈ { + , -, * }}, {op Int | op ∈ {=, < , ≤}) be a signature and let h (with h(Int) = Int and h(op Int ) = op Int for op ∈ { + , -, * }) be a morphism from Φ to Φ I (defined above in Example 1). Let T I be the model of Φ I considered above in Example 2. We have that Int T ′ ↾ h is the set of integers, + Int T ′ ↾ h is the addition of integers, etc.


A Chellali

Woojin Ahn

Ganesh Sankaranarayanan

J T Flinn

S D Schwaitzberg

Suvranu Daniel B Jones

Suvranu De

Caroline G L Cao
email: caroline.cao@wright.edu

Dr D Steven

Drs Amine Chellali

Preliminary evaluation of the pattern cutting and the ligating loop virtual laparoscopic trainers

Keywords: Surgical training, virtual reality (VR), Virtual Basic Laparoscopic Surgical Trainer (VBLaST), Fundamentals of Laparoscopic Skills (FLS), Force feedback

Introduction:

The Fundamentals of Laparoscopic Surgery (FLS) trainer is currently the standard for training and evaluating basic laparoscopic skills. However, its manual scoring system is time-consuming and subjective. The Virtual Basic Laparoscopic Skill Trainer (VBLaST © ) is the virtual version of the FLS trainer which allows automatic and real time assessment of skill performance, as well as force feedback. In this study, the VBLaST © pattern cutting (VBLaST-PC © ) and ligating loop (VBLaST-LL © ) tasks were evaluated as part of a validation study. We hypothesized that performance would be similar on the FLS and VBLaST © trainers, and that subjects with more experience would perform better than those with less experience on both trainers.

Methods: Fifty-five subjects with varying surgical experience were recruited at the Learning Center during the 2013 SAGES annual meeting and were divided into two groups: experts (PGY 5, surgical fellows and surgical attendings) and novices (PGY 1-4). They were asked to perform the pattern cutting or the ligating loop task on the FLS and the VBLaST © trainers.

Their performance scores for each trainer were calculated and compared.

Results: There were no significant differences between the FLS and VBLaST © scores for either the pattern cutting or the ligating loop task. Experts' scores were significantly higher than the scores for novices on both trainers.

Conclusion:

This study showed that the subjects' performance on the VBLaST © trainer was similar to the FLS performance for both tasks. Both the VBLaST-PC © and the VBLaST-LL © tasks permitted discrimination between the novice and expert groups. Although concurrent and discriminant validity has been established, further studies to establish convergent and predictive validity are needed. Once validated as a training system for laparoscopic skills, the system is expected to overcome the current limitations of the FLS trainer.

INTRODUCTION

Laparoscopic surgery is the preferred technique for many general procedures from the patients' perspective (smaller incisions, less blood loss, decreased analgesic requirements, and quicker postoperative recovery) [START_REF] Maithel | Construct and face validity of MIST-VR, Endotower, and CELTS: are we ready for skills assessment using simulators?[END_REF]. However, laparoscopic surgeons develop skills and face many challenges that are different from what they experience in open surgery. These skills include handling tissues with instruments that have limited degrees of freedom and that provide limited haptic feedback, or dealing with altered hand-eye coordination due to changes in depth perception and to indirect vision [START_REF] Cao | Direct, 2-D vs. 3-D endoscopic viewing & surgical task performance. A Symposium on Evolving Technologies: Surgeons' Performance of Surgical Tasks[END_REF]. Therefore, there is a need to establish dedicated training curricula and assessment tools to help surgeons build an acceptable level of laparoscopic skills and thus maintain safe surgical practices [START_REF] Adrales | Evaluating minimally invasive surgery training using low-cost mechanical simulations[END_REF][START_REF] Peters | Development and validation of a comprehensive program of education and assessment of the basic fundamentals of laparoscopic surgery[END_REF].

In this context, surgical simulators have gained momentum in the last decade as the training environments of choice for laparoscopic surgery [START_REF] Powers | Preliminary Evaluation of the VBLaST-PT © and VBLaST-LL © RJ (2002) House staff performance is improved by participation in a laparoscopic skills curriculum[END_REF]. One of the currently most popular simulators is the Fundamentals of Laparoscopic Surgery (FLS) trainer. This physical-box trainer, based on the McGill Inanimate System for Training and Evaluation of Laparoscopic Skills (MISTELS) [START_REF] Fraser | valuating laparoscopic skills: setting the pass/fail score for the MISTELS system[END_REF], was developed to teach and measure basic laparoscopic skills through five basic tasks: peg transfer, pattern cutting, ligating loop, suturing with intracorporeal knot, and suturing with extracorporeal knot [START_REF] Peters | Development and validation of a comprehensive program of education and assessment of the basic fundamentals of laparoscopic surgery[END_REF].

The FLS trainer is currently used as the standard method for assessing the proficiency of laparoscopic surgical skills by the Society of American Gastrointestinal and Endoscopic Surgeons (SAGES) and the American College of Surgeons (ACS) [START_REF] Fried | FLS assessment of competency using simulated laparoscopic tasks[END_REF], and the successful completion of the FLS examination (including a didactic component) has become a requirement for all general surgeons in the USA since 2009.

However, the FLS trainer is relatively expensive and resource intensive as it requires a large supply of consumables, lacks objective methods for performance assessments, and is timeconsuming and labor intensive [START_REF] Fraser | valuating laparoscopic skills: setting the pass/fail score for the MISTELS system[END_REF][START_REF] Botden | Augmented versus Virtual Reality Laparoscopic Simulation: What Is the Difference?[END_REF][START_REF] Sankaranarayanan | Preliminary face and construct validation study of a virtual basic laparoscopic skill trainer[END_REF].

Virtual Reality (VR) technology provides a safe and versatile practice medium for teaching laparoscopic skills [START_REF] Chellali | Haptic communication to support biopsy procedures learning in virtual environments[END_REF] and can overcome some limitations of the physical trainer box. For example, the VR-based systems can be used multiple times, with no need of consumables.

They provide objective and automated measurement of performance, which can improve the evaluation process [START_REF] Grantcharov | Virtual reality computer simulation[END_REF]. Furthermore, they can be designed to provide haptic feedback, an essential component for training minimally invasive surgery skills [START_REF] Chellali | Haptic communication to support biopsy procedures learning in virtual environments[END_REF][START_REF] Reich | High-level virtual reality simulator for endourologic procedures of lower urinary tract[END_REF][START_REF] Dang | Development and evaluation of an epidural injection simulator with force feedback for medical training[END_REF][START_REF] Panait | The Role of Haptic Feedback in Laparoscopic Simulation Training[END_REF][START_REF] Seymour | Virtual Reality Training Improves Operating Room Performance Results of a Randomized, Double-Blinded Study[END_REF][START_REF] Ström | Early exposure to haptic feedback enhances performance in surgical simulator training: a prospective randomized crossover study in surgical residents[END_REF].

However, before introducing this technology into training curricula, there is a need to demonstrate its validity as a training tool and also as an instrument for assessing skill in laparoscopic surgery [START_REF] Aggarwal | An evidence-based virtual reality training program for novice laparoscopic surgeons[END_REF].

Lap-X (Epona Medical, Rotterdam, The Netherlands) [START_REF] Medical | LAP-X[END_REF] LAP Mentor (Simbionix USA, Cleveland, OH) [START_REF] Zhang | Construct validity testing of a laparoscopic surgery simulator (Lap Mentor): evaluation of surgical skill with a virtual laparoscopic training simulator[END_REF], and LapVR (Immersion Medical, Gaithersburg, MD) [START_REF] Iwata | Construct validity of the LapVR virtual-reality surgical simulator[END_REF] are examples of commercially available VR systems for laparoscopic surgery training. However, some of these systems lack realistic haptic feedback, are costly, or have not been validated for training of laparoscopic skills (e.g., Lap-X) [START_REF] Ayodeji | Face validation of the Simbionix LAP Mentor virtual reality training module and its applicability in the surgical curriculum[END_REF][START_REF] Salkini | The role of haptic feedback in laparoscopic training using the LapMentor II[END_REF][START_REF] Gallagher | Human factors in acquiring medical skills; learning and skill acquisition in surgery[END_REF][START_REF] Arikatla | Face and construct validation of a virtual peg transfer simulator[END_REF].

The Virtual Basic Laparoscopic Surgical Trainer (VBLaST © ) is a new VR-based training system, which simulates the five basic laparoscopic tasks present in the FLS trainer box [START_REF] Sankaranarayanan | Preliminary face and construct validation study of a virtual basic laparoscopic skill trainer[END_REF].

The main motivation of designing this system was to overcome some of the current limitations of the FLS trainer. As such, VBLaST © includes automated assessments of laparoscopic skills and repeated trials with no need to replenish materials. Moreover, the system provides haptic feedback to the user through a haptic device. The VBLaST © simulating the peg transfer task of the FLS trainer has been previously validated [START_REF] Arikatla | Face and construct validation of a virtual peg transfer simulator[END_REF][START_REF] Zhang | Characterizing the learning curve of the VBLaST-PT© (Virtual Basic Laparoscopic Skill Trainer)[END_REF]. In this study, two new tasks of the VBLaST © system, namely, the pattern cutting (PC) task and the ligating loop (LL) task, are evaluated. This research is part of a larger study which aims to validate the VBLaST as a training system for laparoscopic surgical skills. The objective of this study was to compare the current version A. Chellali et al.: Preliminary Evaluation of the VBLaST-PT © and VBLaST-LL © of the VBLaST © system, which includes the pattern cutting and ligating loop tasks, to the FLS trainer. It was hypothesized that subjects' performance would be similar on VBLaST © and the FLS trainers (H1) for both tasks. In addition, subjects with more experience would perform better than those with less experience or no experience at all, when using either the FLS or the VBLaST © (H2) for both tasks. For each task, subjects were divided into two groups according to experience (Table 1): experts (surgical fellows and practicing laparoscopic surgeons) and novices (PGY 1-4).

METHODS

Table 1: Composition of the subject groups per task

Apparatus

The FLS and the VBLaST © (Figure 1) were used to perform the pattern cutting and ligating loop tasks. For the pattern cutting task, the work space of the FLS trainer consisted of a piece of gauze with a pre-marked black circle, placed in the center of the FLS box trainer and secured with clips. For the ligating loop task, the work space of the FLS trainer consisted of a The VBLaST © simulator consists of computational software to graphically simulate the FLS work space for both tasks (Figure 1), and a physical user interface to connect different laparoscopic instruments (one Maryland dissector and one endoscopic scissors for the pattern cutting task; one pre-tied ligating loop, one grasper with locked handle and one endoscopic scissors for the ligating loop task) to two PHANTOM Omni haptic devices (Geomagic Inc., Boston, MA, USA). These devices allow force feedback to be transmitted to the users when interacting with the virtual environment. For the FLS tasks, one experimenter manually recorded the subjects' task completion time with a stop watch. Penalty scores for the LL task were calculated manually by the same experimenter after each trial. PC penalty scores (based on the deviations from the circle cutting) were calculated using a custom-built image analysis tool that has been validated and reported elsewhere [START_REF] Flinn | Technology-based procedure for automatic and objective error measurement in FLS pattern cutting task[END_REF]. The method consists of digitally scanning the cut pieces of gauze and analyzing them by the image analysis software to compute the area of error, both inside and outside the prescribed circle. This automatic scoring method provides a quick, accurate, and consistent error measurement for PC scoring.

Groups

The performance measures for the VBLaST © (both time and penalties) were automatically recorded by the system for both tasks.

Tasks

The pattern cutting task

For this task, the subjects were given one Maryland dissector and one endoscopic scissors, and were allowed to interchange the left and the right instruments only at the beginning of the task. One hand was used to provide traction on the gauze using the Maryland dissector and to place the gauze at the best possible angle to the cutting hand. The subjects were instructed to cut the gauze as accurately as possible along the marked circle. Timing started when the gauze was grasped and ended upon completion of cutting the marked circle. A penalty was assessed for any deviation from the line demarcating the circle.

The ligating loop task

For this task, the subjects were required to place a pre-tied ligating loop around the tubular foam appendage and secure the knot on a provided black mark. The subjects were given one pre-tied ligating loop, one grasper with a locking handle, and one endoscopic scissors. They were instructed to insert the ligating loop into the field of view and to position it properly. The knot had then to be secured on the mark near the base of the foam appendage by sliding the pusher rod down. Once the knot was secured, the string had to be cut using the scissors.

Timing started when the appendage was grasped and ended when the string was cut. A penalty was assessed for any deviation from the predetermined marking.

Procedure

Before the start of the experimental session, subjects were asked to fill out a questionnaire detailing the demographics and their previous laparoscopic surgery experience. They were then shown an instructional video describing the pattern cutting task or the ligating loop task.

After that the subjects were asked to perform one trial of the assigned task on both the FLS and the VBLaST © trainers. To control the effect of simulators' order on the performance, the presentation order of the simulators (FLS vs VBLaST) was counterbalanced. That is, half the A. Chellali et al.: Preliminary Evaluation of the VBLaST-PT © and VBLaST-LL © subjects were randomly assigned to begin with the FLS, while the other half of the subjects began with the VBaST. At the end of the session, the subjects were asked to complete another questionnaire evaluating the features of the VBLaST © trainer compared with the FLS trainer, using a 5-point Likert scale (from very poor/not satisfactory to very good/very satisfactory).

The questions were related to visual appearance, haptic feedback, 3D perception, tool movements and overall quality and reliability of the system as a training and assessment tool.

As a further step in data collection and validation, the subjects were given the opportunity to comment on their experience with the system after session completion.

Dependent measures

For the FLS trainer, the dependent measures consisted of a total raw score (ranging from 0 to 300) calculated using undisclosed formula for the FLS [START_REF] Fraser | valuating laparoscopic skills: setting the pass/fail score for the MISTELS system[END_REF]. For each task, the raw score was calculated using a combination of the task completion time and the penalty score. These raw scores were then divided by a normalization factor that was calculated using the best expert FLS score obtained in the FLS condition [START_REF] Fraser | valuating laparoscopic skills: setting the pass/fail score for the MISTELS system[END_REF][START_REF] Arikatla | Face and construct validation of a virtual peg transfer simulator[END_REF]. The FLS normalized scores ranged from 0 to 100. For the VBLaST © trainer, the raw score was automatically calculated by the system using the same formula. These raw scores were then divided by a normalization factor calculated using the best expert score obtained from the VBLaST © condition in the experiment. The VBLaST © normalized scores also ranged from 0 to 100.

Data analysis

Since the data were not normally distributed (tested using the Shapiro-Wilk test

RESULTS

The pattern cutting task

Correlation tests

The Spearman's correlation test showed that the pattern cutting FLS PC and VBLaST-PC © mean normalized scores had a correlation of 0.47 (Spearman's r(31) = 0.47, p = 0.006).

The effect of experience and simulator order

The Mann Whitney U-test showed that the FLS PC and the VBLaST-PC © scores (Figure 2)

were significantly higher in the expert group than in the novice group (U = 39, Z = 3.49, p < 0.0001; U = 68, Z = 2.45, p = 0.01, respectively).

Finally, the Mann Whitney U-test showed no significant effect of the order of simulators either on the FLS scores or on VBLaST scores (U = 133, Z = -0.10, p > 0.05; U = 99, Z = 1.33, p > 0.05, respectively). The Wilcoxon signed rank sum test showed no significant difference (Figure 2) between the FLS PC scores and the VBLaST-PC © scores (Z = 1.94, p > 0.05). The subjective ratings of the VBLaST-PC © features are shown in Figure 3. The average rating for "realism of objects" was the highest. "Usefulness of VBLaST for training laparoscopic skills" was rated second highest. "Realism of instrument handling", "quality of force feedback" and "trustworthiness in quantifying performance measures" had the lowest ratings.

The effect of simulator

Subjective evaluation

Only 28% of the subjects preferred using the VBLaST-PC © over the FLS box for training laparoscopic surgery skills.

The ligating loop task

Correlation tests

The Spearman's correlation test showed that the FLS LL and VBLaST-LL © mean normalized scores had a correlation of 0.53 (Spearman's r(20) = 0.53, p = 0.01).

The effect of experience and simulator order

The Mann Whitney U-test showed that the FLS LL and the VBLaST-LL © scores were significantly higher (Figure 4) in the expert group than in the novice group (U = 27.5, Z = 2.16, p = 0.03; U = 34, Z = 2.13, p = 0.03, respectively).

Finally, the Mann Whitney U-test showed no significant effect of the order of simulators on either the FLS scores or VBLaST scores (U = 52.5, Z = -0.52, p > 0.05; U = 43.5, Z = -1.11, p > 0.05, respectively).

The effect of simulator

The Wilcoxon signed rank sum test showed no significant difference (Figure 4) between the FLS LL scores and the VBLaST-LL © scores (Z = 0.21, p > 0.05).

Subjective evaluation

The subjective ratings of the VBLaST-LL © features are shown in Figure 5. The average ratings for "realism of objects" and "usefulness of VBLaST for learning" were the highest.

"Realism of instrument handling" and "usefulness of force feedback" had the lowest ratings.

Only 30% of the subjects preferred using the VBLaST-LL © over the FLS for training laparoscopic surgery skills.

DISCUSSION

VR is a promising technology that can overcome some limitations of the existing laparoscopic box simulators such as the FLS trainer. This study aimed to evaluate two tasks on the VBLaST © system, the new VR-based trainer for basic laparoscopic technical skills. By comparing the VBLaST © to the validated FLS trainer, we showed that the subjects' performance for the pattern cutting and ligating loop tasks was similar on both systems. This finding supports our first hypothesis and suggests that the VR simulation has faithfully reproduced the content of the FLS system.

The results also demonstrated the concurrent validity of the VBLaST © system, i.e., allowing discrimination between the novice and expert groups. For both tasks, the experts performed significantly better than novices. Finally, the results showed that the VBLaST © scores and the FLS scores were significantly correlated for both tasks although the correlation coefficients were of medium strength (0.47 and 0.53). These results suggest that some aspects of the FLS system were correctly reproduced in VBLaST while others require some improvements to acquire a higher correlation score. In this context, the subjective evaluation and the participants' comments provide valuable information for future improvements of the VBLaST © user interface.

Although they were satisfied by the quality of the graphical user interface in both tasks, the subjects' rating of the realism of instrument handling was low. This suggests that they had difficulty adapting to the use of real instruments with virtual objects. Moreover, the subjects rated the quality of the system's force feedback as low. They commented that the haptic feedback was more important during the pattern cutting task than in the other FLS tasks. In fact, the main learning objective of the task was to be able to apply the correct tension/counter tension on the tissue to cut it properly. Although the quality of the system's haptic feedback did not prevent the users' from completing this task, improvements in the realism of haptic feedback will be necessary to achieve a higher quality training simulator.

For the ligating loop task, the subjects commented that the virtual loop behaved differently from the actual tool. For instance, the subjects felt that the virtual loop slides too easily on the appendage, preventing them from securing it accurately on the mark. While this did not prevent the task from being completed, it is necessary to improve the virtual physics to ensure the learning of correct laparoscopic skills in this task.

Finally, although the users agreed on the usefulness of VR technology for training laparoscopic skills, most of them preferred to use the FLS trainer. Hence, improvements in the manipulation of the tools and the realism of haptic feedback will be necessary to improve the user's willingness to adopt this new technology.

LIMITATIONS AND FUTURE WORK

The limited number of trials per subjects on each simulator (only one trial per system) may have influenced the users' performance in our study. Nevertheless, it provided us with the much needed feedback at an early stage of the system development and served to inform our design modifications of the VBLaST © system. Our design approach for the VBLaST © system utilizes the user-centered design method (as prescribed by ISO 13407). This method is based on an iterative process and recommends involving the end users during the different design stages [START_REF]Human-centred design processes for interactive systems[END_REF]. The study findings suggest that some components of the system were correctly reproduced while others will require another design iteration to be improved. Future developments will include improvement of the physical user interface and the virtual environment physics with a focus on the learning objectives of each task. For instance, force sensors will be mounted on real instruments to measure the exact forces felt by the trainees when using the real FLS box. These measurements can then be used to improve the haptic feedback on the VBLaST system. Moreover, other measurements will also be used to improve the physical behavior of the virtual objects and enhance the realism of the VBLaST system.

Currently, only one study has been conducted to compare the automated assessment method of the pattern cutting task used in the VBLaST system with the manual scoring method currently in use showing advantages in speed, accuracy, and precision for the automated method [START_REF] Flinn | Technology-based procedure for automatic and objective error measurement in FLS pattern cutting task[END_REF]. More investigations are necessary to validate the automated scoring method for the other tasks and further demonstrate the value of the VBLaST system.

Although not addressed here, the issue of cost savings in consumables must be balanced by the cost of the VR simulator itself. Further studies will be conducted in the future before offering the VBLaST © as an alternate training standard for laparoscopic surgery.

Participants

  Fifty-five (55) subjects(25-56 years old) with varied experience in surgery were recruited in this Institutional Review Board (IRB) approved study at the Learning Center during the 2013 SAGES annual meeting. Three of the subjects were left-handed. Thirty-three subjects (27 males, 6 females, 2 left handed) performed the pattern cutting task while twenty-two subjects (20 males, 2 females, 1 left handed) performed the ligating loop task.

  et al.: Preliminary Evaluation of the VBLaST-PT © and VBLaST-LL © red organ-shaped foam, with appendages, placed in a clip at the center of the FLS box trainer such that the appendages are free and visible in the field of view.

Figure 1 :

 1 Figure 1: (A) the pattern cutting trainers, (B) the ligating loop trainers (Left trainer:

Figure 2 :

 2 Figure 2: effect of experience for each simulator on the performance scores in the pattern

Figure 3 :

 3 Figure 3: Subjective evaluations of the VBLaST-PC © trainer (error bars represent the standard

Figure 4 :

 4 Figure 4: effect of experience for each simulator on the performance scores in the ligating

Figure 5 :

 5 Figure 5: Subjects' ratings of the VBLaST-LL© trainer (error bars represent the standard

A.

  Chellali et al.: Preliminary Evaluation of the VBLaST-PT © and VBLaST-LL ©

  . Chellali et al.: Preliminary Evaluation of the VBLaST-PT © and VBLaST-LL ©

	), non-
	parametric statistical tests were used to analyze the data. The Spearman correlation test, the
	Wilcoxon signed rank sum test, and the Mann-Whitney's U-test were used, wherever
	appropriate. P values under 0.05 were considered significant. Descriptive statistics (the mean

subjective ratings and the standard errors) were used to analyze the questionnaire data. All analyses were performed using SPSS v.21.0 (IBM Corp., Armonk, NY, USA).

A

This work was supported by NIBIB/NIH Grant # R01EB010037. Evaluation of the VBLaST-PT © and VBLaST-LL © AKNOWLEDGEMENTS This project was supported by National Institutes of Health (NIH) Grant NIBIB R01 EB010037-01. This research was conducted in collaboration with the SAGES FLS Committee.