Gospel

https://ocaml-gospel.github.io/gospel
Admin
Gospel is a behavioral specification language for OCaml interfaces that allows developers to write...
Tokens:35,925
Snippets:455
Trust Score:9.7
Update:1 month ago
Show doc for...
Tokens:
Raw
### Install Gospel via Opam

Source: https://ocaml-gospel.github.io/gospel/getting-started/installation

Use the Opam package manager to install the Gospel tool and library.

```bash
$ opam install gospel  
```

--------------------------------

### Verify Gospel installation

Source: https://ocaml-gospel.github.io/gospel/getting-started/installation

Check the installed version of the Gospel tool to confirm successful installation.

```bash
$ gospel --version  
gospel version 0.1.0  
```

--------------------------------

### Euclidean division function contract example

Source: https://ocaml-gospel.github.io/gospel/language/function-contracts

An example of a function contract for euclidean_division, demonstrating the use of a header, a requires precondition, and two ensures postconditions.

```gospel
val euclidean_division: int -> int -> int * int  
(*@ q, r = euclidean_division x y  
    requires y > 0  
    ensures  x = q * y + r  
    ensures  0 <= r < y *)  
```

--------------------------------

### function get (s: 'a t) (i: integer) : 'a

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Returns the element at a given index.

```APIDOC
## Function `get`

### Description
`get s i` is `s[i]`.

### Signature
```
function get (s: 'a t) (i: integer) : 'a
```

### Parameters
- **s** (`'a t`) - The sequence.
- **i** (`integer`) - The index of the element.

### Returns
- **'a** - The element at index `i`.
```

--------------------------------

### Union-find simple OCaml interface (type 'a element, make, find, union)

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Starting interface for the Gospel union-find example. Defines 'a element and the make, find, and union operations before ghost declarations are added. The interface does not expose the global universe set, which motivates the ghost-declaration specification.

```ocaml
type 'a element  
(** The type for set elements. *)  
  
val make : 'a -> 'a element  
(** [make x] is the singleton containing an element wrapping [x]. *)  
  
val find : 'a element -> 'a element  
(** [find e] is the representative of the subset containing [e]. *)  
  
val union : 'a element -> 'a element -> unit  
(** [union x y] merges the subset containing [x] with the subset  
    containing [y]. *)  
  

```

--------------------------------

### Type specification with model and invariant

Source: https://ocaml-gospel.github.io/gospel/language/type-specifications

Example of a container data-structure with a model for capacity and contents, and an invariant that the cardinal of contents is at most capacity. The model uses Gospel's standard library Set.t.

```ocaml
type 'a t  
(*@ model capacity: int  
    mutable model contents: 'a Set.t  
    with t invariant Set.cardinal t.contents <= t.capacity *)  

```

--------------------------------

### OCaml constant specification example: val argv with ensures Array.length argv >= 1

Source: https://ocaml-gospel.github.io/gospel/language/constant-specifications

Shows a constant specification for the value argv, asserting that Array.length argv >= 1. The clause holds at the end of the surrounding module evaluation.

```ocaml
val argv : string array  
(*@ ensures Array.length argv >= 1 *)  


```

--------------------------------

### Define Gospel specifications in .mli files

Source: https://ocaml-gospel.github.io/gospel/language/syntax

Gospel specifications are written in special comments starting with '@' after the corresponding OCaml value or type declaration.

```ocaml
val f: int -> int           (* An OCaml value declaration *)  
(*@ y = f x  
    ensures x > 0 *)        (* Its Gospel specification   *)  
  
(*@ type t *)               (* A ghost type declaration   *)  
(*@ ephemeral  
    model size: int *)      (* Its Gospel specification   *)  
```

--------------------------------

### Function contract with requires clause

Source: https://ocaml-gospel.github.io/gospel/language/function-contracts

Example of a function contract using 'requires' to specify that the divisor must be positive.

```OCaml
val eucl_division: int -> int -> int * int  
(*@ q, r = eucl_division x y  
    requires y > 0  
    ensures  x = q * y + r  
    ensures  0 <= r < y *)  

```

--------------------------------

### OCaml container interface with Gospel comments

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Defines a polymorphic container type 'a t with an exception Full and functions create, is_empty, clear, add, and mem. Gospel specifications are written in special comments starting with '@'.

```ocaml
type 'a t  
(** The type for containers. *)  
  
exception Full  
  
val create: int -> 'a t  
(** [create capacity] is an empty container whose maximum capacity  
    is [capacity]. *)  
  
val is_empty: 'a t -> bool  
(** [is_empty t] is [true] iff [t] contains no elements. *)  
  
val clear: 'a t -> unit  
(** [clear t] removes all values in [t]. *)  
  
val add: 'a t -> 'a -> unit  
(** [add t x] adds [x] to the container [t], or raises [Full] if  
    [t] has reached its maximum capacity. *)  
  
val mem: 'a t -> 'a -> bool  
(** [mem t x] is [true] iff [t] contains [x]. *)  

```

--------------------------------

### function init (n: integer) (f: integer -> 'a) : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/List/index.html

Creates a list of length n where each element is initialized by f.

```APIDOC
## Function `init`

### Description
`init n f` is a list of length `n`, with element number `i` initialized with `f i`.

### Declaration
```
function init (n: integer) (f: integer -> 'a) : 'a t
```

### Parameters
- **n** (`integer`) - The length of the resulting list.
- **f** (`integer -> 'a`) - The function used to initialize each element.

### Returns
- **'a t** - A list of length `n` with elements `f 0`, `f 1`, ..., `f (n-1)`.
```

--------------------------------

### choose

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Returns an arbitrary element from a set.

```APIDOC
## Function `choose`

### Description

`choose s` is an arbitrary element of `s`.

### Declaration
`function choose (s: 'a t) : integer`

### Parameters
- **s** ('a t) - The set to choose from.

### Returns
- **integer** - An arbitrary element of the set.
```

--------------------------------

### function make

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Array/index.html

Creates an array of a given length initialized with a value.

```APIDOC
## function make

### Description
`make n x` is an array of length `n`, initialized with `x`.

### Declaration
```gospel
function make (n: integer) (x: 'a) : 'a t
```
```

--------------------------------

### Ephemeral type with model

Source: https://ocaml-gospel.github.io/gospel/language/type-specifications

Example of a type annotated with the ephemeral keyword to indicate mutable state, along with a model.

```ocaml
type t  
(*@ ephemeral  
    model capacity: int *)  

```

--------------------------------

### function init

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Array/index.html

Creates an array of a given length where each element is computed by a function.

```APIDOC
## function init

### Description
`init n f` is an array of length `n`, with element number `i` initialized to the result of `f i`.

### Declaration
```gospel
function init (n: integer) (f: integer -> 'a) : 'a t
```
```

--------------------------------

### function init (n: integer) (f: integer -> 'a) : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Creates a sequence by applying a function to indices from 0 to n.

```APIDOC
## Function `init`

### Description
`init n f` is the sequence containing `f 0`, `f 1`, `...` , `f n`.

### Signature
```
function init (n: integer) (f: integer -> 'a) : 'a t
```

### Parameters
- **n** (`integer`) - The number of elements minus one.
- **f** (`integer -> 'a`) - A function that maps an index to an element.

### Returns
- **'a t** - The sequence of `f 0`, `f 1`, ..., `f n`.
```

--------------------------------

### Constant specification syntax: constant_specification = ("ensures" expr)*

Source: https://ocaml-gospel.github.io/gospel/language/constant-specifications

Defines the grammar for OCaml constant specifications as zero or more clauses, each starting with the ensures keyword followed by a formula.

```ebnf
constant_specification = ("ensures" expr)*  


```

--------------------------------

### choose_opt

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Returns an arbitrary element from a set, or None if empty.

```APIDOC
## Function `choose_opt`

### Description

`choose_opt s` is an arbitrary element of `s`, or `None` if `s` is empty.

### Declaration
`function choose_opt: 'a t -> 'a option`

### Parameters
- **s** ('a t) - The set to choose from.

### Returns
- **'a option** - An arbitrary element, or `None` if the set is empty.
```

--------------------------------

### Gospel contract for create

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Specifies a precondition that capacity `c` is positive and postconditions that the returned container's capacity equals `c` and its contents are empty.

```ocaml
val create: int -> 'a t  
(*@ t = create c  
    requires c > 0  
    ensures t.capacity = c  
    ensures t.contents = Set.empty *)  

```

--------------------------------

### Specify make Function

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Specifies the constructor for creating a new element, ensuring it is its own representative.

```Gospel
val make : 'a -> 'a element  
(*@ e = make [u: 'a universe] v  
    modifies u.dom  
    ensures not (Set.mem e (old u.dom))  
    ensures u.dom = Set.add e (old u.dom)  
    ensures u.rep = (old u.rep)[e -> e] *)  
```

--------------------------------

### function singleton (x: 'a) : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Creates a sequence containing a single element.

```APIDOC
## Function `singleton`

### Description
`singleton` is an alias for `return`. It creates a sequence containing a single element.

### Signature
```
function singleton (x: 'a) : 'a t
```

### Parameters
- **x** (`'a`) - The element to include in the sequence.

### Returns
- **'a t** - A sequence containing `x`.
```

--------------------------------

### Implement fib function with accumulator

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/fibonacci

OCaml implementation of `fib` that computes the nth Fibonacci number given two consecutive ones, `a` and `b`. Requires `n` non-negative; raises `invalid_arg` otherwise. Starts with `a` and `b` representing `fibonacci i` and `fibonacci (i+1)`.

```ocaml
let rec fib n a b = 
  if n < 0 then invalid_arg "n must be non-negative"; 
  if n = 0 then a
  else fib (n-1) b (a+b)
```

--------------------------------

### Specify create function

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/mutable-queue

Defines the contract for creating a new, empty queue. It assumes the returned queue is disjoint from previously allocated queues.

```GOSPEL
val create: unit -> 'a t  
(*@ q = create ()  
      ensures q.view = Sequence.empty *)  
```

--------------------------------

### singleton

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Creates a set containing a single element.

```APIDOC
## Function `singleton`

### Description

`singleton x` is `{x}`, a set containing only `x`.

### Declaration
`function singleton (x: 'a) : 'a t`

### Parameters
- **x** ('a) - The element to include.

### Returns
- **'a t** - A set containing exactly `x`.
```

--------------------------------

### Gospel contract for add (initial attempt)

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Specifies that `add` modifies the contents by adding `x` to the old contents, using the `old` primitive.

```ocaml
val add: 'a t -> 'a -> unit  
(*@ add t x  
    modifies t.contents  
    ensures t.contents = Set.add x (old t.contents) *)  

```

--------------------------------

### Specify make function contract

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Specifies the make function to ensure the returned element is fresh and added to the universe domain.

```ocaml
val make : 'a -> 'a element  
(*@ e = make [u: 'a universe] v  
    modifies u.dom  
    ensures not (Set.mem e (old u.dom))  
    ensures u.dom = Set.add e (old u.dom) *)  
```

--------------------------------

### add

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Adds an element to a set, resulting in the union with a singleton set.

```APIDOC
## Function `add`

### Description

`add x s` is `s ∪ {x}`, adding element `x` to set `s`.

### Declaration
`function add (x: 'a) (s: 'a t) : 'a t`

### Parameters
- **x** ('a) - The element to add.
- **s** ('a t) - The original set.

### Returns
- **'a t** - The resulting set.
```

--------------------------------

### Run gospel check on container.mli

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Run Gospel's type-checker on the container.mli file to verify that the specification is well-typed. Execute this command from the terminal in the directory containing container.mli.

```shell
$ gospel check ./container.mli  
```

--------------------------------

### Gospel contract for add with exception

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Completes the `add` contract by specifying that if it raises `Full`, the old contents had `t.capacity` elements and the contents remain unchanged.

```ocaml
exception Full  
val add: 'a t -> 'a -> unit  
(*@ add t x  
    modifies t.contents  
    ensures t.contents = Set.add x (old t.contents)  
    raises Full -> Set.cardinal (old t.contents) = t.capacity  
                /\ t.contents = old t.contents *)  

```

--------------------------------

### Multiple postconditions as conjunction

Source: https://ocaml-gospel.github.io/gospel/language/function-contracts

Shows that multiple 'ensures' clauses are equivalent to a single 'ensures' with the conjunction operator /\.

```ocaml
(*@ ...  
    ensures P  
    ensures Q *)  
```

```ocaml
(*@ ...  
    ensures P /\ Q *)  
```

--------------------------------

### to_list

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Converts a set to a list.

```APIDOC
## Function `to_list`

### Description

Converts a set to a list.

### Declaration
`function to_list (s: 'a t) : 'a list`

### Parameters
- **s** ('a t) - The set to convert.

### Returns
- **'a list** - The set as a list.
```

--------------------------------

### of_list

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Creates a set from a list.

```APIDOC
## Function `of_list`

### Description

Creates a set from a list.

### Declaration
`function of_list (l: 'a list) : 'a t`

### Parameters
- **l** ('a list) - The list to convert.

### Returns
- **'a t** - The set created from the list.
```

--------------------------------

### to_seq

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Converts a set to a sequence.

```APIDOC
## Function `to_seq`

### Description

Converts a set to a sequence.

### Declaration
`function to_seq (s: 'a t) : 'a Sequence.t`

### Parameters
- **s** ('a t) - The set to convert.

### Returns
- **'a Sequence.t** - The set as a sequence.
```

--------------------------------

### Gospel specification with forall over arrays

Source: https://ocaml-gospel.github.io/gospel/faq

Shows a Gospel specification for a function total_weight that uses a forall quantifier over arrays. This formula is not executable because it quantifies over every possible array.

```OCaml
val total_weight : weight:('a array -> int) -> ('a array) list -> int  
(*@ y = total_weight ~weight l  
    requires forall a. weight a >= 0  
    ensures y = List.fold_left (fun acc a -> acc + weight a) 0 l *)  
```

--------------------------------

### Simplified contract using a real argument i

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/fibonacci

Alternative contract that adds an extra `i` argument as a regular OCaml parameter. Quantification is removed because `i` is given. Still needs precondition `i >= 0` and similar `a`/`b` conditions.

```ocaml
val fib : i:int -> int -> int -> int -> int
(*@ r fib ~i n a b
    checks n >= 0
    requires i >= 0 /\ a = fibonacci i /\ b = fibonacci (i+1)
    ensures r = fibonacci (i+n) *)
```

--------------------------------

### Axiom for fibonacci postcondition

Source: https://ocaml-gospel.github.io/gospel/language/logical

Shows the equivalent axiom for the postcondition of `fibonacci`. The axiom states that for all n >= 0, fibonacci n >= 0.

```ocaml
(*@ axiom fibonacci_post : forall n. n >= 0 -> fibonacci n >= 0 *)  

```

--------------------------------

### function hd (s: 'a t) : 'a

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Returns the first element of a non-empty sequence.

```APIDOC
## Function `hd`

### Description
When `s` contains one or more elements, `hd s` is the first element of `s`.

### Signature
```
function hd (s: 'a t) : 'a
```

### Parameters
- **s** (`'a t`) - The sequence.

### Returns
- **'a** - The first element of `s`.
```

--------------------------------

### of_seq

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Creates a set from a sequence.

```APIDOC
## Function `of_seq`

### Description

Creates a set from a sequence.

### Declaration
`function of_seq (s: 'a Sequence.t) : 'a t`

### Parameters
- **s** ('a Sequence.t) - The sequence to convert.

### Returns
- **'a t** - The set created from the sequence.
```

--------------------------------

### Equivalent uninterpreted function and axiom for fibonacci

Source: https://ocaml-gospel.github.io/gospel/language/logical

Shows the equivalent of the previous contract as an uninterpreted function plus an axiom. The axiom states the definition holds when the precondition is true.

```ocaml
(*@ function fibonacci (n: integer) : integer *)  
  
(*@ axiom fibonacci_def : forall n. n >= 0 ->  
      fibonacci n =  
        if n <= 1 then n  
        else fibonacci (n-2) + fibonacci (n-1) *)  

```

--------------------------------

### function hd (l: 'a t) : 'a

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/List/index.html

Returns the first element of a non-empty list.

```APIDOC
## Function `hd`

### Description
When `l` contains one or more elements, `hd s` is the first element of `l`.

### Declaration
```
function hd (l: 'a t) : 'a
```

### Parameters
- **l** (`'a t`) - The list from which to take the head.

### Returns
- **'a** - The first element of `l`.
```

--------------------------------

### Declare Ghost Universe Constructor

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Introduces a ghost value constructor for the universe type.

```ocaml
(*@ val make_universe: unit -> 'a universe *)  
```

--------------------------------

### compare

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

A comparison function over sets, used for ordering sets.

```APIDOC
## Function `compare`

### Description

A comparison function over sets.

### Declaration
`function compare (s s': 'a t) : integer`

### Parameters
- **s** ('a t) - The first set to compare.
- **s'** ('a t) - The second set to compare.

### Returns
- **integer** - The comparison result.
```

--------------------------------

### function to_seq (s: 'a t) : 'a Sequence.t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/List/index.html

Converts a list to a sequence.

```APIDOC
## Function `to_seq`

### Description
Converts a list to a sequence.

### Declaration
```
function to_seq (s: 'a t) : 'a Sequence.t
coercion
```

### Parameters
- **s** (`'a t`) - The list to convert.

### Returns
- **'a Sequence.t** - The sequence representation of the list.
```

--------------------------------

### Use a predicate in a function contract

Source: https://ocaml-gospel.github.io/gospel/language/logical

Shows how to reuse the `is_sorted` predicate inside a function contract for `merge`. The contract requires sorted inputs and ensures a sorted output.

```ocaml
val merge: int array -> int array -> int array  
(*@ c = merge a b  
    requires is_sorted a  
    requires is_sorted b  
    ensures is_sorted c *)  

```

--------------------------------

### Verbose contract for fib with requires/ensures

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/fibonacci

Full contract for `fib` with preconditions and postcondition that uses an existential quantifier. Requires `n >= 0` and `i >= 0` with `a = fibonacci i`, `b = fibonacci (i+1)`. Ensures the result `r` equals `fibonacci (i+n)` whenever the preconditions hold.

```ocaml
val fib : int -> int -> int -> int
(*@ r = fib n a b
    checks n >= 0
    requires exists i.
              i >= 0 /\ a = fibonacci i /\ b = fibonacci (i+1)
    ensures forall i.
              i >= 0 /\ a = fibonacci i /\ b = fibonacci (i+1)
              -> r = fibonacci (i+n) *)
```

--------------------------------

### function to_list

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Array/index.html

Converts an array to a list.

```APIDOC
## function to_list

### Description
Converts an array to a list.

### Declaration
```gospel
function to_list (a: 'a t) : 'a list
```
```

--------------------------------

### empty

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Returns the empty set, denoted as ∅.

```APIDOC
## Function `empty`

### Description

`empty` is `∅`, the empty set.

### Declaration
`function empty : 'a t`

### Returns
- **'a t** - The empty set.
```

--------------------------------

### Gospel Formulae Syntax

Source: https://ocaml-gospel.github.io/gospel/language/expressions

Syntax for universal and existential quantification, conjunction, disjunction, equivalence, and implication in Gospel.

```text
forall x,y. rest  (* universal quantification of [x] and [y] in [rest] *)  
exists x,y. rest  (* existential quantification of [x] and [y] in [rest] *)  
form1 /\ form2    (* conjunction *)  
form1 \/ form2    (* disjunction *)  
form1 <-> form2   (* equivalence *)  
form1 -> form2    (* implication *)  
```

--------------------------------

### is_empty

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Determines whether a set is empty.

```APIDOC
## Predicate `is_empty`

### Description

`is_empty s` is `s = ∅`, indicating whether the set is empty.

### Declaration
`predicate is_empty (s: 'a t)`

### Parameters
- **s** ('a t) - The set to test.
```

--------------------------------

### Add a postcondition to a logical function

Source: https://ocaml-gospel.github.io/gospel/language/logical

Shows a recursive function `fibonacci` with both a precondition and a postcondition `ensures result >= 0`. The postcondition holds only when the precondition holds.

```ocaml
(*@ function rec fibonacci (n: integer) : integer =  
      if n <= 1 then n else fibonacci (n-2) + fibonacci (n-1) *)  
(*@ requires n >= 0  
    ensures result >= 0 *)  

```

--------------------------------

### Specify Union-Find Function Signatures

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Updates function specifications to include the ghost universe argument, noting modifications to the universe state.

```ocaml
val make : 'a -> 'a element  
(*@ e = make [u: 'a universe] v  
    modifies u *)  
  
val find : 'a element -> 'a element  
(*@ e = find [u: 'a universe] x *)  
  
val union : 'a element -> 'a element -> unit  
(*@ union [u: 'a universe] x y  
    modifies u *)  
```

--------------------------------

### Combine Gospel annotations with documentation comments

Source: https://ocaml-gospel.github.io/gospel/language/syntax

Gospel annotations can be used alongside traditional OCaml documentation comments.

```ocaml
val eucl_division: int -> int -> int * int  
(** this is an implementation of Euclidean division *)  
(*@ q, r = eucl_division x y  
    ... *)  
```

--------------------------------

### function tl (l: 'a t) : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/List/index.html

Returns the list of elements after the first element.

```APIDOC
## Function `tl`

### Description
When `l` contains one or more elements, `tl l` is the list of the elements of `l`, starting at position 2.

### Declaration
```
function tl (l: 'a t) : 'a t
```

### Parameters
- **l** (`'a t`) - The list from which to take the tail.

### Returns
- **'a t** - The list of elements after the first element.
```

--------------------------------

### function to_bag

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Array/index.html

Converts an array to a bag.

```APIDOC
## function to_bag

### Description
Converts an array to a bag.

### Declaration
```gospel
function to_bag (a: 'a t) : 'a bag
```
```

--------------------------------

### Specify modification constraints in exceptional postconditions

Source: https://ocaml-gospel.github.io/gospel/language/function-contracts

When a function raises an exception, you must manually specify if data remains unchanged using the old keyword in the raises clause.

```gospel
exception E  
val inplace_map : ('a -> 'a) -> 'a t -> unit  
(*@ inplace_map f a  
    modifies a.contents  
    raises E -> a.contents = old (a.contents) *)
```

--------------------------------

### Define a logical function in Gospel

Source: https://ocaml-gospel.github.io/gospel/language/logical

Defines a shortcut term `powm` for modular exponentiation using Gospel's `function` keyword.

```ocaml
(*@ function powm (x y m: integer) : integer = mod (pow x y) m *)  

```

--------------------------------

### Define Universe and Representative Invariants

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Defines the universe model with a domain and a representative function, including invariants for membership and idempotency.

```Gospel
(*@ type 'a universe *)  
(*@ mutable model dom : 'a element set  
    mutable model rep : 'a element -> 'a element  
    with u  
    invariant forall e. Set.mem e u.dom -> Set.mem (u.rep e) u.dom  
    invariant forall e. Set.mem e u.dom -> u.rep (u.rep e) = u.rep e *)  
```

--------------------------------

### partition

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Partitions a set into two sets based on a predicate.

```APIDOC
## Function `partition`

### Description

`partition f s` is the pair of sets `(s1, s2)`, where `s1` is the set of all elements of `s` that satisfy `f`, and `s2` is the set of all elements of `s` that do not satisfy `f`.

### Declaration
`function partition (f: 'a -> bool) (s: 'a t) : ('a t * 'a t)`

### Parameters
- **f** ('a -> bool) - The predicate.
- **s** ('a t) - The original set.

### Returns
- **('a t * 'a t)** - A pair of sets: (satisfying elements, non-satisfying elements).
```

--------------------------------

### Exceptional postcondition with pattern matching on Unix_error

Source: https://ocaml-gospel.github.io/gospel/language/function-contracts

Shows a raises clause with exhaustive pattern matching on the Unix_error exception, associating different postconditions with different arguments.

```ocaml
(*@ ...  
    raises Unix_error (ENAMETOOLONG, _, _) -> P  
         | Unix_error _                    -> Q *)  
```

--------------------------------

### function empty : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Returns the empty sequence.

```APIDOC
## Function `empty`

### Description
`empty` is the empty sequence.

### Signature
```
function empty : 'a t
```

### Returns
- **'a t** - The empty sequence.
```

--------------------------------

### Gospel contract for is_empty

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Specifies that `is_empty` is pure and its result is equivalent to the container's contents being empty.

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

```

--------------------------------

### Multiple exceptional postconditions hold independently

Source: https://ocaml-gospel.github.io/gospel/language/function-contracts

Shows two raises clauses for the same exception; each matching postcondition must hold in conjunction when the exception is raised.

```ocaml
(*@ ...  
    raises Error "foo" -> P | Error _ -> Q  
    raises Error x -> R *)  
```

--------------------------------

### Gospel contract for mem

Source: https://ocaml-gospel.github.io/gospel/getting-started/first-spec

Specifies that `mem` is pure and its result is equivalent to membership of `x` in the container's contents.

```ocaml
val mem: 'a t -> 'a -> bool  
(*@ b = mem t x  
    pure  
    ensures b <-> Set.mem x t.contents *)  

```

--------------------------------

### Specify find function contract

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Specifies the find function to ensure the input and output elements belong to the universe domain.

```ocaml
val find : 'a element -> 'a element  
(*@ e = find [u: 'a universe] x  
    requires Set.mem x u.dom  
    ensures Set.mem e u.dom *)  
```

--------------------------------

### map

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Applies a function to each element of a set, creating a new set.

```APIDOC
## Function `map`

### Description

`map f s` is a fresh set whose elements are `f x1 ... f xN`, where `x1 ... xN` are the elements of `s`.

### Declaration
`function map (f: 'a -> 'b) (s: 'a t) : 'b t`

### Parameters
- **f** ('a -> 'b) - The function to apply to each element.
- **s** ('a t) - The set to map over.

### Returns
- **'b t** - The mapped set.
```

--------------------------------

### function of_seq (s: 'a Sequence.t) : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/List/index.html

Converts a sequence to a list.

```APIDOC
## Function `of_seq`

### Description
Converts a sequence to a list.

### Declaration
```
function of_seq (s: 'a Sequence.t) : 'a t
```

### Parameters
- **s** (`'a Sequence.t`) - The sequence to convert.

### Returns
- **'a t** - The list representation of the sequence.
```

--------------------------------

### function to_seq

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Array/index.html

Converts an array to a sequence.

```APIDOC
## function to_seq

### Description
Converts an array to a sequence.

### Declaration
```gospel
function to_seq (a: 'a t) : 'a Sequence.t
```
```

--------------------------------

### Type specification syntax grammar

Source: https://ocaml-gospel.github.io/gospel/language/type-specifications

Grammar for type specifications, showing the structure of model clauses and invariant blocks.

```text
type_specification = "ephemeral"? model-clause* invariant-block?  
model-clause = "mutable"? "model" identifier ":" type_expression  
invariant-block = "with" identifier invariant-clause+  
invariant-clause = "invariant" expr  

```

--------------------------------

### function rev (l: 'a t) : 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/List/index.html

Returns the list with elements in reverse order.

```APIDOC
## Function `rev`

### Description
`rev l` contains the same elements as `l` in a reverse order.

### Declaration
```
function rev (l: 'a t) : 'a t
```

### Parameters
- **l** (`'a t`) - The list to reverse.

### Returns
- **'a t** - The reversed list.
```

--------------------------------

### diff

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Computes the difference of two sets.

```APIDOC
## Function `diff`

### Description

`diff s s'` is `s ∖ s'`, the difference of sets `s` and `s'` (elements in `s` but not in `s'`).

### Declaration
`function diff (s s': 'a t) : 'a t`

### Parameters
- **s** ('a t) - The first set.
- **s'** ('a t) - The second set.

### Returns
- **'a t** - The difference of the two sets.
```

--------------------------------

### Gospel declaration of is_pre_order

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Order/index.html

Defines the predicate `is_pre_order` for a comparison function `cmp`. It requires reflexivity (`cmp x x = 0`), antisymmetry (`cmp x y <= 0 <-> cmp y x >= 0`), and transitivity conditions for both non-strict and strict inequalities.

```gospel
Gospel declaration:
    predicate is_pre_order (cmp: 'a -> 'a -> int) =
      (forall x. cmp x x = 0) /\
      (forall x y. cmp x y <= 0 <-> cmp y x >= 0) /\
      (forall x y z.
         (cmp x y <= 0 -> cmp y z <= 0 -> cmp x z <= 0) /\
         (cmp x y <= 0 -> cmp y z <  0 -> cmp x z <  0) /\
         (cmp x y <  0 -> cmp y z <= 0 -> cmp x z <  0) /\
         (cmp x y <  0 -> cmp y z <  0 -> cmp x z <  0))
```

--------------------------------

### cardinal

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Set/index.html

Returns the number of elements in a set.

```APIDOC
## Function `cardinal`

### Description

`cardinal s` is the number of elements in `s`.

### Declaration
`function cardinal (s: 'a t) : integer`

### Parameters
- **s** ('a t) - The set.

### Returns
- **integer** - The cardinality of the set.
```

--------------------------------

### Exceptional pop specification

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/mutable-queue

Specifies a pop function that raises an Empty exception when the queue is empty, using ensures and raises clauses.

```ocaml
exception Empty  
  
val pop: 'a t -> 'a  
(*@ v = pop q  
    modifies q  
    ensures  old q.view = q.view ++ Sequence.cons v Sequence.empty  
    raises   Empty -> q.view = old q.view = Sequence.empty *)  
```

--------------------------------

### Specification of ghost and logical declarations with contract

Source: https://ocaml-gospel.github.io/gospel/language/attributes

Specification of ghost and logical declarations with a contract. The contract resides in an attribute attached to the string containing the declaration.

```ocaml
[@@@gospel "val f : int -> int"  
  [@@gospel "y = f x ensures x > 0"]]  

```

--------------------------------

### function set (s: 'a t) (i: integer) (x: 'a): 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Replaces an element at a given index.

```APIDOC
## Function `set`

### Description
`set s i x` is the sequence `s` where the `i`th element is `x`.

### Signature
```
function set (s: 'a t) (i: integer) (x: 'a): 'a t
```

### Parameters
- **s** (`'a t`) - The original sequence.
- **i** (`integer`) - The index of the element to replace.
- **x** (`'a`) - The new value.

### Returns
- **'a t** - A new sequence with the `i`th element replaced by `x`.
```

--------------------------------

### function length (s: 'a t): integer

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Returns the length of a sequence.

```APIDOC
## Function `length`

### Description
`length s` is the length of the sequence `s`.

### Signature
```
function length (s: 'a t): integer
```

### Parameters
- **s** (`'a t`) - The sequence whose length is to be computed.

### Returns
- **integer** - The length of the sequence.
```

--------------------------------

### function map (f: 'a -> 'b) (s: 'a t) : 'b t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Applies a function to each element of a sequence.

```APIDOC
## Function `map`

### Description
`map f s` is a sequence whose elements are the elements of `s`, transformed by `f`.

### Signature
```unction map (f: 'a -> 'b) (s: 'a t) : 'b t
```unction map (f: 'a -> 'b) (s: 'a t) : 'b t
```unction map (f: 'a -> 'b) (s: 'a t) : 'b t
```unction map (f: 'a -> 'b) (s: 'a t) : 'b t
```

### Parameters
- **f** (`'a -> 'b`) - The transformation function.
- **s** (`'a t`) - The input sequence.

### Returns
- **'b t** - A new sequence with each element transformed by `f`.
```

--------------------------------

### function cons (x: 'a) (s: 'a t): 'a t

Source: https://ocaml-gospel.github.io/gospel/gospel/Gospelstdlib/Sequence/index.html

Prepends an element to a sequence.

```APIDOC
## Function `cons`

### Description
`cons x s` is the sequence containing `x` followed by the elements of `s`.

### Signature
```
function cons (x: 'a) (s: 'a t): 'a t
```

### Parameters
- **x** (`'a`) - The element to prepend.
- **s** (`'a t`) - The original sequence.

### Returns
- **'a t** - A new sequence with `x` at the front.
```

--------------------------------

### Declare Ghost Universe Type

Source: https://ocaml-gospel.github.io/gospel/walkthroughs/union-find

Defines the ghost type 'a universe and marks it as ephemeral to indicate potential state changes.

```ocaml
(*@ type 'a universe *)  
(*@ ephemeral *)  
```
Tokens:
Raw