Automatic Program Verifier & Dynamic Frames: Understanding Dafny
This content delves into the intricacies of using and building an automatic program verifier, emphasizing dynamic frames in Dafny. Explore concepts such as abstraction, ghost variables, and verification practices. Dive into exercises and resources for a comprehensive understanding.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Using and Building an Automatic Program Verifier K. Rustan M. Leino Research in Software Engineering (RiSE) Microsoft Research, Redmond Lecture 4 LASER Summer School 2011 Elba, Italy 8 September 2011
Abstraction, frames Counter
Dynamic frames, recap Conceptually: class C { invariantJ; } Explicitly in Dafny: class C { function Valid(): bool { J } ghostvar Repr: set<object>; constructor Init() modifiesthis; ensures Valid() && fresh(Repr {this}); method Mutate() requires Valid(); modifies Repr; ensures Valid() && fresh(Repr old(Repr)); }
Dynamic frames idiom RockBand, RockBand2
Exercises List http://rise4fun.com/Dafny/nAW
Links Dafny research.microsoft.com/dafny rise4fun.com/Dafny/tutorial/guide rise4fun rise4fun.com Verification Corner research.microsoft.com/verificationcorner
