Towards a Theory of Sequential Hybrid Programs
Paritosh K. Pandya, H.-P. Wang, Qiwen Xu · 1998
A theory of Sequential Hybrid Programs (SHP) is studied. SHP is a programming notation for representing hybrid systems. It contains a phase statement and the normal sequential programming constructs such as assignments, conditionals and iterations. Time dependent dynamical activities of the system are specified by phase statements. Intermixing of these two features leads to programs with a rich diversity of behaviours including super dense computations, infinite executions, finitely divergent executions and instantaneously divergent executions. Duration calculus is extended with super dense states, fixed point operators and infinite intervals to give a logic μ SDCI. A compositional semantics of SHP programs is defined using the logic μ SDCI. Several high level proof rules are derived for establishing specific kinds of properties of SHP programs such as total correctness and invariance. These high level proof rules provide a modular and syntax directed method for establishing the properties of SHP programs with the program structure guiding the proof of correctness.