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 | 4182 reads
|
Browse archivesActive forum topics |
Recent comments
7 hours 9 min ago
7 hours 12 min ago
7 hours 40 min ago
14 hours 55 min ago
14 hours 58 min ago
15 hours 29 min ago
1 day 2 hours ago
1 day 2 hours ago
1 day 6 hours ago
1 day 7 hours ago