> > I guess we can't avoid the trick of taking a heap as argument and > requiring that it is equal to the real heap. Ideally I would have expected > something like: > > val zero: x: ref nat -> ST unit > (requires (fun h -> contains h x)) > (ensures (fun h0 r h1 -> modifies (only x) h0 h1 /\ sel h1 x = 0)) > (decreases (!x)) // or (decreases (fun h -> sel h x)) > = > if !x = 0 then () else begin > x := !x - 1; > zero x > end > > But this assumes that we can pass a computation (ST nat) to the decreases > argument of ST. >
`(decreases (fun h -> sel h x))` is what I proposed in the past as the most intuitive thing to do here (search for "decreases" here https://github.com/FStarLang/FStar/issues/753). I remember Nik had some reserves about this, but I don't know if they are still present. Catalin
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
