Gospelstdlib (gospel.Gospelstdlib)

The following are not defined in the Gospelstdlib but are built-in in Gospel:

type unit
type string
type char
type float
type bool
type integer
type int

type 'a option
function None: 'a option
function Some (x: 'a) : 'a option

type 'a list
function ([]): 'a list
function (::) (x: 'a) (l: 'a list) : 'a list

predicate (=) (x y: 'a)

The rest of this module is the actual content of the Gospel module Gospelstdlib. This module is automatically opened in Gospel specifications.

Gospel declaration:
    type 'a sequence

The type for finite sequences.

Gospel declaration:
    type 'a bag

The type for finite unordered multisets.

Gospel declaration:
    type 'a ref

The type for references.

Gospel declaration:
    type 'a set

The type for finite unordered sets.

Arithmetic

The type integer is built-in. This is the type of arbitrary precision integers, not to be confused with OCaml's type int (machine, bounded integers).

Gospel declaration:
    function succ (x: integer) : integer

Gospel declaration:
    function pred (x: integer) : integer

Gospel declaration:
    function (-_) (x: integer) : integer

Gospel declaration:
    function (+) (x y: integer) : integer

Gospel declaration:
    function (-) (x y: integer) : integer

Gospel declaration:
    function ( * ) (x y: integer) : integer

Gospel declaration:
    function (/) (x y: integer) : integer

Gospel declaration:
    function mod (x y: integer) : integer

Gospel declaration:
    function pow (x y: integer) : integer

Gospel declaration:
    function abs (x:integer) : integer

Gospel declaration:
    function min (x y : integer) : integer

Gospel declaration:
    function max (x y : integer) : integer

Comparisons

Gospel declaration:
    predicate (>) (x y: integer)

Gospel declaration:
    predicate (>=) (x y: integer)

Gospel declaration:
    predicate (<) (x y: integer)

Gospel declaration:
    predicate (<=) (x y: integer)

Bitwise operations

Gospel declaration:
    function logand (x y: integer) : integer

Gospel declaration:
    function logor (x y: integer) : integer

Gospel declaration:
    function logxor (x y: integer) : integer

Gospel declaration:
    function lognot (x: integer) : integer

Gospel declaration:
    function shift_left (x y: integer) : integer

Shifts to the left, equivalent to a multiplication by a power of two

Gospel declaration:
    function shift_right (x y: integer) : integer

Shifts to the right, equivalent to a multiplication by a power of two with rounding toward -oo

Gospel declaration:
    function shift_right_trunc (x y: integer) : integer

Shift to the right with truncation, equivalent to a multiplication by a power of two with rounding toward 0

Machine integers

There is a coercion from type int to type integer, so that Gospel specifications can be written using type integer only, and yet use OCaml's variables of type int. The Gospel typechecker will automatically apply integer_of_int whenever necessary.

Gospel declaration:
    function integer_of_int (x: int) : integer 
    coercion

Gospel declaration:
    function max_int : integer

Gospel declaration:
    function min_int : integer

Couples

Gospel declaration:
    function fst (p: 'a * 'b) : 'a

fst (x, y) is x.

Gospel declaration:
    function snd (p: 'a * 'b) : 'b

snd (x, y) is y.

References

Gospel declaration:
    function (!_) (r: 'a ref) : 'a

Reference content access operator.

Sequences

Gospel declaration:
    function (++) (s s': 'a sequence) : 'a sequence

s ++ s' is the sequence s followed by the sequence s'.

Gospel declaration:
    function ([_]) (s: 'a sequence) (i: integer): 'a

s[i] is the ith element of the sequence s.

Gospel declaration:
    function ([_.._]) (s: 'a sequence) (i1: integer) (i2: integer): 'a sequence

Gospel declaration:
    function ([_..]) (s: 'a sequence) (i: integer): 'a sequence

Gospel declaration:
    function ([.._]) (s: 'a sequence) (i: integer): 'a sequence

module Sequence : sig ... end

Lists

The type 'a list and the constructors [] and (::) are built-in.

module List : sig ... end

Arrays

module Array : sig ... end

Bags

module Bag : sig ... end

Sets

Gospel declaration:
    function ({}) : 'a set

{} is the empty set.

module Set : sig ... end

Gospel declaration:
    function ( [->] ) (f: 'a -> 'b) (x:'a) (y: 'b) : 'a -> 'b

module Map : sig ... end

Maps from keys of type 'a to values of type 'b are represented by Gospel functions of type 'a -> 'b.

module Order : sig ... end

Other OCaml built-in stuff

exception Not_found

exception Invalid_argument of string

exception Failure of string

module Sys : sig ... end