Abstract: 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 in order to avoid that the first cycle of the pre operator is empty. The input parameters whose type are integers and booleans are initialized to false, and those of floating-point types are initialized to floating-point zero. Those of 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.