Revision e292f893ebb78425a9dcecc759c8e79bbc6f8f3b authored by Jay Bosamiya on 07 June 2019, 00:26:22 UTC, committed by Jay Bosamiya on 07 June 2019, 00:34:42 UTC
1 parent f7d7872
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))
Computing file changes ...