How to copy a finite stream in to a sequence

Apr 4, 2014 at 2:43 PM
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
Coordinator
Apr 4, 2014 at 5:05 PM
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 co-predicates and prefix predicates (which are finite unrollings of co-predicates) in Dafny; if not, please see "Co-induction simply" [Leino and Moskal, FM 2014]. When a co-predicate 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 let-such-that 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 co-predicates 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, co-predicates, ghost methods, lemmas, co-lemmas, etc.) declared lexically outside any "class" declaration will automatically be marked static.

Cheers,
Rustan
Marked as answer by rustanleino on 4/4/2014 at 10:05 AM
Apr 8, 2014 at 12:13 PM
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