The variety of variables in automated real-time refinement

The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.

A model to investigate hepatic extraction of oxygen during anaesthesia in the dog

Measurement of hepatic oxygen extraction was performed on six healthy Greyhound dogs over a two hour period. The Greyhounds were anaesthetised and a right subcostal surgical incision performed. Ultrasonic flow transducers were used to measure flow rate in the hepatic artery and the portal vein. The blood oxygen tensions in arterial blood and in the portal and hepatic veins were also measured. Hepatic oxygen extraction remained stable throughout the study, despite a steady decline in arterial blood pressure. The methodology described in this study provides a direct measure of oxygen uptake by the liver in the dog and could readily be used to investigate hepatic uptake of drugs. (C) 2003 Elsevier Ltd. All rights reserved.