DOCSEARCHbyAlgolia
Submit Docs

Gospel Documentation

website·Indexed 29 days ago

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

A language for writing formal specifications for OCaml programs. Gospel allows developers to annotate OCaml types and functions with contracts, models, and invariants, translating these specifications into separation logic. The documentation covers installation, language semantics, function contracts, and a standard library (Gospelstdlib) providing predicates for common types like lists, sets, and arrays.

Tokens
11.7K
Snippets
100
Records
112
Agent score
72%

What's inside Gospel

  1. Overview of the Gospel Standard Library

    Gospel provides a standard library containing types, functions, and predicates specifically designed for use in specifications. While it mimics the naming conventions and patterns of the OCaml standard library to ease onboarding, it consists exclusively of logical symbols. Users must use the Gospel standard library in specifications instead of the OCaml standard library, as the latter is not permitted in specifications.

  3. Use OCaml attributes for Gospel specifications

    Gospel embeds specifications into OCaml files using OCaml attributes with the identifier gospel. The specifications are provided as strings within the attribute payload. Gospel uses two forms: [@@gospel "<spec>"] and [@@@gospel "<spec>"].

  4. Model a mutable data structure with a logical view

    In Gospel, you can attach a logical model to a type declaration to reason about its state. Use the mutable model syntax to define a field (like view) that represents the mathematical state of the object. This allows specifications to refer to the logical state of a type that may be opaque in the OCaml implementation.
    type 'a t
(*@ mutable model view: 'a sequence *)

  5. Handle preconditions and exceptions in Gospel

    Gospel provides three primary ways to handle assumptions about function arguments:

    1. Exceptional: Use raises to specify the state of the model when a specific exception is thrown.
    2. Unsafe (Precondition): Use requires to place the burden of proof on the caller. If the condition is not met, the behavior is undefined.
    3. Defensive (Runtime Check): Use checks to indicate the function internally verifies the condition and raises Invalid_argument if it fails.
    (* Exceptional Version *)
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 *)

(* Unsafe Version *)
val unsafe_pop: 'a t -> 'a
(*@ v = unsafe_pop q
    requires q.view <> Sequence.empty
    modifies q
    ensures  old q.view = q.view ++ (Sequence.cons v Sequence.empty) *)

(* Defensive Version *)
val pop: 'a t -> 'a
(*@ v = pop q
      checks   q.view <> Sequence.empty
      modifies q
      ensures  old q.view = q.view ++ (Sequence.cons v Sequence.empty) *)

  6. Understand Gospel language semantics and tool capabilities

    The semantics of the Gospel language are defined by its translation to separation logic. The gospel command-line tool performs type-checking on Gospel-specified modules; however, to fully exploit the semantics of these specifications, users must employ additional specialized tools from the Gospel ecosystem.

  7. Verify array properties with Gospel predicates

    Predicates used to assert properties about array contents, such as membership, quantification, and permutations.
    (* True if all elements of a satisfy f *
predicate for_all (f: 'a -> bool) (a: 'a t)

(* True if at least one element of a satisfies f *
predicate _exists (f: 'a -> bool) (a: 'a t)

(* True if x is equal to an element of a *
predicate mem (x: 'a) (a: 'a t)

(* True if a and b contain the same elements with the same occurrences *
predicate permut (a b: 'a array)

(* True if segment [lo..hi-1] of a is a permutation of [lo..hi-1] of b, and others are equal *
predicate permut_sub (a b: 'a array) (lo hi: integer)

(* Two-argument versions of for_all and _exists *
predicate for_all2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t)
predicate _exists2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t)

  8. Understand Gospel lexical conventions and OCaml compatibility

    Gospel adopts most of OCaml's lexical conventions, including whitespace rules, variable naming conventions, and integer representation. Developers familiar with OCaml can apply the same lexical rules to Gospel, with a few specific additions regarding keywords, symbols, and type modifiers.

  10. Specify preconditions using `requires` and `checks`

    Preconditions define properties that must hold at function entry. Gospel provides two ways to express them:

    1. requires: Defines conditions for well-specified behavior. If violated, the call is considered faulty, and all other contract guarantees (postconditions, etc.) are void.
    2. checks: Defines conditions that, if violated, cause the function to raise an OCaml Invalid_argument exception without modifying state. The call is not considered faulty; the caller must handle the exception.

    Interaction: If both are used, requires takes precedence. requires P and checks Q is equivalent to requires P and checks P -> Q.

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

  11. Declare non-terminating functions with `diverges`

    By default, OCaml functions with Gospel contracts are assumed to terminate. To specify that a function (such as a server loop or event listener) may not terminate, add the diverges keyword to the contract.
    val run : unit -> unit
(*@ run ()
    diverges
    (* ... *) *)

  12. Specify code equivalence in Gospel function contracts

    Use the equivalent keyword followed by a string containing OCaml code to specify that a function's behavior is equivalent to another piece of code. This is useful for functions whose behavior is difficult to express in pure logic. Note that the Gospel type-checker does not currently type-check the code inside equivalent clauses.
    type 'a t
val iter : ('a -> unit) -> 'a t -> unit
(*@ iter f t
    ... 
    equivalent "List.iter f (to_list t)" *)