An Extension of Dynamic Logic for Modelling OCL's @pre Operator Thomas Baar, Bernhard Beckert, and Peter H. Schmitt We consider first-order Dynamic Logic (DL) with non-rigid functions, which can be used to model certain features of programming languages such as array variables and object attributes. We extend this logic by introducing an operator @pre on functions that makes a function after program execution refer to its old value before program execution. We show that formulas with this operator can be transformed into equivalent formulas of the non-extended logic. We briefly describe the motivation for this extension coming from a related operator in the Object Constraint Language OCL.