
Hi,
http://rise4fun.com/Dafny/TplFw
I have a Stream codatatype, and a predicate which distinguishes finite streams. I want to write a function that given such a finite stream, copies it into a Dafny sequence.
However, I do not know how to prove termination of such a function.
Is it possible? Any hints?
Cheers,
Tim



Hi Tim,
Fun, fun, fun! :) Essentially, you need to count the number of steps until the Nil, and then use that as the termination metric. In what I'm about to say, I'm assuming you have some familiarity with copredicates and prefix predicates (which are finite unrollings
of copredicates) in Dafny; if not, please see "Coinduction simply" [Leino and Moskal, FM 2014]. When a copredicate like IsInfiniteStream(s) holds, the corresponding prefix predicate holds for all unrollings. That is, IsInfiniteStream(s) is equivalent
to:
forall k: nat :: IsInfiniteStream#[k](s)
IsFiniteStream is the negation of IsInfiniteStream, so IsFiniteStream(s) is equivalent to:
exists k: nat :: !IsInfiniteStream#[k](s)
You can use that k as the bound, see
http://rise4fun.com/Dafny/2BxP. In that program, I broke StreamToSeq into two functions, the second of which takes the bound. To go from IsFiniteStream(s) to obtaining a k as in the existential quantification above, use to letsuchthat expression (which
is essentially Skolemization). I show the "decreases" clause explicitly in StreamToSeq', but Dafny will correctly guess it if you omit it.
A variation of this trick is used in the Filter program that I describe in "Automating Theorem Proving with SMT" [Leino, ITP 2013]. For the full program discussed there, see Test/dafny3/Filter.dfy in the Dafny test suite.
Finally, an orthogonal note about "static". In your example, you have declared the functions, predicates, and copredicates as static, but you don't have to for this example itself. Without the "static" keyword, the functions will have an
implicit receiver parameter ("this"), but that by itself does not hurt. However (and this is probably why you have declared them as static), if you want to put these functions into a module and refer to them from outside that module (that is, using
the module as a library), then they have to be static (or else you'll need to supply an actual receiver parameter). I'm planning to eventually change Dafny so that functions and methods (and thus predicates, copredicates, ghost methods, lemmas, colemmas,
etc.) declared lexically outside any "class" declaration will automatically be marked static.
Cheers,
Rustan



Hi
Thanks, makes sense. I am interested in modeling program executions that do not always terminate.
I copied everything from a module and forgot to remove the "static"s. I am using modules and module refinement to help organise my proofs.
Cheers,
Tim

