The Variety of Variables in Computer-Aided Real-Time Programming

AbstractThe refinement calculus is a well-established theory for translating specifications to program code. Recent research has extended the calculus to handle real-time requirements and we have developed an interactive support tool based on these extensions. Via a case study, this paper shows how the tool helps the programmer by supporting the many forms of variables used in the theory. These include simple state variables as in the untimed calculus, timed-trace variables that model the evolution of properties over time, and auxiliary variables that exist to support formal reasoning only