Piotr Nienaltowski
email: piotr.nienaltowski@praxis-his.com

Bertrand Meyer

Jonathan S Ostroff

Formal Aspects of Computing Contracts for concurrency

Keywords: Concurrency, Object-oriented programming, Design by contract, SCOOP, Software verification, Safety and liveness properties, Partial correctness

The SCOOP model extends the Eiffel programming language to provide support for concurrent programming. The model is based on the principles of Design by Contract. The semantics of contracts used in the original proposal (SCOOP 97) is not suitable for concurrent programming because it restricts parallelism and complicates reasoning about program correctness. This article outlines a new contract semantics which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that it is indeed a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs-similar to those for traditional non-concurrent programs-of partial correctness and loop termination in the presence of asynchrony.

Introduction

Design by Contract (DbC) permits enriching class interfaces with assertions expressing the mutual obligations of clients and suppliers [START_REF] Meyer | Applying "Design by contract[END_REF]. Routine preconditions specify the obligations on the routine client and the guarantee given to the routine supplier; routine postconditions express the obligation on the supplier and the guarantee given to the client. Class invariants express the correctness criteria of a given class; an instance of a class is consistent if and only if its invariant holds in every observable state. The modular design fostered by DbC reduces the complexity of software development: correctness considerations can be confined to the boundaries of components (classes) which can be proved and tested separately. Clients can rely on the interface of a supplier without the need to know its implementation details.

We define the correctness of a routine as follows.

Definition 1 (Local correctness). A routine r of class C is locally correct if and only if, after the execution of r's body, both the class invariant Inv C of C and the postcondition Post r of r hold, provided that both Inv C and the precondition Pre r were fulfilled at the time of the invocation.

The sequential proof technique [START_REF] Meyer | Object-oriented software construction[END_REF] follows this definition which can be captured more formally by the following proof rule:

{INV ∧ Pre r } body r {INV ∧ Post r } {Pre r [a/f ]} x.r(a) {Post r [a/f ]} (2)
Correspondence and offprint requests to: P. Nienaltowski, E-mail: piotr.nienaltowski@praxis-his.com This rule says that if a routine r is locally correct (according to Definition 1) then a call to r in a state that satisfies its precondition will terminate in a state that satisfies its postcondition. Clients simply need to ensure that the precondition holds before the call; they may assume the postcondition in return.

It is tempting to apply the same rule to reasoning about concurrent programs. Unfortunately, the standard correctness semantics of assertions breaks down in a concurrent setting. In particular, clients may be unable to satisfy preconditions that depend on the state of shared objects; no matter how hard they try to establish such preconditions, other clients' actions may invalidate them. To deal with this problem, the original model [START_REF] Meyer | Object-oriented software construction[END_REF], called "SCOOP 97" here, uses two different semantics for preconditions, depending on whether they involve separate calls (calls targeting objects accessible to several clients). Separate preconditions are wait conditions, i.e. a violated precondition causes the client to wait. Non-separate ones are correctness conditions, i.e. a nonsatisfied precondition is a contract violation and results in an exception. This mitigates the problem but the clash between wait conditions and correctness conditions is a source of other problems; for example a call may deadlock if it uses a non-separate actual argument for a separate formal and the associated wait condition does not hold. Furthermore, SCOOP 97 does not exploit the potential of other assertions in a concurrent context: postconditions, loop assertions and check instructions simply keep their sequential semantics. Separate postconditions are particularly problematic: they cause waiting, thus minimise the potential for parallelism and increase the likelihood of deadlock. Since interesting properties of concurrent programs are expressed as separate assertions, and such assertions are completely excluded from proof rules, this limits formal reasoning about concurrent programs.

We propose to solve these problems by "lifting" the principles of DbC to the concurrent context, so that assertions capture the full contract between a client and a supplier, including synchronisation. This requires a new, uniform semantics of contracts applicable in both concurrent and sequential contexts, and a modular proof technique which supports reasoning about interesting properties of concurrent programs in style similar to the above proof technique. We want both the new semantics and the new proof technique to reduce in a straightforward manner to their traditional counterparts when no concurrency is involved.

The article is organised as follows. Section 2 gives a summary of the computational model. (We use the refined SCOOP model described in the first author's PhD thesis [START_REF] Nienaltowski | Practical framework for contract-based concurrent object-oriented programming[END_REF]; a description of the original SCOOP 97 can be found in [START_REF] Meyer | Object-oriented software construction[END_REF].) Sections 3-6 discuss the semantics of preconditions, postconditions, invariants, and loop assertions respectively. Section 7 introduces the proof rule for asynchronous and synchronous calls. Section 8 points out the limitations of the proposed proof technique, and analyses the interplay of the new semantics with other SCOOP mechanisms. Section 9 discusses related work.

SCOOP model

Concurrency in SCOOP relies on the basic mechanism of object-oriented computation: the feature call 1 . Each object is handled by a processor-a conceptual thread of control-called the object's handler. All features of a given object are executed by its handler; as a result, only one processor may access any object at any time. Several objects may have the same handler; the mapping between an object and its handler does not change over time. If a client object and its supplier have the same handler, the feature call is synchronous; if they have different handlers, the call becomes asynchronous, i.e. the computation on the client's handler may move ahead without waiting. Objects handled by different processors are called separate from each other; objects handled by the same processor are non-separate. Likewise, we talk about separate and non-separate calls, entities, and expressions. A processor, together with the objects it handles, forms a sequential system. Therefore, every concurrent system may be seen as a collection of interacting sequential systems; conversely, a sequential system may be seen as a particular case of a concurrent system (with only one processor).

Since each object may be manipulated only by its handler, there is no object sharing between different threads of execution (no shared memory). Given the sequential nature of processors, this results in the absence of intraobject concurrency: there is never more than one action performed on a given object. Therefore, programs are data-race-free by construction. Locking is used to eliminate atomicity violations: illegal interleavings of calls from different clients. For a feature call to be valid, it must appear in a context where the client's processor holds a lock on the supplier's processor, meaning (as we will see in Definition 4 below) that the supplier is controlled by the client. Locking is achieved through a revised form of the mechanism of feature application: the processor 1 A feature is either a routine or an attribute defined in a class. executing a routine with attached formal arguments blocks until the processors handling these arguments have been locked (atomically) for its exclusive use; the routine serves as a critical section. Since a processor may be locked and used by at most one other processor at a time, and all feature calls on a given supplier are executed in a FIFO order, no harmful interleaving occurs. Clients resynchronise with their suppliers if and when necessary, thanks to wait by necessity [START_REF] Caromel | Towards a method of object-oriented concurrent programming[END_REF]: clients wait only on queries (function or attribute calls) because they return some result; commands (procedure calls) do not require waiting.

Preconditions

In a sequential context, a precondition is a correctness condition: the client has to guarantee that the precondition holds at the moment of the call. The supplier expects the precondition to hold when the execution of the routine starts. Since all calls are synchronous, feature application (the action of applying a feature to a target object, performed by the target object's processor) follows the feature call (the action of calling a feature, performed by the client's processor); no other event may happen in between. Therefore, any property that holds at the call time also holds at the application time; conversely, any property that does not hold at the call time does not hold at the application time. Hence the usual understanding of the client's obligation: the precondition must hold at the call time.

In a concurrent context, the feature call and the feature application do not necessarily coincide; other events may happen in between. Therefore, a supplier cannot assume that a property satisfied at the call time still holds at the application time. (This is the source of the separate precondition paradox [START_REF] Meyer | Object-oriented software construction[END_REF].) Conversely, a property that does not hold at the time of the call may become true later on; the supplier could safely execute the feature at that time. These observations lead to treating preconditions as a synchronisation mechanism: a called feature cannot be executed unless the precondition holds; a violated precondition delays the execution of the feature. This wait semantics is reflected by the refined feature application mechanism and the feature application rule introduced in Sect. 6.1 of [START_REF] Nienaltowski | Practical framework for contract-based concurrent object-oriented programming[END_REF].

SCOOP 97 uses both semantics, depending on whether a given precondition clause involves separate calls. The precondition clause i > 0 in Fig. 1 is a correctness condition because it involves no separate calls, whereas not buffer.is full has the wait semantics. This distinction is somewhat artificial because buffer, although declared as separate, may denote a non-separate object at run time, for a call such as store (ns buffer, 10). Should wait semantics apply here? If yes, the client will be blocked forever if ns buffer is full. In this example, the static type of the actual argument is non-separate; but the same problem may occur even if the actual argument has a separate type, for example in the subsequent call store (s buffer, 79). Clearly, wait semantics should be replaced by correctness semantics here.

Sometimes, the opposite is required: a correctness condition should be turned into a wait condition. This happens in the presence of polymorphism and feature redefinition. A class that redefines a feature may change the type of a formal argument from non-separate to separate; such redefinitions are safe because clients of the original class may only use a non-separate actual argument. The precondition clauses that involve the redefined The necessity to turn wait conditions occasionally into correctness conditions, and occasionally to do the reverse, suggests a uniform semantics of preconditions. We adopt the semantics captured by Definition 3. Definition 3 (Semantics of preconditions). A precondition expresses the necessary requirements for a correct application of a feature. The execution of the feature's body is delayed until the precondition is satisfied.

The guarantee given to the supplier is exactly the same as with the traditional semantics: the precondition holds on entry to the feature's body. Nevertheless, the definition does not force the clients to ensure the precondition before the call. A client performing a feature call naturally has certain obligations, but it must share the responsibility for establishing the precondition with the environment: the client should be blamed for any contract breaches that it could have avoided; the environment is responsible for everything that is not under the client's control. Meyer [START_REF] Meyer | Object-oriented software construction[END_REF] argues that only non-separate precondition clauses are binding for the client. We go one step further: since the client has full control over controlled expressions, which represent objects whose processors are locked by the client's processor (see Definition 4), it should be blamed for breaches in precondition clauses involving such expressions. Therefore, we extend the client's responsibilities to all controlled clauses.

Definition 4 (Controlled expression

). An expression exp is controlled if and only if exp is attached (statically known to be non-void) and either exp is non-separate or exp is handled by the same processor as some formal argument of the routine r in which exp appears.

Definition 5 (Controlled clause). For a client performing the call x.f (a) in the context of a routine r, a precondition clause or a postcondition clause of f is controlled if and only if, after the substitution of the actual arguments a for the formal arguments, it only involves calls on expressions that are controlled in the context of r; otherwise, it is uncontrolled.

We have chosen assertion clauses as units of controllability, although finer-grained units could be used instead. Assertion clauses are convenient because they are clearly demarcated in the program text. Also, Eiffel follows this style for the representation of inherited and immediate assertions in redefined features.

Figure 2 illustrates the difference between controlled and uncontrolled precondition clauses. For the client executing the call x.store (s buffer, 10) in the body of r, the first precondition clause of store is uncontrolled because, after the substitution of actuals for formals, it involves the expression s buffer.is full whose target s buffer is not controlled in the context of r. On the other hand, the same precondition clause is controlled in the three remaining calls to store because the targets of the involved expressions are controlled in r: ns buffer is non-separate; buf is separate but locked by r; x.ns buffer is separate, but it is non-separate from x and x is controlled, therefore x.ns buffer is controlled too (see Definition 4). The second precondition clause i > 0 is controlled in all cases because the expected actual argument is handled by the same processor as the target x. (x itself is controlled; otherwise, no calls on x would be allowed in r.) In this particular case, the actual argument is expanded2 , hence controlled in any context.

Coming back to the client's responsibilities: each controlled precondition clause must be satisfied by the client. But the calls on x in Fig. 2 are asynchronous; how can the client ensure a property if the previously scheduled calls are still being executed and may change the state of the involved objects? Indeed, the state of x and buf at the moment of the call x.store (buf, 79) may be different from their state at the moment the feature gets actually applied; the client knows, however, that all its calls on x and buf are performed in the FIFO order, allowing the client programmer to reason sequentially about the execution. That is, the state of x and buf at the moment of the application of store (buf, 79) is exactly the same as it was when store (ns buffer, 24) terminated. The client only needs to ensure that the properties established by x.store (ns buffer, 24) imply the precondition of x.store (buf, 79). It does not matter that the precondition may not hold at the moment of the call; it will hold when required, at the moment of the feature application.

The establishment of uncontrolled precondition clauses depends on the emergent behaviour of the whole system. The client cannot take responsibility for such preconditions: calling a feature with an uncontrolled precondition clause may result in indefinite waiting; see Sect. 8.1 for a detailed discussion of this problem.

Although we use the same name for the proposed wait semantics of preconditions, there are three major differences with respect to SCOOP 97:

• The semantics applies to all preconditions; there is no distinction between separate and non-separate clauses.

• Clients are responsible for establishing all controlled precondition clauses, not only the non-separate ones.

• Waiting happens on the supplier side. For example, the client executing the call x.store (s buffer, 10) in Fig. 2 is not blocked; it is x's handler that waits until the precondition is satisfied. (If the client and the supplier are non-separate from each other, then waiting on the supplier side is equivalent to waiting on the client side.)

Even though a precondition violation causes waiting, this waiting is only conceptual in the case of controlled clauses: if a controlled precondition clause is violated when it is supposed to hold (at the moment of the feature application), waiting is useless because the state of the involved objects cannot change in the meantime as they are handled by the client's processor; an exception is raised instead. In a sequential setting, this semantics is equivalent to the traditional correctness semantics because all precondition clauses involve only non-separate expressions and are therefore controlled (see Definition 5). For example, the call store (ns buffer, 10) in Fig. 1 can be handled correctly: if the precondition not buffer.is full does not hold during the execution, the result will be to trigger an exception. Similarly, the application of store with a negative second argument results in an exception because the precondition i > 0 is violated. Since the feature application happens immediately after the corresponding feature call, it looks as if the exception occurs at the moment of the call, just as with traditional sequential semantics.

Postconditions

The original design of SCOOP 97 applied the standard correctness semantics to separate postconditions; they are evaluated synchronously and understood to hold immediately when the feature call terminates. Meyer [START_REF] Meyer | Object-oriented software construction[END_REF] discusses the separate postcondition paradox: on return from a separate call, the client cannot be sure that the postcondition still holds: the processor handling the involved supplier may become free in the meantime so that other clients may modify its state, thus invalidating the postcondition. Rodriguez et al. [RDF + 05] refer to the same problem as external interference.

The treatment of postconditions in SCOOP 97 is unsatisfactory for two reasons:

• Separate postconditions are excluded from the proof rule for feature calls; this limits considerably the range of safety properties that can be proven. • The synchronous evaluation of separate postconditions limits the parallelism and may lead to deadlocks. Suppose the client executing the call spawn two activities (york, tokyo) in Fig. 3 wants to launch jobs at two independent locations, with the guarantee that the job at each location will eventually terminate. Such guarantees are most naturally expressed as postconditions of spawn two activities. The synchronous semantics of postconditions would block the client until the call terminates: the subsequent operation do local stuff would not be performed until both postcondition clauses post 1 and post 2 of spawn two activities have been evaluated. The amount of effective parallelism would be much lower than without the postconditions, where the client is able to move on immediately (but there is no guarantee that the jobs are done). To take advantage of parallelism without sacrificing the guarantees given to the client, postconditions should be evaluated asynchronously, that is to say treated similarly to command calls: wait by necessity should not apply. As a result, the client can now move on with its next activity (do local stuff) without waiting for the evaluation of post 1 and post 2; but it still gets the guarantee that both clauses will be satisfied eventually. More precisely, they will be satisfied when the execution of the features called within the body of spawn two activities terminates. Because york and tokyo are separate from the client (and from each other), the calls to do job are asynchronous, so post 1 and post 2 do not necessarily hold when the client executes do local stuff; but this does not matter because york and tokyo are not used in that operation. The clause post 1 becomes relevant only at the moment of the call to get result (york), which cannot start its execution until all the previous calls on york have terminated. Therefore, get result cannot be executed until york terminates the job requested by spawn two activities; when this happens, the postcondition post 1 stating that york.is ready holds. This property implies the precondition of the routine get result, which as a result can now be executed. The client is not penalised by the asynchronous evaluation of postconditions; it gets the same guarantees as with the synchronous semantics but projected into the future (a postcondition may be assumed to hold immediately after the execution of a feature's body although it may not hold at that point).

This semantics can be further refined to allow independent evaluation of postcondition clauses. In the above example, the state of tokyo is irrelevant for get result (york); it only becomes important later on, when get result (tokyo) is called. The client is only interested in the first postcondition clause involving york; if this clause holds, get result (york) proceeds without waiting for tokyo. This enables more parallelism, in particular if tokyo is much slower than york. Once again, the client is not penalised because it gets all the guarantees in due time. Definition 6 captures the new semantics of postconditions.

Definition 6 (Semantics of postconditions). A postcondition describes the result of a feature's application. Postconditions are evaluated asynchronously. Postcondition clauses that do not involve calls on targets handled by the same processors are evaluated independently.

Following Definition 5, in the call spawn two activities (york, tokyo), the postcondition clause post 1 is controlled whereas post 2 is uncontrolled. The client may assume the former (york.is ready) after the call because no other client can invalidate it; the latter clause (tokyo.is ready) cannot be assumed because of the possible interference by other clients. The situation is symmetric to the treatment of preconditions: a controlled precondition clause constitutes an obligation on the client; a controlled postcondition clause is a guarantee given to the client. We use this observation to derive a proof rule for feature calls in Sect. 7.

Each query call appearing in a postcondition clause is evaluated by its target's handler; the results of all the queries are combined into one boolean value (This operation is performed by a processor involved in the given clause. The implementation of SCOOP described in [START_REF] Nienaltowski | Practical framework for contract-based concurrent object-oriented programming[END_REF] picks the first processor in the order of appearance). The violation of a postcondition clause raises an exception in the processor that has executed the routine. This gives rise to the problem of asynchronous exceptions: the client's processor might have already left the context of the call, so the exception cannot be propagated correctly. This topic is beyond the scope of this article; see the exception handling mechanisms proposed by Arslan and Meyer [START_REF] Arslan | Asynchronous exceptions in concurrent object-oriented programming[END_REF], Brooke and Paige [START_REF] Brooke | Exceptions in Concurrent Eiffel[END_REF], and Adrian [START_REF] Adrian | SCOOP for SmallEiffel[END_REF].

We may observe how the semantics of postconditions reduces to the traditional sequential semantics if no concurrency is involved. Consider the call my x.r (my a) in Fig. 4. The client, the supplier my x, and the actual argument my a are handled by the same processor. The client cannot proceed to do local stuff until both postcondition clauses have been evaluated because the client's processor is in charge of evaluating them. As a result, either all the postcondition clauses hold immediately after the call or an exception is raised. Also, the client can assume all the postconditions of r because they are controlled. This corresponds to the sequential semantics.

Invariants

Invariants play an important role in the DbC methodology. They are the primary tool for ensuring the consistency of objects: an instance of class C is consistent if and only if it satisfies the invariant of C. The invariant must be satisfied in every observable state, i.e. in any state where the object may be accessed by a client.

The standard Eiffel semantics applies to class invariants in SCOOP because all the expressions appearing in invariants must be non-separate. There is no explicit rule prescribing it; however, the controllability requirement imposed by the new call validity rule [Nie07b, rule 6.5.3] can only be satisfied by non-separate entities because invariants have no enclosing routines. The invariant is checked before and after the application of a feature (unless the feature has been called using an unqualified form, i.e. with the Current object as the implicit target); an invariant violation raises an exception in the supplier.

Loop assertions and check instructions

We apply the asynchronous semantics to loop variants, loop invariants, and check instructions. 3 Wait by necessity does not apply: the evaluation of an assertion is blocking only if the current processor is involved, i.e. the assertion includes non-separate expressions. All loop variants, invariants, and check instructions are controlled because all the involved entities serving as targets of calls must be controlled; the call validity rule would be violated otherwise. Therefore, such assertions preserve their contractual character and may be used for formal reasoning. Similarly to postconditions, their asynchronous evaluation does not influence the reasoning style: they may be assumed to hold immediately. When a loop assertion or a check evaluates to False, an exception is raised.

Figure 5 illustrates the advantages brought by the asynchronous semantics. The assertions appearing in the body of remove n capture the essence of the loop: at each iteration, the number of elements in list is reduced, and the number of remaining elements plus the number of removed elements equals the initial number of elements. If the variant and invariant are to be evaluated, the evaluation will be asynchronous; the processor handling list is asked to evaluate them in due time, after the previous features targeting list but before the next application of remove. The request queue of list's handler may look like this:

P list : ...[list.remove][eval var ][eval inv ][list.remove][eval var ][eval inv ][list.remove]...
The client does not wait; it performs the next iteration of the loop, until the exit condition becomes true. Even if the handler of list is very slow, so that the application of remove or the evaluation of assertions takes a long time, the client may forsake waiting for the execution of remove n to terminate, and still rely on the guarantee that n elements will eventually be removed. (If the call to remove n occurs in a context where the actual argument is controlled then the postcondition is controlled and the client may assume it immediately after the call.) Even though the assertions involve separate calls, the correctness and the termination of the loop, as well as the establishment of the postcondition can be proved using the standard sequential reasoning. The new semantics maximises the amount of parallelism while preserving the sequential reasoning style.

Check instructions are treated in the same way as loop assertions; they are evaluated asynchronously in due time. For example, the following sequence of calls:

x.f; x.set i (10); check x.i 10 end; x.g results in checking x.i 10 after the application of x.set i (10) but before the application of x.g. The request queue of x's handler looks like that:

P x : ...[x.f ][x.set i(10)][eval x.i 10 ][x.g]...
The client is sure that x.i 10 is true before the application of x.g. Note the difference between this guarantee and the guarantee given by an explicit if instruction if x.i 10 then x.g else ... end Here, due to wait by necessity, the client is sure that x.i 10 holds before calling x.g. This is a stronger guarantee but it comes at the cost of reduced parallelism.

Towards a proof rule

The semantics of preconditions discussed in Sect. 3 implies that a client's responsibilities should be limited to establishing the controlled precondition clauses before the call; the uncontrolled ones may only be established by the environment, through the emergent behaviour of other processors. Similarly, the semantics of postconditions introduced in Sect. 4 lets clients assume controlled postcondition clauses after the call; the uncontrolled ones hold when the routine terminates but the client cannot assume them, due to the potential interference of other clients. We use this observation to define the mutual obligations of clients and suppliers, thus establishing the contractual character of assertions and capturing the essence of DbC in a general (potentially concurrent) context. Definition 7 (Mutual obligations of clients and suppliers). The supplier may assume all the precondition clauses at the entry to the feature's body; it must establish all postcondition clauses when the body terminates. The client must satisfy all the controlled precondition clauses at the moment of the call; it may assume all the controlled postcondition clauses after the call.

The above definition applies to synchronous and asynchronous calls but needs no temporal operators: sequential reasoning applies here. This is possible because controlled assertions may be projected into the future, i.e. assumed to hold immediately even if their evaluation is delayed. From the supplier's point of view, all the preconditions and postconditions are controlled; therefore, its obligations are the same as in a sequential context. The client, however, has fewer obligations; conversely, it gets fewer guarantees. The Hoare-style Rule 8 derived from the sequential proof rule for feature calls formalises Definition 7. There is no distinction between separate and non-separate assertions; both preserve their contractual character. Only controlled assertion clauses are considered by the client; hence the superscript ctr decorating them in the conclusion of the rule. From the point of view of the supplier, all assertions occurring in Pre r and Post r are controlled; therefore, all of them appear in the antecedent. The invariant must be fully controlled to avoid side effects: the call validity rule prohibits separate expressions, but expressions of the form q (x) must also be prohibited if x is separate; otherwise, the evaluation of INV might be blocking and subsequent evaluations might yield different results. The proof rule now becomes:

{INV ∧ Pre r } body r {INV ∧ Post r } {Pre ctr r [a/f ]} x.r(a) {Post ctr r [a/f ]} (8)
The following sequential-like proof technique for partial correctness of synchronous and asynchronous feature calls relies on the newly introduced proof rule.

Definition 9 (Proof technique for synchronous and asynchronous calls). Consider a call x.r(a). If we can prove that the body of r, started in a state satisfying the precondition, satisfies the postcondition if and when it terminates, then we can deduce the same property for the above call, with actual arguments a substituted for the corresponding formal arguments, every non-qualified call in the assertions (of the form some property) replaced by the corresponding property on x (of the form x.some property), and ignoring the uncontrolled assertions.

Our approach eliminates the need for a special treatment of asynchrony. It makes it possible to reason about sequences of asynchronous calls-or interleaved synchronous and asynchronous calls-without using temporal operators. For example, it is easy to demonstrate the correctness of the feature store three in Fig. 6 even though its body contains a sequence of separate calls. The precondition of the first call to buffer.put is implied by the precondition of store three. Its postcondition is assumed to hold immediately after the call; the postcondition implies the precondition of the second call to buffer.put. The postcondition of the second call -again assumed immediately after the call -implies the precondition of the third call to buffer.put. Finally, the postcondition of the third call implies the postcondition of store three. This technique is modular: the proof of store three relies on the contract of {BUFFER}.put; once we have proved the correctness of store three, its contract can be used for proving the correctness of routines that call store three, and so on.

Discussion

Limitations of the proof technique

Rule 8 is strong enough to prove partial correctness of programs; certain liveness properties, such as loop termination, can also be proved. Total correctness, however, cannot be proved because of the potential deadlocks Fig. 6. Assertional reasoning about asynchronous calls and infinite waiting on non-satisfied uncontrolled preconditions. Recall the York-Tokyo example from Fig. 3. The calls spawn two activities (york, tokyo), get result (york), and get result (tokyo) happen in a context where york is controlled but tokyo is not. Therefore, all assertion clauses involving tokyo are uncontrolled; the proof rule ignores them. Assume that the feature get result is defined as get result (location: separate LOCATION) require location.is ready ensure location.result retrieved and the postcondition of do local stuff is empty. The proof sketch for the routine r in Fig. 7 demonstrates that reasoning about york's properties is not hindered: the client has to establish the precondition of get result (york) using the postcondition of spawn two actitivies; it can prove the postcondition of r using the postcondition of get result (york). The establishment of the precondition clauses involving tokyo is beyond the client's control: the client does not need to prove anything about tokyo but is not even sure whether the calls involving tokyo will ever proceed. The first possibility is that tokyo's handler is never released by its current client; both calls spawn two activities (york, tokyo) and get result (tokyo) may block for that reason.

The second possibility is that tokyo becomes available but its state never satisfies the precondition (this may only happen for get result (tokyo) because it has a non-trivial precondition). As a result, the total correctness of r cannot be proved without considering the behaviour of the whole system; but this requires global reasoning and the use of temporal operators to express such properties as "tokyo will eventually become available in a state satisfying tokyo.is ready". Alternatively, Rely/Guarantee specifications [Jon81, MC81, Jon03] can be used to reason about the influence of the environment. Ostroff et al. [START_REF] Ostroff | Beyond contracts for concurrency[END_REF] propose a technique to deal with properties of uncontrolled targets and introduce the concept of a controlled routine to define contexts in which our proof rule can be used to reason about total correctness of feature calls.

Contract redefinition

The proposed semantics of contracts and the proof technique are sound in the presence of polymorphism and dynamic binding; clients are not deceived even if contracts are redefined. The standard DbC rules apply: preconditions may be kept or weakened; postconditions and invariants may be kept or strengthened. A redefined precondition results in fewer obligations on the client and (potentially) less waiting at the moment of the feature

Importance of lock passing

The proof technique proposed here assumes the semantics of argument passing enriched with the lock passing mechanism introduced in [Nie07a, Nie07b]: if a feature call x.f (a 1 , ..., a n ) occurs in the context of the routine r where some actual argument a i is controlled, i.e. a i is attached and locked by the processor executing r, and the corresponding formal argument of f is declared as attached, the client's handler (the processor executing r) passes all currently held locks (including the implicit lock on itself) to the handler of x, and waits until f has terminated; when the execution of f is complete, the client's handler resumes the computation. Indeed, the proof technique would not be sound without the above mechanism. Consider the proof sketch in Fig. 8. The call x.transfer to (y) is processed synchronously because y is controlled; therefore, lock passing occurs at the moment of the call. Any calls on y within the body of transfer to are guaranteed to be executed before the subsequent call to y.empty issued by the client. Therefore, the postcondition of transfer to may be assumed before the call y.empty; it is necessary to prove the correctness of that call (and the whole routine s). If no lock passing occurred (as in SCOOP 97), the call y.empty would be processed before the calls issued by the body of transfer to; the assumption y.is full would be false and the call y.empty invalidated. In fact, following SCOOP 97 rules, x would be able to execute transfer to only after the client terminated s and unlocked y; therefore, y.is full would eventually become true, which contradicts the promise made by s: its postcondition says that y is empty. See [START_REF] Nienaltowski | Practical framework for contract-based concurrent object-oriented programming[END_REF] for a more detailed discussion of lock passing and related issues.

Run-time assertion checking

Meyer [START_REF] Meyer | Object-oriented software construction[END_REF] mentions the problem of run-time assertion checking in a concurrent context, concluding: "The assertions are an integral part of the software, whether or not they are enabled at run time. Because in a correct sequential system the assertions will always hold, we may turn off assertion checking for efficiency if we think we have removed all the bugs; but conceptually the assertions are still there. With concurrency the only difference is that certain assertions -the separate precondition clauses -may be violated at run time even for a correct system, and serve as wait conditions. So the assertion monitoring options must not apply to these clauses."

In fact, assertion monitoring may be turned off even for wait conditions. Since the client is responsible for establishing the controlled precondition clauses, the runtime checks of such preconditions are not necessary, provided that the calls have been proved correct (or, at least, we are convinced that they are correct). Uncontrolled precondition clauses must be monitored; but even here some optimisations are possible. If an uncontrolled precondition clause holds whenever the feature is applied-for example the clause follows from the class invariant, or maybe it requires some (monotonic) property that has already been established by an earlier call-then there is no point in re-checking the clause every time; we know that it holds.

This reveals another advantage of the new semantics of postconditions, checks, and loop assertions: the run-time monitoring of assertions has no impact on the semantics of correct programs (except for the incurred overhead). With the traditional sequential semantics, wait by necessity forces the client to wait for the evaluation of an assertion if the run-time checking is on but no waiting happens when it is turned off; the program's behaviour changes. Our semantics eliminates such inconsistencies.

Related work

Ostroff et al. [START_REF] Ostroff | Beyond contracts for concurrency[END_REF] show that contracts provide only a certain measure of correctness but do not guarantee additional safety and liveness properties without global reasoning. They model SCOOP programs as fair transition systems [START_REF] Manna | Temporal verification of reactive systems: safety[END_REF] and use temporal logic for describing and proving system properties beyond contractual correctness. This approach is complementary to ours: it permits expressing and proving properties of uncontrolled targets which cannot be captured by our proof rules.

Bailly [START_REF] Bailly | Formal semantics and proof system for SCOOP[END_REF] assumes a different semantics of separate preconditions: they are merely guards of conditional critical regions represented by routine bodies. Guards are excluded from contracts and treated separately from the traditional (correctness) preconditions. The approach does not support inheritance, therefore it does not address problems caused by guard strengthening vs. precondition weakening. The treatment of postconditions is identical as in the sequential context, although the author comments on the infeasibility of formal reasoning with the sequential proof rule. Other concurrent extensions of Eiffel, such as CEiffel [L öh92], CEE [START_REF] Jalloul | Concurrent object-oriented systems: a disciplined approach[END_REF], and Distributed Eiffel [START_REF] Gunaseelan | Distributed eiffel: a language for programming multigranular objects[END_REF] rely on guard-based synchronisation with a syntactic distinction between guards and preconditions. The distinction between guards and preconditions has deep implications for formal reasoning: clients need to satisfy preconditions but not guards; in the context of polymorphism, guards can be strengthened whereas preconditions can only be kept or weakened.

Sutton [START_REF] Sutton | Preconditions, postconditions, and provisional execution in software processes[END_REF] describes a new strategy for condition-based process execution, based on delayed evaluation of preconditions and postconditions. Preconditions have guard semantics but they are evaluated in parallel with task (routine) bodies; a task might be allowed to execute even if some of its preconditions have not yet been evaluated. They only have to hold at a particular point of execution; otherwise, the task is put on hold or cancelled. The task may terminate even if some of its postconditions have not been established. They have to be established eventually; otherwise, the task must be cancelled (rolled back or compensated). This semantics is similar to ours: postconditions are also projected into the future. The precondition semantics proposed by Sutton may be simulated in our model by splitting up a routine into smaller subroutines which require their preconditions to hold on entry to their bodies.

Rodriguez et al. [RDF + 05] propose a concurrent extension of JML whereby method guards are treated in a similar way to Sutton's preconditions. Guards are specified using the keyword when and appear in a feature header, after the preconditions. If a feature is called in a state where its guard does not hold, it should block until the guard is satisfied. Interestingly, the guard does not need to hold at the beginning of the body but only at a point marked with a special statement label commit; if no commit point is specified, it is assumed to be at the end of the body. There is no implicit waiting mechanism; programmers must write synchronisation code by hand, for example using busy-waiting loops. The approach facilitates static verification of atomicity properties but it does not simplify the construction of concurrent programs.

Conclusions

We have outlined a new semantic approach to contracts-routine preconditions and postconditions, loop variants and invariants, and check instructions-which lifts the principles of Design by Contract from purely sequential programming to the concurrent context, while remaining applicable to sequential object-oriented programs. Preconditions become wait conditions; separate postcondition clauses earn an asynchronous semantics and are evaluated independently from other postcondition clauses. Similarly, loop assertions and check instructions are evaluated asynchronously. The resulting programming model makes it possible to exploit the potential for parallelism while preserving the intuitive meaning of contracts as a way to express the mutual obligations of clients and suppliers. We have argued that the proposed semantics is indeed a generalisation of the traditional sequential semantics: they are equivalent when no concurrency is involved. The contract semantics presented here is supported by the current implementation of SCOOP, available for download at http://se.ethz.ch/research/ scoop.html.

We have also proposed a proof technique for reasoning about safety properties of object-oriented concurrent programs. It builds upon the new contract semantics and the Hoare-style rule for feature calls which permits guarantees expressed in assertions to be projected into the future. As a result, it becomes possible to treat synchronous and asynchronous calls in a similar way; this greatly reduces the complexity of reasoning formally about concurrent code.

Our treatment of contracts and the proof technique are compatible with such essential object-oriented mechanisms as inheritance, polymorphism, and dynamic binding.

306P.

  Nienaltowski et al.

Fig. 1 .

 1 Fig. 1. Preconditions in a concurrent context

Fig. 2 .

 2 Fig. 2. Controlled and uncontrolled preconditions clauses

Fig. 3 .

 3 Fig. 3. Postconditions in a concurrent context

Fig. 4 .

 4 Fig. 4. New postcondition semantics in a sequential context

Fig. 5 .

 5 Fig. 5. Loop assertions in a concurrent context

Fig. 7 .

 7 Fig. 7. Limitations of the proof technique

Fig. 8 .

 8 Fig. 8. Interplay of lock passing and contracts

An expanded target represents an object rather than a reference to an object; expanded targets are always non-separate.

Check instructions are similar to assert statements in Spec[START_REF] Barnett | The Spec programming system: an overview[END_REF] and JML/Java [LPC + 05].

Acknowledgments

We would like to thank the FACJ referees and CORDIE'06 participants for their comments on earlier versions of this article. We are also grateful to Peter M üller for important feedback on the proof technique as well as to Volkan Arslan and many ETH students for numerous comments and discussions on the model and its implementation. This research work was conducted during the first author's PhD studies at the ETH Zurich. We are grateful for the generous support of the Hasler Foundation as part of its DICS project on Dependable Information and Communication Systems [AENV06] (DICS project number 1834), and of the Swiss National Science Foundation (FNS project number 200021-100498/1).


Wolfgang Schreiner
email: wolfgang.schreiner@risc.uni-linz.ac.at

A Duce

J Oliveira

P Boca

R Boute

Formal Aspects of Computing The RISC ProofNavigator: a proving assistant for program verification in the classroom

Keywords: Interactive proving assistants, Computer-aided verification, Teaching formal methods

This paper gives an overview of the RISC ProofNavigator, an interactive proving assistant for the area of program verification. The assistant combines the user-guided top-down decomposition of proofs with the automatic simplification and closing of proof states by an external satisfiability solver. The software exhibits a modern graphical user interface which has been developed with a focus on simplicity in order to make the software suitable for educational scenarios. Nevertheless, some use cases of a certain level of complexity demonstrate that it may be also appropriate for various realistic applications.

Introduction

Formal methods [START_REF] Huth | Logic in computer science-modelling and reasoning about systems[END_REF] become more and more visible in computer science curricula, but typically for the purpose of modeling hardware and software systems rather than for actually reasoning about them. Lecturers tend to shy away from performing formal proofs of system properties in the classroom such that most software engineers enter the market without ever having attempted such proofs. This perpetuates the general opinion that the only value of formal methods (if any) is in areas where fully automatic tools hide the underlying theory (e.g. the model checking of finite state systems). That the act of formal reasoning on certain aspects of a system may actually help to gain insight into the system is completely neglected.

One major reason that the aspect of proving is underrated in computer science curricula is that manual system proofs are complex, error-prone, and hardly ever convincing. However, in the last two decades, a variety of powerful automatic theorem provers and interactive proving assistants have become available many of which can be also applied to the area of program and system verification [START_REF]The seventeen provers of the world[END_REF]. For instance, the prototype verification system PVS [START_REF] Owre | PVS: a prototype verification system[END_REF] is an integrated specification and verification environment based on higher order logic. Isabelle [START_REF] Nipkow | Isabelle/HOL-a proof assistant for higher-order logic[END_REF] is a generic proving environment into which various logics can be embedded; the most widely used variant is Isabelle/HOL which uses higher order logic. Coq [START_REF] Bertot | Interactive theorem proving and program development-Coq'Art: the calculus of inductive constructions[END_REF] is based on the calculus of constructions; from proofs in Coq, programs can be extracted. ACL2 [START_REF] Kaufmann | Computer-aided reasoning: an approach[END_REF] is the latest incarnation of the Boyer-Moore family of provers based on a first-order logic of total recursive functions. Theorema [BCJ + 06] is a system that generates human-readable automatic proofs by a combination of a higher-order predicate logic prover and a collection of special provers. Also CASE tools have been augmented by capabilities for formal specification and verification: the KeY tool [START_REF]Verification of object-oriented software: the KeY Approach[END_REF] for the development of JavaCard programs includes a proving assistant for first-order dynamic logic; Perfect Developer is a commercial object-oriented development tool that includes a fully automatic theorem prover [START_REF] Carter | Software refinement with perfect developer[END_REF].

Correspondence and offprint requests to: W. Schreiner, E-mail: Wolfgang.Schreiner@risc.uni-linz.ac.at While thus a variety of tools for supporting reasoning are around, the available budget of teaching time is frequently considered too small to introduce students to their practical use. Indeed, while more and more effort is also put into the user interface aspects of such systems [A + 05, AC03], it has to be admitted that many of them are difficult to learn and/or inconvenient to use, which makes them less suitable for classroom scenarios [START_REF] Feinerer | Formal program verification: a comparison of selected tools and their theoretical foundations[END_REF]. We (the author) had the same experience when we evaluated from 2004 to 2005 a couple of prominent proving assistants by a number of use cases derived from the area of program verification. While we achieved quite good results with PVS, we generally encountered various problems and nuisances, especially with navigation within proofs, the presentation of proof states, the treatment of arithmetic, and the general interaction of the user with the systems; we frequently found that the elaboration of proofs was more difficult than we considered necessary. Without any doubt, some of these problems were caused by our own inabilities and could have been overcome by more training and experience but this is exactly the hurdle for the more wide-spread application of this kind of software.

From these experiments, we drew a couple of important conclusions for the pragmatics of using a proving assistant in program verification (in the classroom and elsewhere):

• The presentation of a proof as a tree of all proving states (as opposed to the presentation as a flat list of only the open proving tasks) is crucial to keep track of the overall situation; correspondingly, facilities for convenient navigation in proof trees are essential. • The aggressive simplification of proof state descriptions and their comfortable presentation (in particular an adequate layout of large formulas) is important; the user quickly loses intuition about the interpretation of a proof situation. • Decent automation in dealing with arithmetic is important; furthermore, a subtype relationship between integers and reals (rather than explicit conversion functions between the two domains) simplifies some proofs considerably.

• Automatic search for proofs based on elaborate strategies is rarely of much help; typically it is the combination of semi-automatic proof decomposition, critical hints given by the user, and the application of decision procedures for ground theories that shows practical success.

Based on these considerations we decided to write a proving assistant to meet above criteria (with various features copied from PVS and adapted to our taste). We reckoned that this task would become possible with reasonable effort by making use of existing software that decides about the satisfiability of formulas over certain combinations of ground theories. During the last couple of years, various tools for solving this SMT (satisfiability modulo theories) problem have emerged [START_REF]SMT-LIB-the satisfiability modulo theories library[END_REF]. Around one such tool, the Cooperating Validity Checker Lite (CVCL) [START_REF] Barrett | CVC Lite: a new implementation of the cooperating validity checker[END_REF], we finally developed the RISC ProofNavigator [START_REF] Schreiner | The RISC ProofNavigator-tutorial and manual[END_REF], a proving assistant which should be suitable as well in educational as in real application scenarios. The software is implemented in Java, runs on GNU/Linux computers with x86-compatible processors, and is freely available as open source [START_REF]Research Institute for Symbolic Computation (RISC)[END_REF].

The remainder of this paper is structured as follows: in Sect. 2, we describe the system's user interface and the corresponding design considerations; Sect. 3 sketches the implementation of the system; Sect. 4 presents the specification language and proof logic; Sect. 5 walks through an example verification; Sect. 6 surveys the application of the software to various use cases; Sect. 7 concludes and gives an outlook on further development.

This paper is a substantial revision and extension of [Sch06a] from which the verification example presented in Sect. 5 is taken.

The user interface

When the RISC ProofNavigator is started, a window pops up that displays three major areas (see Figure 1):

Proof tree This area illustrates the skeleton structure of the proof which is currently investigated. It mainly serves for easy navigation: a click on a tree node displays the corresponding proof state; a double click switches to that state in order to apply a proof command. Proof state Initially this area displays the declarations entered by the user (respectively read from a file) in a pretty-printed form which closely resembles the usual mathematical notation (the output window below shows a corresponding plain text notation). When a proof is started, this area displays the proof state which is currently investigated. Input/output This area consists of an input field where the user may type in declarations and commands and an output field where the effect of the user input is shown as plain text. The user may directly type in a command or select it from a menu as a template with gaps for the individual arguments: by pressing the tabulator button, the user jumps from one gap to the next to enter the necessary data.

Furthermore, there is a row of buttons that serve two purposes:

Proof navigation The buttons ("previous open state"), ("next open state"), ("undo command"), ("redo command") allow circling through the list of open proof states, undoing the effect of a proof command (thus discarding a subtree) and restoring a discarded proof tree again. Proof control The other buttons give the user access to the most important high-level strategies for decomposing a proof and/or closing a proof state. For instance, the button ("scatter state") recursively applies logical decomposition rules such as "∀-introduction", "∧-introduction", etc. to the current proof state and to all generated child states and also attempts to close the generated states by the application of the underlying satisfiability solver. Less aggressive decomposition strategies are applied by the buttons ("decompose state") and ("split state"); the buttons ("close state by automatic instantiation of formulas") and

("apply formula instantiation also to sibling states") apply heuristics for the instantiations of universally quantified assumptions respectively existentially quantified goals. By pressing the button , a menu of all available proof commands is displayed. Finally, by moving the mouse cursors over the label attached to a formula, a menu pops up that displays commands that may be applied in the current proof state and relate to that formula (e.g. to use a disjunctive assumption to split a proof state into multiple child states).

The button icons for proof control were chosen to visually resemble their effects, for instance the icon ("decompose state") is expended to expand the proof tree "downwards" (towards the leaves) in a limited fashion, while ("scatter state") expands the proof tree until no further automatic expansion is possible. Correspondingly, ("close state by automatic instantiation of formulas") is intended to "refresh" the view of a proof state and ("apply formula instantiation also to sibling states") "cleans up" a sequence of proof states. All buttons are equipped with explanatory popup menus such that their meaning should become quickly apparent also to new users.

The user interface was deliberately designed with various goals in mind:

Maximize survey The user should easily keep a general view on proofs with many states; she should also easily keep control on proof states with large numbers of potentially large formulas. These purposes are served by the proof tree area and by the pretty-printing of formulas with appropriate indentations. Furthermore, before presentation every proof state is forwarded to a decision/simplification procedure; only if it cannot be automatically closed, it is displayed after simplification by logical and arithmetic transformations.

Minimize options

The number of commands is deliberately kept as small as possible in order to minimize confusion and simplify the learning process (in total there are about thirty commands, of which only twenty are actually proving commands; in typical proofs, less than ten commands need to be used). In particular, there are only commands to control the predicate-logic structure of a proof; reasoning on the level of terms and arithmetic is completely left to the underlying satisfiability solver (which decides linear integer arithmetic; non-linear arithmetic properties can be introduced as lemmas and subsequently verified by induction).

Minimize efforts

The most important commands can be triggered by buttons or by menu entries attached to formula labels. The keyboard only needs to be used in order to enter terms for specific instantiations of universal assumptions or existential goals (but even here typing effort is minimized by the selection of command "templates" from menus).

Formulas are presented in a visually appealing mathematical form (in the proof state area) as well as in a linear textual form (in the output area); the later form on the one hand uniquely exhibits the logical structure of a formula (which is useful if uncertainties arise) and on the other hand is convenient for copying and pasting formulas and terms into the input area (e.g. for the instantiation of a quantified formula). Every formula is tagged with a label of the form [xyz ] where xyz are three characters derived from hashing the text of the formula (after a canonical renaming of the variables bound in the formula); this allows references to be made to formulas independent of their positions in a proof state, which makes proofs whose commands refer to specific formulas more robust against changes in definitions (compared to systems such as PVS or Isabelle where commands depend on the ordering of formulas and even minor changes in definitions subsequently break proofs).

We believe that after a short learning period the interface becomes very transparent such that the user can concentrate on the mathematical aspects of a proof rather than on handling the software. By convenient navigation and undo/redo mechanisms one can quickly browse through a proof and experiment with different proving strategies.

The software architecture

The RISC ProofNavigator has been entirely implemented with free software. It consists of the following components (see Fig. 2):

The graphical user interface The GUI is written in Java with the use of the Eclipse Standard Widget Toolkit (SWT) and embeds the Mozilla browser as a component for the presentation of declarations and proofs. User interactions in the browser component (selections of menu entries) are forwarded as HTTP requests to a thread that acts as an HTTP server and triggers the corresponding activity in the ProofNavigator kernel. The ProofNavigator kernel The kernel of the system is written in Java; it includes parsers generated with ANTLR for processing the Proof Navigator specification language and the output of the CVCL software. Using the Java Document Object Model (DOM) interface, it generates external representations of declarations and proofs that remain persistent across sessions. The cooperating validity checker (CVCL) CVCL is written in C++; instances of the software are incorporated as external processes that interact with the kernel via their standard input/output interfaces. One instance is created for simplifying user declarations and one instance is created for the simplification of every proof state. Presentation The kernel generates XHTML documents which embed MathML expressions for the presentation of declarations and proofs by the GUI's browser component. These documents are appropriately hyper-linked and pertained across sessions such that they can be used for presentation in the Web by standard-compliant browsers (such as the browsers of the Mozilla suite). Session store Declarations are stored for use in later sessions as (compressed) OMDoc documents [START_REF] Kohlhase | OMDoc-an open markup format for mathematical documents (version 1.2)[END_REF] embedding the XML representations of OpenMath objects [START_REF]The OpenMath standard. Version 2.0[END_REF] denoting types, functions, and predicates; these documents may thus in principle be processed by other OMDoc-compliant tools. Likewise, proof trees are stored for later replay in an XML representation where for every node of the tree (only) the proof command issued in the corresponding proof situation is stored; the representation is ad-hoc because OMDoc does not support a notion of proofs suitable for our purpose. For details on the representation formats, see the manual [START_REF] Schreiner | The RISC ProofNavigator-tutorial and manual[END_REF].

The session store maintains the dependencies among declarations and proofs as well as the status of every proof as "open" or "completed". If a new session is started, the dependencies are used to re-assess the status of every proof: if the proof only depends on declarations whose dependencies have not changed, its status is tagged as "trusted"; if however, some dependency (e.g. the declaration of a formula on which the proof depends) has changed, its status is tagged as "untrusted" indicating that the stored proof should be replayed to re-establish its trust level.

The explicit maintenance of proofs is very important, because the proof development process typically requires continuous modifications of definitions and thus more than one proving session; nevertheless it is (with the major exception of PVS) not supported by most other assistants.

If an untrusted proof is replayed from its representation in the session store, the kernel traverses the proof tree and executes the proving commands indicated by the nodes of the tree. If a proving command fails, the proof replay suspends in the denoted proof situation and prompts the user for help. The user has now the chance to abort the proof situation (i.e. the original subtree rooted in that node is discarded and the replay continues with the other nodes) or to provide a substitution command with which the replay attempts to continue the proof (as if no error had occurred). This possibility is rather important in those cases where the replay has only failed because of some minor change (such as the label of a formula referenced in a proof command) but the proof remains structurally intact; while in PVS the user has to construct the corresponding proof subtree again from scratch, it can with little effort be recovered in the RISC ProofNavigator.

The specification language and proof logic

The RISC ProofNavigator uses a language in the style of PVS respectively CVCL for the specification of types, constants, functions, predicates, axioms, and ultimately formulas to be proved. The language is based on a higherorder logic and includes boolean values, integer numbers, real numbers, tuples, functions, arrays, and records as basic datatypes respectively type constructors. The language also supports subtypes, i.e., types that are defined as those elements of some other type that satisfy some (user-defined) condition. Type checking is based on a combination of static type checking for the basic types and the verification of automatically generated type checking conditions for the subtypes.

The full language is described in the manual [START_REF] Schreiner | The RISC ProofNavigator-tutorial and manual[END_REF]. As an illustrative example, we define a datatype "finitelength arrays" with corresponding constructor and selector operations. Every element of this datatype is a tuple of a function that maps the natural numbers to array values (based on the internal notion of arrays as unary functions) and a natural number that denotes the length of the array (and thus constrains the range of indices to which the function may be applied). The corresponding type declarations are

INDEX: TYPE = NAT; ELEM: TYPE; ARR: TYPE = [INDEX, ARRAY INDEX OF ELEM];

We then introduce various auxiliary constants whose values remain undefined and that serve in the later declarations as error signals: The value of this constant is the function that, given an argument a of type ARR, returns its second component a.1, i.e. the content of the array (the notation a.i denotes component i of tuple a; components are numbered starting with 0). With the help of these auxiliary notions, we define our core functions on arrays: The adequacy of these definitions is stated by the declarations of the following formulas which say that the functions satisfy the classical properties required from arrays: These declarations are pretty-printed by the RISC ProofNavigator as shown in Figure 3. To start the proof of e.g. formula get2, we may either enter the command prove get2 or simply select this command from the menu hidden behind the label of this formula. This yields the initial proof state

The presentation of the proof state consists of the value constants visible in the state and of two sequences of labelled formulas separated by a horizontal line: the assumptions and the goals (initially there are no assumptions and a single goal [vvg] which represents the formula get2 to be proved). The logical interpretation of this presentation is that of a Gentzen-style sequent [START_REF] Gallier | Logic for computer science-foundations of automatic theorem proving[END_REF] A 1 , . . . , A n B 1 , . . . , B m with assumptions A 1 , . . . , A n and goals B 1 , . . . , B m . This sequent can be viewed as the task to prove the validity of the formula

A 1 ∧ . . . ∧ A n ⇒ B 1 ∨ . . . ∨ B m
i.e. that the conjunction of the assumptions logically implies the disjunction of the goals. This is in particular achieved, if it can shown that some of the assumptions are false or some of the goals are true.

Proofs are constructed by the application of a rule to the current proof state such that the system

• Either recognizes the current state to denote a valid formula (in the sense described above),

• or a set of child states are generated such that the validity of the formulas denoted by these states implies the validity of the formula denoted by the current state.

By recursive rule application, a proof tree is constructed; the proof is completed, if all leaves of the tree are recognized to denote valid formulas.

Since

A 1 ∧ A 2 ⇒ B 1 ∨ B 2 is logically equivalent to A 1 ∧ A 2 ∧ ¬B 1 ⇒ B 2
, by negation every formula can be switched from the list of goals to the list of assumptions and vice versa. PVS applies this property to avoid a negation symbol at the outermost level of every formula in proof state presentations by automatically presenting it as an assumption or as a goal. We found this automation quite disturbing, because the user typically focuses on a particular formula as the goal to be proved and considers all others (negated or not) as corresponding assumptions; likewise, in a proof by contradiction, all formulas are considered as assumptions whose conjunction is shown to be inconsistent. Furthermore, to have more than one goal formula hardly corresponds to any user intuition at all.

The proving rules of the RISC ProofNavigator are therefore designed to generate a single goal formula (multiple goal formulas are still supported but only arise from the explicit manipulation of the proof state by the user, see below). Moreover, some rules treat the goal formula specially, e.g. the command scatter restricts the branching of the proof tree by applying those rules that may generate several child states only to the goal formula, not to any of the assumptions. The user may always choose to change her focus by explicitly "flipping" formulas between the list of assumptions and the list of goals and thus control further elaboration of the proof. The automatic proof state simplification always draws negations into formulas such that e.g. a universal assumption becomes an existential goal and vice versa (while such formulas are logically equivalent, they actually represent rather different user intuitions).

Returning to above example, the root of the tree is the state labelled [adu] which consists of a single goal [vv6] representing the content of formula get2. To expand all occurrences of the defined constants to their values in this proof state, we apply the command expand length, get, put, content; which yields a single child state [c3b] of the following form:

The state has a single goal [d5q] which is the result of the expansion of all constants in the parent's goal [vv6]. Our next task is to simplify the proof state by eliminating the universal quantifier and of the logical connectives in the goal. The simplest way to achieve this is by pressing the "Scatter State" button which applies various proving rules in order to scatter the current state to a number of simpler ones. This yields the following dialog which indicates that the remainder of the proof has been automatically completed and that the system has returned to declaration mode:

Proof state [qid] is closed by decision procedure. Formula get2 is proved. QED. Save this proof and overwrite the previous one (y/n)? y Proof saved (browse file get2_index.xhtml). Quit proof of formula get2 (use 'proof get2' to see proof).

By selecting the command proof get2 from the menu of formula get2, we see the structure of the generated proof:

From state [c3b] a single child state was generated that was automatically proved by the external decision procedure CVCL. Clicking on the corresponding node in the tree displays the state as follows:

The state has four new constants a 0 , i 0 , j 0 , and e 0 that replace the bound variables of the universally quantified goal [d5q] in the parent state. The resulting goal without quantifier was decomposed into three atomic formulas as assumptions and a single atomic formula (the equality of two conditional expressions) as a goal. This proof state was automatically closed by the decision procedure; for a human, the corresponding reasoning steps are (although not really difficult) tedious and error-prone.

This small example already illustrates a general strategy of how to work with the system: to decompose a proof and get rid of quantifiers until sufficient low-level knowledge in the form of atomic predicates is available such that a decision procedure can automatically close the proof state. The task of the human (and the difficulty in real-world proofs) is to expose this low-level knowledge by guiding the overall proof construction; the task of the system is to make this process as painless as possible and to take over (via an external decision procedure) low-level reasoning on builtin datatypes.

A program verification

In this section, we are going to demonstrate the use of the RISC ProofNavigator for the verification of a Hoare triple [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. The triple represents the core of a program which searches in an array a for the smallest index r at which an element x is stored:

{olda a ∧ old x x ∧ n | a | ∧i 0 ∧ r -1} while i < n ∧ r -1 do if a[i ] x then r : i else i : i + 1 {a olda ∧ x old x ∧ ((r -1 ∧ ∀ i : 0 ≤ i <| a |⇒ a[i ] x ) ∨ (0 ≤ r <| a | ∧a[r ] x ∧ ∀ i : 0 ≤ i < r ⇒ a[i ] x ))}
By the rules of the Hoare calculus, the verification of this triple is reduced to the proof of four verification conditions. The condition that is most difficult to prove is

I nvariant ∧ ¬(i < n ∧ r -1) ⇒ Out put
where Out put represents the postcondition of the above triple and I nvariant is a suitable loop invariant:

Out put :⇔ a olda ∧ x old x ∧ ((r -1 ∧ ∀ i : 0 ≤ i < length(a) ⇒ a[i ] x ) ∨ (0 ≤ r < length(a) ∧ a[r ] x ∧ ∀ i : 0 ≤ i < r ⇒ a[i ] x )) I nvariant :⇔ olda a ∧ old x x ∧ n length(a) ∧ 0 ≤ i ≤ n ∧ ∀ j : 0 ≤ j < i ⇒ a[j ] x ∧ (r -1 ∨ (r i ∧ i < n ∧ a[r ] x ))
We are now going to elaborate the proof of the verification condition; this proof will ultimately have the following tree structure:

This tree has seven inner nodes representing invocations of the commands expand, scatter, auto, and split by the user; it has five leaf nodes which were automatically closed by the satisfiability solver CVCL. The root state [dca] has goal [zfg] with occurrences of the predicates Invariant and Output.

We use the command expand Invariant, Output in zfg to replace these predicates by their definitions, which results in the following state: However, pressing the "Auto" button in this state also has no effect, thus we press the "Redo" button to return to the parent state [ecu]. Since we still do not know how to proceed, we attempt the "Counterexample" button which annotates the proof state with a "counterexample", i.e. an interpretation of the constants which might invalidate the proof state:

Apart from some trivial equalities following from the constant definitions and proof state assumptions, the counterexample includes the formula r -1 (denoting the condition "element not found" in the program being verified); this lets us suspect that its truth might be of importance. Investigating the proof state further, we realize that it contains three assumptions that start with r -1. Our further reasoning depends on the fact whether this formula is true, i.e. we have to perform a corresponding case distinction. We may trigger this distinction by the command case r -1 or, more easily, by selecting from the menu of the formula [pkg] the command split pkg which generates two child states each of which receives one component of the disjunction as an additional assumption. From the resulting two child states one is automatically closed while the other with label [lel] still requires our attention:

This state has an existential assumption [1bb]. To get rid of the quantifier, we press the "Scatter" button and get the state [lvn]:

This state contains a universally quantified assumption [564]; we try its instantiation with the "Auto" button . Indeed, a proof state [lap] is generated which is automatically closed such that the proof is completed.

Application

As mentioned in the introduction, the development of the RISC ProofNavigator has been triggered by the investigation of a number of use cases; the corresponding proofs are included in the distribution of the software. These proofs cover the following scenarios (the names set in teletype denote the corresponding subdirectories in the distribution).

1. Induction proofs: sum and sum0. 2. Quantifier proofs: quant and quant0. 3. Proofs based on axiomatization of arrays: arrays1. 4. Proofs based on constructive definition of arrays: arrays2. 5. Verification of linear search: linsearch. 6. Verification of binary search: binarysearch. 7. Verification of a concurrent system of one server and 2 clients: clientServer. 8. Verification of a concurrent system of one server and N clients: clientServerN.

Use cases 1 and 2 illustrate basic features of the system. Use case 3 gives an axiomatic definition of the datatype "array" and a proof of a fundamental array property (which becomes a bit complicated because the RISC Proof-Navigator does not yet support rewriting as a proving strategy). Use cases 4-8 describe sample verifications that are suitable for classroom presentation. While use case 4 (sketched in this paper) only needs simple linear integer arithmetic, use case 5 already combines integer arithmetic with rational arithmetic and involves an axiomatization of the "floor" function mapping rationals to integers. Use cases 6 and 7 describe the verification of a mutual exclusion property of a concurrent system based on a suitable system invariant. The last two examples generate proofs that consist of some hundreds of proof states (most of which are closed automatically, the user only has to apply about two dozen commands).

With various other proving assistants, we personally got stuck somewhere between use cases 5 and 6 (which dealt for the first time with not completely trivial arithmetic properties). Only with PVS were we able to comfortably prove these use cases and also (with major effort involving several hundreds of user interactions) use case 7; the proof of use case 8 was only attempted with the RISC ProofNavigator. Compared to the corresponding PVS proofs, with the RISC ProofNavigator the proofs of use cases 7 and 8 were actually quite simple and regular; when we had devised the overall proof decomposition, the system was able to prove most of the several hundreds of proof states automatically by heuristic instantiation of quantified formulas (where PVS had substantial problems).

The use cases are definitely not sufficient to qualify the RISC ProofNavigator as an industrial-strength proving assistant (as PVS certainly is). However, they demonstrate the practical usability of the software for a limited set of scenarios that are in particular typical for the use in courses on formal methods and program verification. We believe that its carefully designed interaction facilities substantially flatten the learning curve such that quicker success can be achieved within a limited time frame. Moreover, as demonstrated by some of the use cases, the software does not immediately bow to more complicated verifications and might therefore also be usable for limited non-classroom use.

As for actual classroom use, the software has been applied for the first time in the summer semester 2007 by a course on "Formal Methods in Software Development" [START_REF]Formal Methods for Software Development[END_REF] (a regular course for students of the master studies "Software Engineering" and "Computer Mathematics" of the Johannes Kepler University Linz, Austria) replacing the previously used PVS for proving verification conditions of sequential and concurrent programs. We first introduced the software by performing sample verifications in the classroom and then gave the students similar home exercises in deriving verification conditions and proving them on their own with the help of the software.

There were virtually no complaints about the software and only a few suggestions for improvement (such as the possibility to re-open already closed proof states) which we will take into account in the next version. Compared to the previous use of PVS, students seemed to get effective with the software in a shorter period; most students were quickly able to work with it and perform the verifications essentially as expected. Sometimes, however, the proofs were considerably more complicated than necessary because critical information (manual instantiations of quantified formulas or new lemmas) was not introduced early enough (close to the root of the proof tree) such that later automatic instantiations were not effective in closing proof states in the various proof branches. This is a point which certainly requires further experience and training.

Independently, the RISC ProofNavigator is at the time of writing this paper (September 2007) used in a course of the University of Waikato, New Zealand for performing proofs in a course on program reasoning [START_REF]Course at the school of computing and mathematical sciences[END_REF]. Furthermore, the software is going to be used from the winter semester 2007 onwards by another lecturer in a regular course on Formal Methods for the master program "Software Engineering" of the University of Applied Sciences in Hagenberg, Austria. Since we can thus expect the regular use of the software in the following years, we plan to investigate more systematically how students interact with it in order to further improve its usability.

Conclusions

We believe that the repertoire of every decent computer scientist should (based on a sound education in mathematical logic) also comprise the use of a proving assistant and that practical experience with some tool of this kind should be a part of every computer science curriculum. The RISC ProofNavigator is an attempt to help to achieve this goal. At the moment we have successfully evaluated the software by a number of use cases; soon we will also be able to report on the actual use of the software in the classroom.

Currently the major limitations of the software are the lack of rewriting as a proving strategy, i.e. equations cannot be declared as rewriting rules which complicates proofs on e.g. axiomatically declared datatypes (rather than constructively defined ones as shown in this paper). Furthermore, the software is currently bound to a particular SMT solver (CVCL); however, a diploma thesis is under way to provide a generic interface that allows the integration of other state of the art solvers.

The RISC ProofNavigator has been successfully applied to verifications that were already so complex that they were very difficult to manage with some other tools of this kind; the software should therefore be also suitable for non-classroom scenarios. Indeed our long-term goal is the development of an integrated program reasoning environment which includes the RISC ProofNavigator as a core component.

Fig. 1 .

 1 Fig. 1. The RISC ProofNavigator in Action

Fig. 2 .

 2 Fig. 2. The software architecture of the RISC ProofNavigator

  We also define the following auxiliary function constant: content: ARR -> (ARRAY INDEX OF ELEM) = LAMBDA(a:ARR): a.1;

  length: ARR -> INDEX = LAMBDA(a:ARR): a.0; new: INDEX -> ARR = LAMBDA(n:INDEX): (n, any); put: (ARR, INDEX, ELEM) -> ARR = LAMBDA(a:ARR, i:INDEX, e:ELEM): IF i < length(a) THEN (length(a), content(a) WITH [i]:=e) ELSE anyarray ENDIF; get: (ARR, INDEX) -> ELEM = LAMBDA(a:ARR, i:INDEX): IF i < length(a) THEN content(a)[i] ELSE anyelem ENDIF;

  INDEX): length(new(n)) = n; length2: FORMULA FORALL(a:ARR, i:INDEX, e:ELEM): i < length(a) => length(put(a, i, e)) = length(a);

Fig. 3 .

 3 Fig. 3. Array declarations

We do not bother to investigate the structure of this state further but immediately press the "Scatter" button which generates four child states of which one is closed automatically. Of the three remaining states [dcu],

[ecu], and [fcu], the first one is as follows:

The state has a universally quantified assumption [564]; we need to use a proper instantiation of this formula.

Since also the other two open states may have similar structures, we press which heuristically instantiates universally quantified assumptions in all these states. Indeed both [dcu] and [fcu] are closed automatically such that we only need to investigate state [ecu] further:

We might lack a concrete idea how to proceed any further and try our luck with expand length, get, i.e., an expansion of the definitions of the functions occurring in the state, yielding the substate [kel]: