Framing the frame problem (new paper)
Among the open problems of verification, particularly the verification of object-oriented programs, one of the most vexing is framing: how to specify and verify what programs element do not change. Continuing previous work, this article presents a “double frame inference” method, automatic on both sides the specification and verification sides. There is no need to write frame specifications: they will be inferred from routine postconditions. For verification, the method computes the set of actually changed properties through a “change calculus”, itself based on the previously developed alias calculus.
Some verification techniques, such as Hoare-style proofs, require significant annotation effort and potentially yield full functional verification; others, such as model checking and abstract interpretation, have more limited goals but seek full automation. Framing, in my opinion, should be automatic, freeing the programmer-verifier to devote the annotation effort to truly interesting properties.
Reference
[1] Bertrand Meyer: Framing the Frame Problem, in Dependable Software Systems, Proceedings of August 2014 Marktoberdorf summer school, eds. Alexander Pretschner, Manfred Broy and Maximilian Irlbeck, NATO Science for Peace and Security, Series D: Information and Communication Security, Springer, 2015 (to appear), pages 174-185; preprint available here.
Eiffel Software
Home page at ETH
Informatics Europe
LASER summer school
Propulsion Academy
The paper says that the frame problem is all about ‘x = old x’ expressions. From my perspective, this has never been the problem. The actual problem is that there are many things that need to be said that are not expressible as queries, because the vocabluary is missing (independent classes, features introduced in subclasses, unreachable objects etc.). I do not agree with reducing the frame problem to ‘x = old x’.