User loginNavigation |
Framing: The implementation sideOne of the main obstacles for formally verified imperative software is the so called framing problem. A solution to the framing problem has to give a precise answer to the question: "What does a procedure modify and what does in leave unchanged?". Some weeks ago I have presented the specification view of a new attempt to solve the framing problem (An approach to framing and mutability). The following paper describes the implementation view of the frame contracts and how the implementation view and the specification view can be kept consistent. Furthermore it demonstrates how loop invariants can be kept readable by using ghost functions. By hbrandl at 2012-06-18 13:18 | LtU Forum | previous forum topic | next forum topic | other blogs | 4815 reads
|
Browse archives
Active forum topics
|
Recent comments
1 week 6 days ago
2 weeks 4 days ago
2 weeks 5 days ago
2 weeks 5 days ago
3 weeks 3 days ago
3 weeks 6 days ago
3 weeks 6 days ago
3 weeks 6 days ago
5 weeks 1 day ago
5 weeks 3 days ago