Summary: Refinement calculus is a formal framework for the development of provably correct software. It is used by action systems, a predicate transformer based framework for constructing distributed and reactive systems. Recently, action systems were extended with a new action called the differential action. It allows the modelling of continuous behaviour, such that action systems may model hybrid systems. In this paper we investigate how the differential action fits into the refinement framework. As the main result we develop simple laws for proving a refinement step involving continuous behaviour within the refinement calculus.
For the entire collection see [Zbl 0911.00057].