The correctness verification methods of PLC programs include software model checking and theorem proving, etc. The paper studies the definition of denotational semantics on PLC program language, which is convenient to PLC programs modeling and model checking. The purpose of work is the correctness verification on PLC programs by formal methods. Based on the extended λ-calculus definition, the paper has defined the configuration of PLC program architecture, denotational semantics of PLC programs and functions of denotational semantics. It is the basis of model checking and theorem proving.