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.