Module Gospelstdlib

This file contains the Gospel standard library.

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 

Lists

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

Arrays

Bags

Sets

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

{} is the empty set.

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

Other OCaml built-in stuff