Revision 9be42a7de30adad4bbae854c929c9a6ba00edf14 authored by Son HO on 16 June 2020, 14:30:15 UTC, committed by Son HO on 16 June 2020, 14:30:15 UTC
1 parent d476397
Lib.Loops.fsti
module Lib.Loops
open FStar.HyperStack
open FStar.HyperStack.ST
open Lib.IntTypes
inline_for_extraction
val for:
start:size_t
-> finish:size_t{v finish >= v start}
-> inv:(mem -> (i:nat{v start <= i /\ i <= v finish}) -> Type0)
-> f:(i:size_t{v start <= v i /\ v i < v finish} -> Stack unit
(requires fun h -> inv h (v i))
(ensures fun h_1 _ h_2 -> inv h_2 (v i + 1))) ->
Stack unit
(requires fun h -> inv h (v start))
(ensures fun _ _ h_2 -> inv h_2 (v finish))
(*
{inv h0}
while (test ()) do
{inv h1 /\ guard h1}
body ()
{inv h2}
{~(guard h3) /\ inv h3}
*)
inline_for_extraction
val while:
inv: (mem -> Type0)
-> guard: (h:mem{inv h} -> GTot bool)
-> test: (unit -> Stack bool
(requires inv)
(ensures fun h0 b h1 -> b == guard h0 /\ h0 == h1))
-> body: (unit -> Stack unit
(requires fun h -> inv h /\ guard h)
(ensures fun _ _ h -> inv h))
-> Stack unit
(requires inv)
(ensures fun _ _ h -> inv h /\ ~(guard h))
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...