Translation Verification of Synchronous Data Stream Language Pre Operator in Coq

The pre operator of the synchronous data stream language is processed in detail. In addition to translating the pre operator to the fby operator, the value of the pre operator in the first cycle is initialized according to the type of its input parameters. Solved the problem that the first cycle of the pre operator is empty. The input parameters are integers and booleans whose first cycle is initialized to false, and floating-point types are initialized to floating-point zero. Array and structure types are initialized differently according to their element types. The translation application scenarios of the pre operator are mostly nuclear power safety digital control systems (SDCS). In order to ensure the correctness and safety of its compilation, the entire translation process has undergone strict formal verification, and all of them are in the auxiliary theorem prover Coq completed in. The translation and verification method has been tested in SDCS, and can achieve the expected translation effect.