Create a gist now

Instantly share code, notes, and snippets.

module Typestate
open FStar.Heap
open FStar.ST
type state =
| Open
| Closed
type file = {
name: string;
state: ref state;
}
type isClosed file heap = (sel heap file.state) == Closed
type isOpen file heap = (sel heap file.state) == Open
val openHelper : file:file -> ST unit
(requires (fun heap -> isClosed file heap))
(ensures (fun heap _ heap' ->
isOpen file heap'
))
let openHelper file =
file.state := Open
val read : file:file -> ST int
(requires (fun heap -> isOpen file heap))
(ensures (fun heap _ heap' -> isOpen file heap'))
let read file =
13
val computeBase : unit -> Tot int
let computeBase () =
12
val readFromFile : file:file -> ST int
(requires (fun heap -> isClosed file heap))
(ensures (fun heap s heap' -> isClosed file heap'))
let readFromFile file =
openHelper file;
let x = computeBase () + read file in
file.state := Closed;
x
let () =
let file1 = {
name = "file1";
state = alloc Closed;
} in
let y = readFromFile file1 in
()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment