Population pharmacokinetic analysis of mycophenolic acid in renal transplant recipients following oral administration of mycophenolate mofetil

Aim To develop a population pharmacokinetic model for mycophenolic acid in adult kidney transplant recipients, quantifying average population pharmacokinetic parameter values, and between- and within-subject variability and to evaluate the influence of covariates on the pharmacokinetic variability. Methods Pharmacokinetic data for mycophenolic acid and covariate information were previously available from 22 patients who underwent kidney transplantation at the Princess Alexandra Hospital. All patients received mycophenolate mofetil 1 g orally twice daily. A total of 557 concentration-time points were available. Data were analysed using the first-order method in NONMEM (version 5 level 1.1) using the G77 FORTRAN compiler. Results The best base model was a two-compartment model with a lag time (apparent oral clearance was 271 h(-1), and apparent volume of the central compartment 981). There was visual evidence of complex absorption and time-dependent clearance processes, but they could not be successfully modelled in this study. Weight was investigated as a covariate, but no significant relationship was determined. Conclusions The complexity in determining the pharmacokinetics of mycophenolic acid is currently underestimated. More complex pharmacokinetic models, though not supported by the limited data collected for this study, may prove useful in the future. The large between-subject and between-occasion variability and the possibility of nonlinear processes associated with the pharmacokinetics of mycophenolic acid raise questions about the value of the use of therapeutic monitoring and limited sampling strategies.

Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

A partial-correctness semantics for modelling assembler programs

Previous work on formally modelling and analysing program compilation has shown the need for a simple and expressive semantics for assembler level programs. Assembler programs contain unstructured jumps and previous formalisms have modelled these by using continuations, or by embedding the program in an explicit emulator. We propose a simpler approach, which uses techniques from compiler theory in a formal setting. This approach is based on an interpretation of programs as collections of program paths, each of which has a weakest liberal precondition semantics. We then demonstrate, by example, how we can use this formalism to justify the compilation of block-structured high-level language programs into assembler.