| Operator (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. We consider rst-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 brie y describe the motivation for this extension coming from a related operator in the Object Constraint Language (OCL). 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||