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, for each non-rigid function symbol f, a new function symbol f@prethat after program execution refers to the old value of f before program execution. We show that DL formulas with @pre can be transformed into equivalent formulas without @pre. We briefly describe the motivation for this extension coming from a related concept in the Object Constraint Language (OCL). © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Baar, T., Beckert, B., & Schmitt, P. H. (2001). An extension of dynamic logic for modelling OCL’s @pre operator. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2244 LNCS, pp. 47–54). Springer Verlag. https://doi.org/10.1007/3-540-45575-2_7
Mendeley helps you to discover research relevant for your work.