Specification of parameterized programs: persistency revisited
Yngve Lamo, Michał Walicki · 2001
this paper. Study of PSPs has long tended in the direction of PDTs [1, 2, 3, 5]. One of the problems is that, while the former continued the tradition of working with classes axiomatized by (possibly conditional) equations, the latter require a precise grasp on individual algebras (which, for modeling purposes, can be identified with programs): a program P taking as a parameter another program X cannot change X -- X functions in the context of P , that is in P [X ], in the same way as it would in isolation. This intuition of "preserving actual parameter" has been identified as one of the semantic requirements on PSP in form of the persistency requirement on the functors from # Email: [email protected] + Email: [email protected] (1), e.g., [3, 15, 2]. However, in the purely equational context, there was hardly any syntactic counterpart of this semantic requirement. Thus, no syntactic/logical means were available for reasoning about correctness of such implementations