A hoare calculus for the verification of synchronous languages
Manuel Gesell, Klaus Schneider · 2012
The synchronous model of computation divides the execution of a program into macro steps that consist of finitely many atomic micro steps (like assignments). The micro steps of a macro step are executed within the same variable environment (i.e. in parallel) but all updates to the variables are synchronously performed at the level of macro steps. The availability of a formally defined semantics allows one to use formal methods for the verification of synchronous programs. To this end, model checking is already widely used for synchronous programs, but the use of interactive verification e.g. by using a Hoare calculus, is only in its infancies. One reason for this situation is that the assignment rule of the classic Hoare calculus implicitly defines a sequential programming model which is only a special case of the synchronous model of computation.