Download this episode
Description
In this episode of The Verification Corner, Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the proof before modeling it using the Dafny language.
 Try Dafny in your web browser at http://rise4fun.com/dafny !
 Find past and future episodes of the The Verification Corner!
The Verification Corner is a show on Software Verification Techniques and Tools. The show is produced by the Research in Software Engineering team (RiSE), which coordinates Microsoft's research in Software Engineering in Redmond, USA.
Share
Format
Available formats for this video:
Actual format may change based on video formats available and browser capability.
More episodes in this series
Margus Veanes  Rex  Symbolic Regular Expression Exploration
Related episodes
PerfView Tutorial 2  A Simple CPU Performance Investigation
PerfView Tutorial 1  Collecting data with the Run command
PerfView Tutorial 3  Resolving Symbols
PerfView Tutorial 0  Getting PerfView
Tutorial 10  Investigating .NET Heap Memory Leaks :Part1 Collecting the data
PerfView Tutorial 9  .NET Memory Investigation: Basics of GC Heap Snapshots
Getting Started with Visual Studio  Tips & Tricks
PerfVIew Tutorial 4  Grouping And Folding
Tutorial 11  Investigating .NET Heap Memory Leaks :Part2 Analyzing the data
Getting Started with Visual Studio  Debugging your code
The Discussion

Minor nitpick: Around 2:35 the argument is made that one needs to ensure a minimum decrease for the loop termination expression; however this is not the case. Rather, it is sufficient and necessary that the sequence of values either diverges, or converges to a value less than zero. For instance, both these loops will provably terminate, for any positive values of x and n:
/* decreases x  1 */ while (x > 1) { x = x / 2; }
/* decreases x */ while (x > 0) { x = x  (1 / n); n = n + 1; }

while (x > 0) may terminate in theory but wont do that in any other case .
int x = 1, n = 100000; while (x > 0) { x = x  (1 / n); n = n + 1; } n = 0x7ffffffe, x = 1 n = 0x7ffffff, ... n = 0x8000000, ..., n = 1, x = 2 n = 0 > div by zero

In your particular examples, there is minimum decrease. In the first example (with x = x/2), every iteration decreases x by at least 0.5 (since the loop body is entered only if x>1). In the second example, there is not a single constant that will work for every run of the program. However, the minimum decrease can be computed from the values that x and n have just before the loop begins. For example, let X denote the initial value of x and suppose the initial value of n is 1; then, it will take about e^X iterations before the 1/n terms add up to X, where e is the base of the natural logarithm and I'm using ^ to denote exponentiation; so, each iteration will decrease x by at least 1 / e^X.
What you are getting at, though, is correct, namely that what is necessary and sufficient for the loop to terminate is that the successive iterations can be mapped to strictly decreasing values in some wellfounded order.

I downloaded Boogie and dafny verifiers and wanted to know if the Dafny editor used in the demo available for download. I couldn't locate it anywhere.
Thanks!
Iman

@iman.saleh: We just recently released the Visual Studio 2010 mode for Dafny, see http://boogie.codeplex.com, click "How to install and build the sources" and then scroll down to "Visual Studio integration".
Rustan
Comments closed
Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums, or Contact Us and let us know.