Ingo Feinerer

Gernot Salzer
email: salzer@logic.at

A Duce

J Oliveira

P Boca

R Boute

Formal Aspects of Computing

Keywords: Formal software verification, Frege Program Prover, Key system, Perfect developer, Prototype verification system

We compare four tools regarding their suitability for teaching formal software verification, namely the Frege Program Prover, the Key system, Perfect Developer, and the Prototype Verification System (Pvs). We evaluate them on a suite of small programs, which are typical of courses dealing with Hoare-style verification, weakest preconditions, or dynamic logic. Finally we report our experiences with using Perfect Developer in class.

Introduction

Courses on the formal verification of software are part of many curricula worldwide, at least as elective subjects. Typically they cover topics like the specification of program properties using formal logic, the systematic development of programs guided by loop invariants, and formal semantics based on the Hoare calculus or weakest preconditions. Assignments are usually done on paper. Contrary to hardware verification, where fully automated model checkers are regularly used by industry, there are hardly any automated tools supporting formal software verification due to its inherent complexity.

The course Formal Verification of Software at our university was no exception; the students had to verify numerous one-loop-programs by hand, guided by the books by Dijkstra [START_REF] Dijkstra | A discipline of programming[END_REF] and Gries [START_REF] Gries | The science of programming[END_REF]. The slow but steady progress in the automation of program verification led us in 2004 to evaluate several tools in order to select one for use in the course [START_REF] Feinerer | Formal program verification: a comparison of selected tools and their theoretical foundations[END_REF]. Our aim was twofold. On the one hand an automated verification system lets the students concentrate on formal specification, with immediate feedback if the program does not match the specification. On the other hand we think that automated program verification has become mature enough to spread the word in industry, via the students. This paper is not intended as a comprehensive overview of tools for formal verification, nor does it offer a general methodology for evaluating such tools. Instead, we present four candidate systems selected with respect to the goals of our particular course (Sect. 3), and compare them on a small set of examples typical of the assignments there (Sect. 4). Section 5 summarises the results and argues why we decided in favour of Perfect Developer. Finally, Sect. 6 reports our experiences with using it in class. To put the tool evaluation into context, we start with a section describing the situation of formal methods at our university.

Correspondence and offprint requests to: G. Salzer, E-mail: salzer@logic.at

Educational background

Curricula of studies in computer science and software engineering currently undergo (or recently underwent) more or less dramatic changes at many universities. Among the reasons are: making the studies more attractive to counter the decrease in enrolment [START_REF] Denning | Recentering computer science[END_REF][START_REF] Patterson | Restoring the popularity of computer science[END_REF] or to address the underrepresentation of women and minorities [SL03]; reflecting the growth of the field by replacing old-fashioned topics by new ones; or adapting the studies to new regulations like the Bologna declaration of the EU. No matter what the reasons are, the changes usually lead to a reduction of mathematical and formal training; e.g., traditional topics like formal language and recursion theory, formal specification and verification, or the concept of mathematical proof are dropped or moved to elective courses.

As an example consider the situation at the Technische Universität Wien (Tuw, Vienna University of Technology). Its computer science department is the biggest in Austria: About 120 full, associate, and assistant professors (5 % of Tuw's teaching personnel) teach approximately 6,000 students (30 % of Tuw's students). Until 2001, there were only two monolithic studies: Informatik (informatics) taking 5 years and Wirtschaftsinformatik (business informatics) taking 4.5 years. In 2001, triggered by the Bologna declaration of the European Union, the two studies were replaced by six bachelor1 and nine master2 degrees taking three and two years, respectively.

The change of the curricula had a significant impact on the kind and amount of formal methods taught. First, specialisation and diversification now start as early as the second year; the required room was partially gained by reducing mathematics, theory and logic by one third (Table 1). Second, traditional theory and logic was compressed into a single course on bachelor level; a second course on master level now focuses on applied logics following by and large the book Logic in Computer Science by Huth and Ryan [HR03]. Apart from these compulsory courses there are only a few elective ones dealing with formal methods, most notably Computer Aided Verification emphasising model checking [START_REF] Clarke | Model checking[END_REF], and Formal Verification of Software concentrating on Hoare calculus and dynamic logic; each has 6.0 Ects and consists of a lecture and a lab. In summary, the change led to a modernisation concerning theory and logic, but at the same time reduced mathematics to a minimum, leaving hardly any room to train the ability to understand and construct rigorous proofs.

Consequently, our master course on software verification had to cope with a new situation. First, students no longer have a uniform background in programming, theory, and mathematics, since they are admitted to master studies on the basis of many different bachelor studies of computer science. Moreover, students increasingly come from abroad funded by exchange programs, doing the bachelor in one place and the master in another. Second, the focus of the subjects taught in bachelor studies has shifted. Nowadays students are trained in objectoriented modeling, networked computing, component-oriented software construction, and techniques specific to application areas, whereas the design and implementation of algorithms and data structures based on (semi-) formal principles, abstract specifications and formal reasoning has become less important.

The aim of our course is to give students of varied mathematical and computing backgrounds a common grounding in verification concepts and practice by introducing formal semantics of typical programming constructs using the Hoare calculus and weakest preconditions, by showing how to specify the behaviour of programs and derive correct programs from formal specifications, and by training the ability to argue rigorously about program correctness. Books like the one by Gries [START_REF] Gries | The science of programming[END_REF] are old regarding the time scale of computer science, but in our opinion are still of high didactic value. Based on this and similar books, our course illustrates the concepts and techniques on small examples involving mainly integers, arrays of integers, and simple loops.

Tools for formal program verification

Tools for formal program verification roughly fall into three categories: interactive or semi-automatic proof construction environments like Isabelle [Isa] or the Prototype Verification System [PVS, ORS92], tools for model checking (using abstract interpretation and similar techniques) like the Symbolic Model Verifier [SMV], and systems based on the Hoare calculus or related approaches (weakest precondition, dynamic logic) like the Frege Program Prover [START_REF]Frege Program Prover[END_REF][START_REF] Winkler | The Frege program prover[END_REF], the Key system [KEY, ABB + 05, BHS07], or Perfect Developer [PD, Cro03]. We selected the latter three systems for evaluation, since the theory part of the course concentrates on structured program development using invariants, pre-and postconditions. Moreover, we included Pvs to see whether systems for verifying algorithms (instead of programs) could be an alternative for teaching formal methods. We give short descriptions of these four tools.

Frege program prover

The Frege Program Prover (Fpp) is an experimental system developed by a group at Friedrich-Schiller-Universität Jena (Germany) for proving the correctness of simple annotated programs. Fpp is implemented as a web application: the annotated program is pasted into a web form, the verification is done at the home site of Fpp, and the result is again presented as a web page.

The program syntax is a subset of Ada and offers assignments, compound statements, if-and case-conditionals, and for-and while-loops. The only supported data types are Boolean and integer. Annotations can be used to specify pre-and postconditions, loop invariants, and termination functions. The system computes weakest preconditions or proves the correctness of Hoare triples. Verification conditions are discharged using an extended version of Analytica [START_REF] Clarke | Analytica-a theorem prover in Mathematica[END_REF], an automated theorem prover for theorems in elementary analysis. Analytica is written in the script language of Mathematica [Mat].

The key project The KeY project is developed jointly by groups at Universität Karlsruhe (Germany), Universität Koblenz-Landau (Germany), and Chalmers University of Technology (Sweden). It is distributed under the Gnu General Public License; additionally one of the supported commercial Case tools and the Java runtime environment is required.

Key aims at integrating formal specification and verification of software into the software development process. This is achieved by coupling the Key system tightly with a Case tool like Borland's Together Control Center, by supporting JavaCard-a single-threaded subset of Java intended for programming mobile and embedded devices like smart cards-as programming language, and by accepting the Unified Modeling Language (Uml) [START_REF]Unified modeling language 2.0 Superstructure specification[END_REF], the Object Constraint Language (Ocl) [START_REF]UML 2.0 Object constraint language specification[END_REF], and since recently also the Java Modeling Language (Jml) as specification language.

Key is able to generate Ocl constraints automatically by instantiating design patterns. Additionally the user may specify any valid Ocl statement, may annotate the program with Jml clauses, or may use the logic internally used by Key, dynamic logic for JavaCard. Key then checks the specification for consistency. If the user provides a refinement of the specification in the form of a program written in JavaCard, Key generates proof obligations in first-order dynamic logic and tries to discharge them automatically; alternatively, proofs can be constructed interactively by specifying explicitly the rules to be applied.

Perfect developer

Perfect Developer (Pd) is a commercial tool for the development of safety-critical software developed by the British company Escher Technologies Limited. Binaries for Windows and Linux are available free of charge to universities and schools.

Pd consists of a separate object-oriented programming language called Perfect, of an automated theorem prover, and of a code generator translating programs from Perfect to Java or C++. A rich collection of built-in data types, classes, functions, and theories allows the user to write concise specifications on a fairly abstract level. The advantage of using Perfect, a newly designed language, instead of an existing one is that the specification language, the programming language, and the prover match each other concerning expressiveness.

Pd comes with a small project manager that helps to circle between editing source files (specifications or programs) with one of several supported language-sensitive editors (Crimson, Text Pad, Multi-Edit, XEmacs, Kate, Vim), verifying specifications and refinements, generating Java or C++ code, and compiling this code. Uml class diagrams can be imported to create the skeleton of classes automatically. As feedback to the user, the verification phase provides proofs in natural deduction style and a description of failed proof attempts, in Htmlor T E X format. Pvs is a specification language integrated with support tools and a semi-automatic theorem prover. It is used for academic purposes to test new methods, but has also been successfully applied in safety-critical projects, e.g., at Nasa. In contrast to the systems presented above it does not generate verified program code, but proves properties of algorithms. The specification language is strongly typed and supports recursive definitions as well as parametrised theories that encapsulate abstract data types and their verified properties.

Evaluation

We evaluated the tools with respect to the following criteria.

1. Expressiveness The specification languages of the tools have to be sufficiently expressive to support the examples covered in the course. As benchmark we used the problems listed in Table 2, which are representative of those in the course (Tables 5,6), but which in general do not demonstrate the full power of the systems. 2. Ease of use Bearing in mind that the main objective of the course is to teach general principles of program verification, the students should not be forced to spend too much time on learning a new specification/programming language and on understanding its idiosyncrasies. Moreover, once a student has obtained a correct program by systematically refining the specification (as advocated in the course), the system should be able to discharge the proof obligations as automatically as possible. 3. Feedback on errors Error messages and reports on proof failures should provide feedback that can be readily understood without deep knowledge of the tool's specific underpinning formalism, in order to keep the focus on the verification problems itself. Note that specifications, like programs, are hardly ever correct and complete on the first try, so support in locating conflicts between specification and refinement is essential. 4. Adequate documentation There should be sufficient documentation comprehensible to students at masters level. The better the documentation the less help the teaching staff has to provide on basic language issues. 5. Ease of installation The system should be easy to install on any of the platforms students typically use, i.e., on Windows, Linux, and MacOS. It should not be necessary to install further software components from other sources.

In the remaining section we describe our experiences with each of the four systems. Table 3 summarises their evaluation on our set of benchmark problems. To convey an idea what the input to the systems looks like, Table 4 shows implementations of the factorial function for all four systems.

Frege program prover

The evaluated version dates from May 22, 2001. It seems that there was a minor update in September 2006, which does not affect the result of the evaluation.

The first thing one notes about Fpp is its simplicity. A few web pages tell everything one needs to know, there is no installation required since it is implemented as a web service hosted in Jena, and the functionality covers exactly the topics discussed in introductory books on formal software verification: given a program and a postcondition, it computes the weakest precondition; given additionally a precondition, the system checks whether the program is correct with respect to its specification. Proofs are fully automatic, no human intervention is needed. This simplicity comes at a price. The supported subset of Ada comprises basic constructs only (assignments, if-and loop-statements), the only data types are Boolean and integer, no aggregate data types like arrays are allowed. Moreover, the language for specifying verification conditions is restricted to formulas over a collection of built-in functions; it is difficult or impossible to specify program behaviour beyond the functions supported by the prover.

These limitations lead to the results in Table 3: Fpp handles well all integer problems whose behaviour can be specified. This includes factorials and even Fibonacci numbers since they are built in; see e.g. the specification in Table 4, where the result of the program is simply specified as result = factorial(n). Problems involving arrays, however, can be neither specified nor implemented.

The work with Fpp exhibited some practical problems. Fpp assumes the program to be syntactically correct and well-typed; errors are silently ignored and may lead to unexpected results like meaningless preconditions. Formulas constructed by Fpp are not simplified, hence the output (pure Ascii) can be more difficult to read than necessary. In the case of failed proof attempts-either because the specification is incomplete or because of prover limitations-the system gives no hints regarding the source of the problem. Finally, implementing Fpp as a web service also has drawbacks: it is not always available, like at the time of preparing this article.

The key project The main evaluation of the system took place in 2004 and 2005. At that time, KeY was in alpha stage at version 0.95. Contrary to the other systems it evolved considerably since then, so some of the limitations may no longer apply.

The Key system needed some effort to get it working. One reason was that Borland's Together Control Center-the commercial Case tool serving as user interface-requires a license and has to be set up separately. Our evaluation license expired after 30 days and set tight time constraints on the testing schedule.

Writing programs in JavaCard for the evaluation problems is easy for anyone familiar with Java. The bottleneck is Ocl for specifying pre-and postconditions; it is not expressive enough to capture the behaviour of the programs. Constructs like allInstances or Set{1..n} are not yet supported. Hence the specification and verification of the more complex examples involving arrays failed. For example, the postcondition of the Key implementation in Table 4 just states that the result of the program is positive; a complete specification of the factorial function against which the program can be verified is not possible at the moment. 3While the front-end of Key is quite familiar to software engineers, its back-end is not. The Key prover is an interactive tool with support for tactics and strategies which automate part of the reasoning. Directing the prover and interpreting the voluminous output requires a thorough understanding of the underlying dynamic logic and the proof rules.

The situation has recently changed with Key version 1.0, which supports the Java Modeling Language (Jml). On the one hand Key now no longer depends on the Case tool which is required to handle Uml and Ocl, on the other hand Jml is more expressive than Ocl. However, the current support of Jml is not yet sufficient for full program verification, but rather allows the user to check light-weight properties of classes and methods. Jml annotations in the program (like loop invariants) are also useful for guiding the prover and thus constitute one more step towards automation of proofs.

Perfect developer

The evaluation was initially performed with version 2.00 of Perfect Developer and later partially repeated with version 3.03. Installation under Windows and under recent Linux distributions like Redhat or Debian is straightforward. The changes since version 2.00 mostly concern the theorem prover. It has become more powerful in the sense that it is now able to discharge more proof obligations, and also has become more user friendly in the case of failed proofs as it now gives hints how to correct the specification.

Pd comes with its own object-oriented programming language called Perfect, which on the one hand excludes features of known languages that cause problems for verification, and on the other hand includes mathematical data types like unbounded integers. A rich collection of built-in data types, classes, functions, and theories allows the user to write concise specifications on a fairly abstract level. Uml class diagrams can be imported to generate the skeleton of classes automatically. People acquainted with Java or C++ will learn Perfect in a short time; the web site of Pd offers an online tutorial.

As an example, consider the Pd program for computing the factorial (Table 4). The recursive, functional specification in the third line is refined by an iterative program following the keyword via. The loop construct states that nn is a variable local to the loop (initialised with zero) and that tot is the only other variable changed by the loop. Moreover, the keyword keep introduces the loop invariant, until the loop condition, and decrease the termination function. The loop body increments nn by one and multiplies tot by nn.

Using Pd it is possible to specify and verify (automatically) all benchmark problems except the last one (see the corresponding column in Table 3). The verification of the last problem requires induction, which is not supported by the prover. The prover output is quite intuitive, mixing natural language explanations with formal logic. However, at least a basic knowledge of formal logic is required to be able to interpret the prover output and to use it for detecting errors in the specification or in the program.

Although Perfect Developer is already quite perfect, there are still some things that could be better. As mentioned above, the prover currently does not support induction. Consequently certain recursive functions and loops cannot be verified by the system; e.g., if multiplication is specified recursively by iterating over the first argument but is implemented as a loop over the second argument, the loop invariant cannot be proved automatically since the proof involves induction. As a workaround one could specify the inductive theorem as an axiom to the system, and prove the theorem outside the system. In practice this limitation is not as severe as it may seem. The principle of proof-by-contract generates dozens of proof obligations even for toy programs, most of which are rather trivial and therefore are verified by Pd's prover automatically; the user can focus his attention on a few unproven assertions resulting from the core algorithms.

Another weakness, at least from an academic point of view, is the lack of information concerning the internals of the prover. Ideally the logical rules used in correctness proofs should be open for inspection such that independent proof checkers can establish additional trust in the system. Finally, the prover does not support all specification methods equally well. It may happen that a natural and obvious specification of an algorithm leads to unprovable assertions, whereas a less obvious one using different built-ins succeeds. Ideally, the user should be able to formalise the informal specification of a problem as directly as possible without paying attention to the prover.

Prototype verification system

We used Pvs version 3.2 for our evaluation; the current version is 4.0. Since our problems scratch only the surface of what Pvs can do the precise version does not matter.

Pvs is a powerful interactive proof assistant, which is versatile and offers many possibilities. It is automatic to a certain degree, but usually requires frequent user interactions. We tried only some of the problems since it soon turned out that Pvs takes too long to learn to be used by the students in our course. By developing appropriate theories (many are already provided by the Pvs community) one can construct proofs for any problem. For example, Table 4 shows a Pvs version of factorials. It contains a recursive definition of the factorial function and states two properties of factorials, namely that factorials are always positive (fac_pos) and that factorials increase with their arguments (fac_inc). To prove the latter we need the monotonicity of multiplication with respect to its second argument (mul_mon). The lemmas fac_pos and mul_mon both can be verified by induction regarding variable x and two simplification steps:

(induct "x") (grind) (grind) Note that hardly any human intervention is needed. The proof of lemma fac_inc is more involved and uses the other two lemmas:

(skolem!) (expand "fac" :occurrence 2) (lemma mul_mon) (inst -1 "fac(1+x!1)" "x!1+2" "1") (prop) (grind) (lemma fac_pos) (grind) (grind) Lemma fac_inc is skolemised and the second occurrence of fac is expanded by its definition. Then a particular instance of lemma mul_mon is added and the result is propositionally simplified. Finally the lemma fac_pos is used to establish the precondition of lemma mulmon.

The verdict

Fpp is a valuable tool for illustrating the basic ideas of formal program verification in courses, where Hoare-style verification is just one of many topics and where concepts like postconditions and invariants are introduced for the first time. Programs are limited to those involving just integers, but no arrays. Before using Fpp in class we recommend to install the system locally to be safe from server failures in Jena; this probably requires negotiations since the tool is not offered for download by default. Fpp is too simple, however, for advanced courses based on books like [START_REF] Gries | The science of programming[END_REF], which discuss many examples using arrays and various types of quantifiers.

For such advanced courses, Pd is the best choice among the four tools at the moment. It offers a high-level language, which can be learned within the time constraints of a course. The high degree of proof automation lets the students concentrate on the primary goals of the course, namely writing correct specifications and refining them. The notoriously difficult problem of providing feedback on failed proof attempts is solved sufficiently well to give at least some help in tracking down errors. The Key system makes rapid progress and will be a serious alternative as soon as the prover offers a similar degree of automation and user friendliness as Pd's prover. The use of languages like JavaCard, Uml, Ocl, and Jml, which are familiar to most students, saves time that can be spent on more advanced examples.

Pvs requires a long learning phase due to its many basic inference rules and proof tactics, and users of Pvs need a firm background in mathematics and formal logic to guide the prover. This makes Pvs unsuitable for any regular course with its tight time constraints and the limited mathematical skills of average students. It might be the right tool for selected students at master or Ph.D. level.

Perfect developer in class

So far we have used Pd twice in a lab on formal software verification, for which the students are supposed to spend 75 working hours on average. The course can be chosen by students of informatics and business informatics as elective subject.

The first assignment consisted in installing Perfect Developer under Windows or Linux, and in getting acquainted with the system by working through the online tutorial offered on the web site of Escher Technologies, the company behind Pd. As a check we asked the students to write a report listing the errors in the tutorial; there are a few, which can be easily corrected provided the assignment is taken seriously.

The second, third and fourth assignment consisted in selecting two problems from a list of six easy and one problem from a list of four harder problems (Tables 5,6). The students had to write a formal specification in Perfect, refine it to an executable function and verify the correctness. The algorithms were required to run in time O(n) or O(n log n), since in many cases Pd is able to generate code automatically from the specification which for these examples has quadratic or cubic runtime. The students had to write a report including their errors, solutions, and the time they had spent on the problem. In case they were not able to get Pd to verify their solution completely they had to provide formal arguments explaining why their specification and implementation was correct nevertheless.

We used the collected data to answer two questions: (1) Are 75 h sufficient for learning to use the system and doing the assignments? (2) How relevant are algorithmic, formal, and mathematical skills as prerequisite for doing the assignments? We separated the students into two groups: those doing a bachelor or master program in informatics, and those doing a bachelor or master in business informatics. In the curriculum valid until 2006, the latter had a few hours less on math, algorithmics and programming than their colleagues in pure informatics.

The statistical analysis is summarised in Figs. 1 and2. Students in informatics needed less time on average and got better grades than their colleagues in business informatics. All students finished the assignments in time; those studying informatics needed only half of the allotted time. This shows that even though Perfect Developer is new to the students, there is sufficient time to get acquainted with the system to solve the assignments. In fact, there is even time for more assignments. Moreover, the intuition is confirmed that the ability of applying formal methods correlates with the amount of algorithmic and mathematical training on bachelor level.

  . . . using Fpp --!pre: n >= 0; result := 1; --!pre: result = 1 AND n >= 0; --!post: result = factorial(n); --!inv: result = factorial(i); FOR i IN 1..n LOOP result := result * i; END LOOP; . . . using Key public class Fac { /* @preconditions n >= 0 @postconditions result > 0 */ public static int fac(int n) { if (n == 0) return 1; else return (n * fac(n -1)); } } . . . using Pd function factorial(n: nat): nat decrease n ^= ([n = 0]: 1, []: n * factorial(n -1)) via var tot: nat! = 1; loop var nn: nat! = 0; change tot keep tot' = factorial(nn') until nn' = n decrease n -nn'; nn! = nn + 1; tot! = tot * nn end; value tot end; . . . using Pvs fac: THEORY BEGIN n, x, y, z: VAR nat fac(n): RECURSIVE nat = (IF n = 0 THEN 1 ELSE n * fac(n-1) ENDIF) MEASURE (LAMBDA n: n) mul_mon: LEMMA FORALL x, y, z: (x > 0 AND y > z) IMPLIES x * y > x * z fac_pos: LEMMA FORALL x: fac(x) > 0 fac_inc: LEMMA FORALL x: fac(x + 1) < fac(x + 2) END fac

Fig. 1 .Fig. 2 .

 12 Fig. 1. Time needed for assignments (hours)

Table 1 .

 1 Comparison of old and new CS curricula

		Duration	Credits	Math and statistics	Theory and logic
	Diploma study (up to 2001)	5 years	324 Ects	34.5 Ects (10.6%)	19.5 Ects (6.0%)
	Bac.+Mast. (2001 onwards)	3+2 years	180 + 120 Ects	21.0 Ects (7.0%)	12.0 Ects (4.0%)
	Ects ECTS credit, where ECTS means European Credit Transfer System; 1 year corresponds to 60 Ects, 1 Ects equals 25 working hours in
	Austria.

Table 2 .

 2 Problems for evaluating the systems A, of n integers, count the pairs (i, j ) of indices satisfying i < j andA[i] > A[j ] QuicksortGiven a sequence of integers, perform Hoare's Quicksort Prototype verification system The Prototype Verification System (Pvs) was developed at the Stanford Research Institute (SRI). It is an open source Lisp program under the Gnu General Public License with pre-built binaries for Linux, SunOS and MacOS, and uses the Emacs editor as user interface.

	Problem	Description
	Conditional Cubic sum Multiplication Division Factorial Prime	Check pre-and postconditions for an if-statement Given a positive integer n, compute n i 1 i 3 Given two positive integers m and n, compute the product m • n Given two positive integers m and n, compute the quotient and remainder for the division m n Given a positive integer n, compute the factorial n i 1 i Given a nonnegative integer n, determine whether n is prime
	Index of maximum	Given a list of integers, determine the index of a maximal element
	Card. of intersection	Given two sorted lists of integers, compute the cardinality of their intersection
	Count inversions	Given a list,

Table 3 .

 3 Summary of evaluation on benchmark problems

	Problem	Fpp	Key	Pd	Pvs
	Conditional				.
	Cubic sum
	Multiplication
	Division				.
	Factorial		?
	Prime	?	?		.
	Index of maximum	-	?		.
	Cardinality of intersection	-	?		.
	Count inversions	-	?
	Quicksort	-	?	?
	algorithm can be specified and verified
	? algorithm can be specified, but not properly verified
	-algorithm can be neither specified nor verified
	. not evaluated

Table 4 .

 4 Computing the factorial of a number

Table 5 .

 5 Simple assignments

	Problem	Description
	Card. of intersection	Given two sorted lists of integers, compute the cardinality of their intersection in linear time
	Merging of lists	Given two sorted lists of integers, compute a sorted list containing the elements of the original lists in
		linear time
	Minimal distance	Given two sorted lists of integers, A and B, compute the minimum of abs(A[i], B[i]) for all i, j in linear
		time
	Longest plateau	Given a sorted list of integers, determine the length of the longest sublist of identical elements in linear
		time
	Index of maximum	Given a list of integers, determine the index of a maximal element in linear time
	Sortedness	Check in linear time whether a list of integers is sorted

Table 6 .

 6 More difficult assignmentsGiven a list of integers, compute in linear time the length of the longest sublist, where the first element of the sublist is minimal among the elements of the sublist

	Problem	Description
	Count inversions	Given a list, A, of n integers, count the pairs (i, j ) of indices satisfying i < j and A[i] > A[j ] in time
		O(n log n)
	Count Boolean	Given a list, A, of Booleans, count the pairs (i, j ) of indices satisfying i < j , A[i] and ¬A[j ], in linear
	inversions	time
	Length of longest	Given a list of integers, compute the length of the longest non-increasing or non-decreasing sublist in
	monotone sublist	linear time
	Length of longest
	left-minimal sublist

Business Informatics, Computer Engineering, Data Engineering and Statistics, Media Informatics, Medical Informatics, Software and Information Engineering.

Business Engineering and Informatics (Wirtschaftsingenieurwesen Informatik), Business Informatics, Computer Engineering, Computational Intelligence, Information and Knowledge Management, Media Informatics, Medical Informatics, Software Engineering and Internet Computing, Visual Computing.

As a workaround one could specify the postcondition as a formula of the dynamic logic that is used internally by Key. This is no option, however, for an introductory course and its tight time constraints.

Acknowledgments

We are grateful to two anonymous referees for their detailed and constructive criticism. Their advice lead to substantial improvements.


Laura Ottolenghi

Vittorio Bertele'
email: bertele@marionegri.it

Silvio Garattini

Limits of add-on trials: antirheumatic drugs

Keywords: Add-on studies, Registration trials, Marketing authorisation, European Medicine Agency, Rheumatoid arthritis, Disease-modifying antirheumatic drugs, Infliximab, Etanercept, Adalimumab, Rituximab, Anakinra, Abatacept, Methotrexate

published or not. The documents may come

Introduction

The principle behind the need for combination therapy is to use drugs with different mechanisms of action together to increase efficacy without increasing toxicity in multifactorial diseases such as diabetes, hypertension, etc. This is the case with rheumatoid arthritis (RA) also, in which patient responses to standard treatments tend to vary. The European Medicine Agency (EMEA) guidelines of 2003 (CPMP/ EWP/556/95 rev1/Final) recommend that approval of new antirheumatic drugs for RA should be based on proof of efficacy from adequately designed parallel group randomised trials against placebo, or comparative studies against an established active comparator. Combination therapy is also accepted, as this strategy "is gaining popularity", provided that therapeutic claims, pharmacological rationale and investigation on drug interactions are presented. "Addon placebo therapy may also be used when study design requires placebo and allows for combination with other effective treatment".

Following on from our previous critical evaluation of regulatory criteria for marketing approval of antirheumatic drugs [START_REF] Bertele | New antirheumatic drugs: any real added value? A critical overview of regulatory criteria for their marketing approval[END_REF], this paper focuses on how add-on studies influence regulatory decisions, examining the design of clinical studies used in the process of EMEA regulatory approval of new anti-RA agents.

Methods

Information on each anti-RA drug approved by the EMEA from 1995 to 2007 was collected from the European Public Assessment Reports (EPARs), Scientific Summary (www. emea.europa.eu/index/indexh1.htm), and completed with the published papers on the trials that provided the basis for approval. These trials were reviewed with particular attention to study design, type of comparator used, combination therapy and inclusion criteria and are grouped according to the comparators used or their combinations.

Results

Seven anti-RA [one nonbiological, three tumour necrosis factor (TNF)-α blockers-infliximab (IFX), etanercept (ETN) and adalimumab (ADL)-the interleukin (IL)-1 blocker anakinra (ANK), the anti-CD20 antibody rituximab (RTM) and the selective co-stimulation modulator abatacept (ABA] were granted a marketing authorisation (MA) by the EMEA. Table 1 reports the main characteristics of the pivotal clinical studies submitted to EMEA: leflunomide (LFE) [2], the only nonbiological disease modifying antirheumatic drug (DMARD) and the first to be approved (1999), was authorised on the basis of four phase III trials [START_REF] Scott | Treatment of active rheumatoid arthritis with leflunomide: two year followup of a double blind, placebo controlled trial versus sulfasalazine[END_REF][START_REF] Smolen | Efficacy and safety of leflunomide compared with placebo and sulphasalazine in active rheumatoid arthritis: a double-blind, randomised, multicentre trial. European Leflunomide Study Group[END_REF][START_REF] Emery | A comparison of the efficacy and safety of leflunomide and methotrexate for the treatment of rheumatoid arthritis[END_REF][START_REF] Strand | Treatment of active rheumatoid arthritis with leflunomide compared with placebo and methotrexate. Leflunomide Rheumatoid Arthritis Investigators Group[END_REF] including placebo and active controls [methotrexate (MTX) and sulphasalazine (SSZ)], although only superiority over placebo was demonstrated. ETN [7] gained approval in 2000 as monotherapy or in combination with MTX in patients inadequately responding to a DMARD, with two phase III studies vs. placebo [START_REF] Moreland | Etanercept therapy in rheumatoid arthritis. A randomized, controlled trial[END_REF][START_REF] Jobanputra | The effectiveness of infliximab and etanercept for the treatment of rheumatoid arthritis: a systematic review and economic evaluation[END_REF] and one phase II/III add-on study [START_REF] Weinblatt | A trial of etanercept, a recombinant tumor necrosis factor receptor:Fc fusion protein, in patients with rheumatoid arthritis receiving methotrexate[END_REF]. Indication for treatment (in combination with MTX) of early RA patients not previously treated with MTX followed in 2004, with two phase III studies [START_REF] Genovese | Etanercept versus methotrexate in patients with early rheumatoid arthritis: two-year radiographic and clinical outcomes[END_REF][START_REF] Klareskog | Therapeutic effect of the combination of etanercept and methotrexate compared with each treatment alone in patients with rheumatoid arthritis: double-blind randomized controlled trial[END_REF] comparing ETN and MTX and with the combination of the new agent and MTX. An add-on study supported approval of the 50-mg strength (2005) [START_REF] Keystone | Once-weekly administration of 50 mg etanercept in patients with active rheumatoid arthritis: results of a multicenter, randomized, double-blind, placebo-controlled trial[END_REF].

The clinical trial programme for the initial authorisation (2000) of IFX [14] encompassed six clinical studies, the pivotal one being a phase III add-on study [START_REF] Maini | Infliximab (chimeric anti-tumour necrosis factor alpha monoclonal antibody) versus placebo in rheumatoid arthritis patients receiving concomitant methotrexate: a randomised phase III trial. ATTRACT Study Group[END_REF], which demonstrated the superiority of the combination in active RA patients inadequately responding to a DMARD (MTX). The extension of indication for early RA in patients not previously treated with MTX or other DMARDs ( 2001) was based on one clinical trial [START_REF] St Clair | Combination of infliximab and methotrexate therapy for early rheumatoid arthritis: a randomized, controlled trial[END_REF] comparing the combination of IFX and MTX with MTX plus placebo in MTX-naïve patients.

ADL [17] was approved in 2002 for treating patients inadequately responding to MTX on the basis of four studies, two that were placebo-controlled [START_REF] Van De Putte | Efficacy and safety of adalimumab as monotherapy in patients with rheumatoid arthritis for whom previous disease modifying antirheumatic drug treatment has failed[END_REF]; one primarily a safety study; and two add-on trials [START_REF] Weinblatt | Adalimumab, a fully human antitumor necrosis factor alpha monoclonal antibody, for the treatment of rheumatoid arthritis in patients taking concomitant methotrexate: the ARMADA trial[END_REF][START_REF] Keystone | Radiographic, clinical, and functional outcomes of treatment with adalimumab (a human anti-tumor necrosis factor monoclonal antibody) in patients with active rheumatoid arthritis receiving concomitant methotrexate therapy: a randomized, placebocontrolled, 52-week trial[END_REF]. In MTXnaïve patients, a phase III RCT supported the combination of ADL and MTX (2005) [START_REF] Breedveld | The PREMIER study: A multicenter, randomized, double-blind clinical trial of combination therapy with adalimumab plus methotrexate versus methotrexate alone or adalimumab alone in patients with early, aggressive rheumatoid arthritis who had not had previous methotrexate treatment[END_REF].

ANK [22] in combination with MTX received approval (2002) on the basis of two add-on randomised clinical trials (RCTs) [START_REF] Cohen | Treatment of rheumatoid arthritis with anakinra, a recombinant human interleukin-1 receptor antagonist, in combination with methotrexate: results of a twenty-four-week, multicenter, randomized, double-blind, placebo-controlled trial[END_REF][START_REF] Cohen | A multicentre, double blind, randomised, placebo controlled trial of anakinra (Kineret), a recombinant interleukin 1 receptor antagonist, in patients with rheumatoid arthritis treated with background methotrexate[END_REF] and one dose-finding study lasting 24 weeks (not reported in Table 1).

RTM [25] in combination with MTX is indicated for severe active RA in patients inadequately responding or intolerant to DMARDs, including one or more TNF inhibitors (2006). The clinical programme included one phase III add-on trial and two supportive phase II studies: one comparative vs. MTX and one add-on.

ABA [26], the latest to be approved (2007), with an indication similar to RTM, presented a clinical development programme including three studies providing the main efficacy data and three with additional efficacy/safety information: a phase IIA pilot dose-finding monotherapy (not reported in Table 1), a phase IIB exploratory, and a phase III study. One further pivotal trial was submitted during evaluation of the MA application. As stated in the EPAR, it was designed "to validate the efficacy responses and to directly compare the safety profile of ABA-MTX and IFX-MTX combinations and placebo rather than to demonstrate noninferiority or superiority of ABA compared to infliximab". In all studies, ABA was tested as add-on to background therapy with MTX, DMARDs or anti-TNF.

On the whole, comparison with placebo was the topic of four trials, mainly dose ranging, of ETN and ADL (Table 2). LFE (four studies) and ETN (one) were compared with but were no better than established comparators. Four studies (ETN, ADL, RTM, IFX) comparing the efficacy of the test products and of the active comparator MTX alone or their combinations confirmed the better efficacy of the combination arm.

The add-on design was the most frequent approach used in the approval process of new biologic response modifiers. Three strategies were used in combination therapy in RA: "parallel" (multiple treatments are administered concurrently), "step-up" (addition of a DMARD to the background of another, partially effective, DMARD) and "step-down" (concomitant DMARDs sequentially withdrawn once benefit has been achieved) [START_REF] Verhoeven | Combination therapy in 369 rheumatoid arthritis: updated systematic review[END_REF]. For four agents (IFX, ETN, ADL and RTM) the add-on trials contributed to obtaining approval as combination therapy, whereas ANK and ABA were authorised only on the data of add-on trials.

The new biologic agents are all indicated (Table 2) in combination with MTX for treating adult patients with active RA inadequately responding to previous DMARDs, including MTX and one or more TNF inhibitors, such as RTM and ABA. ADL is approved for monotherapy only in case of intolerance to MTX or when continued treatment with MTX is inappropriate.

A further critical issue in the process of approval of new agents is pharmacokinetic drug interactions. Table 3 summarises the pharmacokinetic and interaction studies reported in the EPAR. Routine pharmacokinetic studies were produced for each new agent, but formal studies on interactions were either generally limited (MTX raised plasma concentrations of IFX, did not modify the kinetics of RTM and ETN; the influence of ETN on MTX was not investigated) or neglected, as in the case of concomitant background therapy. Only clinical evidence of toxicity in patients concurrently receiving two TNF antagonists led to the warning not to use such combinations.

Discussion

Our survey found that add-on trials had an important role in the approval process of the newer antirheumatic agents, possibly because this approach easily provides a demonstration of efficacy. In the last few years, the comparison of a new drug or placebo added to ongoing DMARD treatment has become the standard trial design, with MTX being the standard DMARD [START_REF] Hochberg | Stepping-up" from methotrexate: a systematic review of randomised placebo controlled trials in patients with rheumatoid arthritis with an incomplete response to methotrexate[END_REF][START_REF] Kremer | Rational use of new and existing diseasemodifying agents in rheumatoid arthritis[END_REF], in a population of socalled partial responders.

Add-on trials are reported to have some practical advantages (absence of flares, similarity to daily practice, benefits of maintenance of concomitant drugs, proof of concept accepted by regulatory agencies). However, data on the superiority of combination DMARD therapy in RA are controversial [START_REF] Smolen | Superior efficacy of combination therapy for rheumatoid arthritis: fact or fiction?[END_REF] because of confounding factors. These include inadequate definition of incomplete responders to previous/concomitant DMARDs, quite low percentages of patients without adequate response to MTX and background therapy (NSAIDs, glucocorticoids) not considered a part of the add-on combination [START_REF] Boers | Add-on or step-up trials for new drug development in rheumatoid arthritis: a new standard?[END_REF][START_REF] Pincus | Add-on or step-up trials in rheumatoid arthritis: comment on the article by Boers[END_REF][33]. In phase III co-administered MTX, corticosteroids, NSAIDs, anti-TNF no influence on ABA Cl.

No studies in special populations Some of the drawbacks reported in the literature show up in the add-on studies included in this review (Table 1). The inclusion criteria of the add-on trials submitted to the EMEA show the heterogenicity of the patient populations enrolled (suboptimal response to one or more DMARD, duration, type and dosages of background therapy, with or without washout period, etc.). In the majority of the add-on trials, patients had very active disease and were "inadequate" or "partial" responders to MTX or anti-TNF agents. Another point for concern is the failure to report detailed information about the number and dosage and possible interactions of concomitant background medications, specifically NSAIDs and corticosteroids, which are anti-inflammatory agents with their own efficacy and toxicity. Another disadvantage of this design is that it can be potentially harmful, as shown by the negative experience with combined ANK and ETN [34] and the exploratory phase IIB study adding ABA to ETN [35].

The main concern, however, regards the use of placebo in patients with a poor response to current treatment. If the treatment is definitively ineffective, it should not be continued in either treatment group, as it would be useless and therefore unethical. If it is partially effective, adding placebo in one arm while providing an active drug in the other would be unethical too. It is advisable in any case to compare two active treatments, as either an alternative or an add-on to the current unsatisfactory therapies. Comparing one treatment against two seems an uneven challenge, it being possibly easier for the new drug together with the standard treatment to perform better than the latter alone. Moreover, this approach does not provide adequate information on how the test drug added on top of ongoing therapies fares in comparison with other treatments.

The lack of direct comparisons between new active principles makes it difficult to choose among so many alternatives. Ideally, it would be useful to compare any new agent with the best current treatment and with their combination (A vs. B vs. A + B, than A vs. C vs. A + C, and so on). In view of the lack of direct comparisons of newly approved anti-RA, it is difficult to identify the "gold standard" of treatment on top of MTX with which a new compound should be compared. From a historical point of view, the first approved agent, LFE, should have served as comparator for the next ones, namely IFX and ETN. Combinations should also be compared with each other. In the approval process, the true value of the new agent alone and in combination should be assessed through superiority clinical trials.

The pharmacokinetic drug interactions studies, which do not actually seem to be considered very important, are in fact needed because research on interactions could be helpful in developing rational combination therapy with less toxicity. These studies would also show whether apparently better efficacy of the add-on approach is merely due to a higher concentration of one or the other component of the combination.

In conclusion, the add-on approach is popular for registration purposes, as it offers many practical, financial (savings in time and investment and exempting the sponsor from correct comparisons) and theoretical advantages, mirrors clinical practice and substantially demonstrates the efficacy of a combination. This design, however, does not provide firm proof that any effect observed really relates to the combination, as the control arm is so often a placebo in patients with active disease despite treatment with MTX or other background therapy, so it is difficult to assess the intrinsic efficacy and safety of the new agent and its value as an alternative to current remedies. The indications granted do not indicate whether newer drugs can replace standard treatments in nonresponders and even less whether they can do better. Nor do they say which of them must come first, if any.

This review of the clinical data submitted to the EMEA indicates that to obtain approval easily, no comparative studies between the new biologic anti-RA agents were done, even though efficacy patterns seem to be similar and a direct comparison would have been possible, at least after the MA. Surprisingly, not even equivalence or noninferiority trials against the best available treatment were done. As uncontrolled trials artificially set up in the late stages of diseases, placebocontrolled trials and equivalence or noninferiority trials, the add-on approach complies with the European Pharma law [36], which allows each drug to be approved on the basis of its own quality, safety and efficacy, with no need for comparison with active comparators. Legislators and regulatory authorities could usefully redesign regulations and registration trial requirements, as suggested above, with a view to obtaining unequivocal data about the comparative efficacy and safety of current and newer drugs, including anti-RA agents, which would best meet the needs of the clinical community.

  33

Table 1

 1 Registration trials in rheumatoid arthritis according to study design

	Efficacy primary endpoint		ETN 25 mg p<0.001 vs. PLB		All dosing regimens significantly	more effective than PLB	ACR 20: ADL 40 mg eow/weekly	p≤0.001		No specific concern on concomitant	use of DMARDS ACR 20	(secondary endpoint)	response superior to PLB	efficacy comparable with SSZ		LFE significantly superior to PLB.	NS vs. SSZ	LFE significantly less effective	than MTX		LFE significantly superior to PLB.	NS vs. MTX	Radiographic progression results	NS different between	treatment groups	24 weeks: ACR-N AUC ETN +	MTX p<0.01 vs. ETN and MTX	Week 52: ACR 50 response ADL +	MTX p<0.001 vs. ADL + PLB and	MTX + PLB	ACR 50: RTM + CTX and RTM +	MTX statistically superior	significantly	ACR response: combination	p<0.001 vs. MTX	ACR 20: each group p<0.0001	vs. control	ACR 20: ETN + MTX p < 0.001	vs. MTX	Safety and efficacy comparable
	trial design, duration	(weeks)	Phase III RCT, DB, PG 24 [8]		Phase III RCT, DB, PG 12 [9]		Phase III RCT, DB, PG 26 [18]			Phase III RCT, DB 24				Phase III RCT, DB, PG 24 [3]		Phase III RCT, DB, PG 24 [4]		Phase III, equivalence RCT,	DB, PG 52+52 [5]		Phase III RCT, DB, PG 52 [6]		Phase III RCT, DB, PG 52 [11]			Phase III RCT, DB, PG 52 [12]		Phase III RCT, DB, PG 104 [21]			Phase IIa RCT, DB, PG 24+80			Phase III RCT, DB, PG 54 [16]		phase III RCT, DB, PG 54+48 [15]	Phase II/III RCT, DB, PG 24 [10]	Phase III RCT, DB, PG 16 [13]
	No.	patients	234		599		544			630				197		358		999			482		632			682		799			161			1004		428	89	420
	treatment		ETN 2 doses tw vs. PLB		ETN 4 dosing regimens vs. PLB		ADL 4 dosing regimens vs. PLB			ADL 40 mg eow vs. PLB				LFE vs. SSZ		LFE vs. SSZ vs. PLB		LFE vs. MTX			LFE vs. MTX vs. PLB		ETN 2-weekly dosing regimens	+ PLB vs. MTX + PLB		ETN 25 mg tw vs. MTX vs.	ETN + MTX	ADL 40 mg eow + PLB vs.	ADL + MTX vs. MTX + PLB		RTM vs. MTX vs. RTM + CTX	vs. RTM + MTX		IFX 2 doses + MTX vs.	PLB + MTX	MTX + PLB vs. MTX + IFX	4 doses	MTX + PLB vs. MTX + ETN	25 mg tw	MTX + PLB vs. MTX + ETN	25 mg tw vs. MTX + ETN 50 mg
	Concomitant medication		NSAIDs corticosteroids		NSAIDs corticosteroids		None			Any DMARD except	azathioprine, cyclosporine,	anti-TNFs		NSAIDs, low-dose	corticosteroids	NSAIDs, low-dose	corticosteroids	NSAIDs, low-dose	corticosteroids		NSAIDs corticosteroids	folate supplementation	NSAIDs corticosteroids	folate supplementation		Folate supplementation		Folate supplementation						Folate supplementation?		Corticosteroids NSAIDs	folate supplementation	NSAIDs folate	supplementation	50% on MTX	corticosteroids NSAIDs
	Inclusion criteria		DMARD failing patients	(washout 1 month)	DMARD failing patients	(washout 4 weeks)	DMARD failing patients	(mainly MTX), washout	of all prior treatment	DMARD failing or	DMARD-naïve patients			DMARDs washout		DMARDs washout-naïve	patients about 2/3	folate supplementation in	10% patients, DMARDs	washout	MTX-naïve DMARDs	washout	MTX-naïve patients	DMARDs washout 4 weeks		DMARDs other than MTX	nonresponders	MTX-naïve patients and	DMARDs (67.5%) (washout	for DMARDs)	DMARDs inclusive anti-TNF,	nonresponders		MTX-naïve patients		MTX nonresponders	(on stable MTX for 30 weeks)	DMARDs nonresponders MTX	stable dose 4 weeks	MTX stable dose 28 weeks
	Drug	A vs. PLB	Etanercept [7]				Adalimumab [17]			Safety study			A vs. B (vs. PLB)	Leflunomide [2]	extension	study							Etanercept [7]	early RA	A vs. B vs. A + B	Etanercept [7]		Adalimumab [17]	early RA		Rituximab [25]	supportive	A + B vs. B + PLB	Infliximab [14]	early RA	Add-on	Infliximab [14]	pivotal	Etanercept [7]

Table 2

 2 Designs adopted in registration trials and approved indications of each antirheumatic drug

	Drug	A vs.	A vs. B	A vs.	A + B	Add-on	Approved indication
		PLB	(vs. PLB)	B vs.	vs. B	A + PLB
				A + B	+ PLB	A + B
	leflunomide		4				Treatment of adults with active RA as a DMARD
	etanercept	2	1	1		2	In combination with MTX for moderate to severe active RA in
							adults with inadequate response to DMARDs
	infliximab				1	1	In combination with MTX for reduction of signs and symptoms
							and improvement of physical function in active RA patients with
							inadequate response to DMARDs. Patients with severe, active
							progressive disease not previously treated with MTX or DMARDs
	adalimumab	2		1		2	In combination with MTX for moderate to severe active RA in adults
							with inadequate response to DMARDs and in patients with severe,
							active progressive disease not previously treated with MTX. In
							monotherapy in case of intolerance to MTX or continued treatment
							with MTX is inappropriate
	anakinra					2	For signs and symptoms of RA in combination with MTX in patients
							with an inadequate response to MTX alone
	rituximab			1		2	In combination with MTX for treatment of adults with severe active
							RA with inadequate response or intolerance to other DMARDs
							including one or more TNF inhibitors
	abatacept					6	In combination with MTX for moderate to severe active RA with
							insufficient response or intolerance to other DMARDs including
							at least one TNF inhibitor

A new drug, B active comparator, PLB placebo. See abbreviation list for all other definitions

Table 3

 3 Pharmacokinetics (PK) and interaction studies for each antirheumatic drug

	warnings	Liver and renal impairment contraindicated	Concomitant administration of hepatotoxic or	hematotoxic DMARDs (MTX) not advisable			The combination with ANK and ETN (serious infections seen	in clinical studies) not recommended		combination with ANK not recommended (serious	infections seen in clinical studies)					The combination with ANK not recommended (serious	infections seen in clinical studies)					Not to be used in severe renal insufficiency	Combination with any other TNF antagonist not recommended	(increased risk of serious infections)			Concomitant/sequential use of other DMARDs other than those	specified under RA indications not recommended	Insufficient data on safety of sequential use of other DMARDs	(including TNF inhibitors)	Combination with TNF antagonists not recommended (increased	risk of serious infections)
	interaction studies	No influence by CYP inhibition or induction	(cimetidine, rifampicin).	No safety problems with NSAIDs	No effect on PK by cimetidine, ibuprofen, diclofenac	No PK interaction with MTX	MTX slightly raised	IFX plasma	concentrations	No formal studies conducted	No interactions observed in clinical trials	Pk not altered by MTX	No data on the effect of ETN on MTX (no	effect in animal studies)		Concomitant NSAIDs: no influence on safety	Limited experience on concomitant DMARDs	other than MTX	MTX increased exposure to ADL by about 40%	Slightly higher % of infectious SAEs in ADL patients	taking corticosteroids	No evidence of interactions with NSAIDs or	corticosteroids (no studies)				No specific studies.	Not influenced by cyclophosphamide or MTX.	Cmax may be increased by high doses of corticosteroids.	No specific studies.
	pharmacokinetic studies	Basic parameters	Impaired renal function, no change	Impaired liver function, not done but contraindicated			Basic parameters	No studies on metabolism and excretion	No impaired organ function studies	Basic parameters	Renal and hepatic failure (limited data):	No change in dosage	No effect of age, gender, ethnic origin	PK in CHF patients similar to healthy	subjects and RA patients	Basic parameters	No data on renal, hepatic failure	Cl 44% lower in MTX-treated patients	Trend to decreasing Cl with increasing age.	No gender differences.		Basic parameters subcutaneous and	intravenous injection.	Elimination route not studied.	Cl: no effect of gender or age; reduced in	hepatic impairment; no studies in severe insufficiency	Basic parameters	No data on renal, hepatic failure and hypoproteinuria	No data on PK of NSAIDs or other drugs	In RCT phase II/III basic parameters.	No accumulation following monthly dosing.	No effect of age or renal function.
	drug	leflunomide					infliximab			etanercept						adalimumab						anakinra					rituximab			abatacept

  . Strand V (2004) Counterpoint from the trenches: a pragmatic approach to therapeutic trials in rheumatoid arthritis. Arthritis Rheum 50:1344-1347 34. Genovese MC, Cohen SB, Moreland L et al (2003) A randomized double-blind controlled trial study evaluating the safety and efficacy of etanercept vs. etanercept plus anakinra in patients with rheumatoid arthritis. Ann Rheum Dis 62(Suppl.1):66 35. Weinblatt M, Schiff M, Goldman A et al (2007) Selective costimulation modulation using abatacept in patients with active rheumatoid arthritis while receiving etanercept: a randomized clinical trial. Ann Rheum Dis 66:228-234 36. Regulation (EC) No 726/2004 of the European Parliament and of the Council of 31 March 2004 laying down Community procedures for the authorization and supervision of medicinal products for human and veterinary use and establishing a European Medicines Agency. Available on the web: http:// europa.eu/scadplus/leg/en/lvb/l22149.htm (last access June 25, 2008)

Acknowledgments The authors are grateful to Giuseppina Petruzzelli of the G.A. Pfeiffer Memorial Library, to Judith Baggott for editorial assistance and to Elena Pozzoli for secretarial support.

Conflict of interests None of the authors has any financial or personal relationships with other people or organisations that could be considered conflicts of interest for this work.

Source of funding Institutional funds from the Mario Negri Institute