Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Replace example png by actual code #384

Merged
merged 1 commit into from
Mar 11, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 53 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,9 +22,59 @@ interfaces with formal contracts that describe type invariants, mutability,
function pre-conditions and post-conditions, effects, exceptions, and [much
more](https://ocaml-gospel.github.io/gospel/)!

<div align="center">
<img src="screenshot.png" title="Gospel specification">
</div>
```ocaml
type 'a t
(*@ model capacity : integer
mutable model contents : 'a sequence
with s
invariant s.capacity > 0
invariant Sequence.length s.contents <= s.capacity *)

exception Full
exception Empty

val create : int -> 'a t
(*@ s = create n
requires n > 0
ensures s.capacity = n
ensures s.contents = Sequence.empty *)

val is_empty : 'a t -> bool
(*@ b = is_empty s
pure
ensures b <-> s.contents = Sequence.empty *)

val clear : 'a t -> unit
(*@ clear s
modifies s.contents
ensures s.contents = Sequence.empty *)

val push : 'a -> 'a t -> unit
(*@ push a s
modifies s.contents
ensures s.contents = Sequence.cons a (old s.contents)
raises Full -> Sequence.length (old s.contents) = s.capacity
/\ s.contents = old s.contents *)

val pop : 'a t -> 'a
(*@ a = pop s
modifies s.contents
ensures a = Sequence.hd (old s.contents)
ensures s.contents = Sequence.tl (old s.contents)
raises Empty -> old s.contents = Sequence.empty = s.contents *)

val pop_opt : 'a t -> 'a option
(*@ o = pop_opt s
modifies s.contents
ensures match o with
| None -> old s.contents = Sequence.empty = s.contents
| Some a -> old s.contents = Sequence.cons a s.contents *)

val top : 'a t -> 'a
(*@ a = top s
ensures a = Sequence.hd s.contents
raises Empty -> s.contents = Sequence.empty *)
```

We designed Gospel to provide a tool-agnostic frontend for bringing formal
methods into the OCaml ecosystem, meaning that we make no assumptions on the
Expand Down
Binary file removed screenshot.png
Binary file not shown.
Loading