Handling data-flow programs in PVS

This paper investigates the use of the PVS tool for handling dataflowprograms. In particular, we show how to express the constructsof the Lustre synchronous data-flow language. We then provide examplesof program derivation and proofs within this framework, whichhopefully illustrate the interest of the approach.1 IntroductionRecently, several toolboxes for program formal derivation and proof havebeen proposed, among which we can cite B [1], Coq [5], and PVS [10].Clearly this...