# 0  Introduction to SSG

SSG is a refinement checker based on the CSP theory. You can check the refinement relation between two processes modeled in CSP. Two semantics are supported: the traces semantics and the stable-failures semantics. In addition to the refinement checks, deadlock check and divergence check can be performed.

# 1  Prerequisites

• Knowledge of CSP
• Programming experience with a functional programming language

# 2  System requirements

CPU

• intel x86_64

Memory

• 8 GiB memory or more (depends on the size of models to be checked)

Operating System

• Linux
• macOS
• Microsoft Windows 10 (Bash on Windows is required)

C compiler

• gcc 4.9 or later

# 3  How to use SSG

Checking process consists of five steps:

1. Model the behavior of systems and expecting properties in CSP.
2. Translate the model into a C source file with SSG.
3. Compile the C source file with gcc and link with libssg.
4. Invoke the executable. It checks the properties specified in the model and generates a report file.
5. Consult the report file.

## 3.0  Invoking SSG

ssg model-filename c-filename

## 3.1  Compiling C source

gcc [-std=gnu11] -O3 -o check-prog c-filename -lssg -lpthread

The option -std=gnu11 is needed if gcc version is older than 5.1.

## 3.2  Invoking a checking program

check-prog [option ...]

### 3.2.0  Command-line options

-o report-filename

specify output report filename. If not specified, model-filename + ".report" is used as default.

specify the number of threads. The default is 1.

-m heap-size

specifiy the size of heaps in GiB. The default is 1 GiB.

Note that checking programs use four heaps per thread.

-t hashtable-size

specifiy the number of hashtable slots (not in bytes). The default is 4000037.

-v

verbose: print messages during the checking

-p

show the checking progress. The progress is roughly expressed with the number of states processed so far and the index number of the remaining states to be processed.

-h

show hashtable statistics. They are also going to be included in the report file. Note that the calculation of the statistics takes time.

-q

quiet: do not show messages during the checking.

-x

do not output the report file.

# 4  Modeling language

## 4.0  Syntax

### 4.0.0  Model elements

model ::= model-element ...

model-element ::= definition | assertion

definition ::=

constant-definition |

type-definition |

typename-definition |

function-definition |

channel-definition |

process-definition

constant-definition ::= (def constant-name expression)

function-definition ::= (def (function-name parameter-specifier ... ) expression)

process-definition ::=

(def process-name process) |

(def (process-name parameter-specifier ... ) process)

type-definition ::= (deftype type-name {literal | (constructor type-specifier ...)} ...)

typename-definition ::= (deftypename type-alias type-specifier)

channel-definition ::= (defch channel-name type-specifier ...)

assertion ::= (check property)

property ::=

(divergence process-name) |

(traces process-name process-name) |

(failures process-name process-name)

### 4.0.1  Types

type-specifier ::=

type-name

type-alias

bool

(int expression expression)

(list type-specifier expression)

(set type-specifier)

event

(channel type-specifier ...)

parameter-specifier ::= parameter | (parameter type-specifier)

parameter ::= symbol

### 4.0.2  Processes

process ::=

STOP

SKIP

(! event process)

(? channel (parameter ...) [guard] process)

(alt process ...)

(ndc process ...)

(seq process ...)

(par event-set process ...)

(hide event-set process)

(rename event-map process)

(xalt parameter-specifier range process)

(xndc parameter-specifier range process)

(xseq parameter-specifier range process)

(xpar parameter-specifier range event-set process)

(if expression process process)

(let ((parameter-specifier expression) ...) process)

(case expression (pattern process) ...)

event ::= expression

channel ::= expression

guard ::= expression

range ::= expression

event-set ::= expression

event-map ::= expression

pattern ::= literal | (constructor parameter ...)

### 4.0.3  Expressions

expression ::=

constant

parameter

( function-name expression ...)

channel-name

( channel-name expression ...)

literal

( constructor expression ...)

(type type-specifier expression)

(if expression expression expression)

(let ((parameter-specifier expression) ...) expression)

(case expression (pattern expression) ...)

(chset expression ...)

(chmap (expression expression) ...)

constant ::=

boolean

integer

UNIV

event

constant-name

type-alias

boolean ::= true | false

constant-name ::= symbol

function-name ::= symbol

process-name ::= symbol

type-name ::= symbol

type-alias ::= symbol

channel-name ::= symbol

literal ::= symbol

constructor ::= symbol

# 5  Types

## 5.0  Event

The type event represents event objects.

## 5.1  Channel

The type (channel type-specifier ...) represents channel objects. A channel ch of type $\mathtt{(channel}\ t_1\ \ldots\ t_n\mathtt{)}$ can take at most $n$ arguments. When $k$ $(k < n)$ arguments are supplied, $\mathtt{(}\mathit{ch}\ a_1\ \ldots\ a_k\mathtt{)}$ represents a channel which takes $n - k$ arguments. This is called a partial channel of ch. When $n$ arguments are supplied, $\mathtt{(}\mathit{ch}\ a_1\ \ldots\ a_n\mathtt{)}$ represents an event.

## 5.2  Boolean

The type bool represents logical values true and false.

## 5.3  Integer

The type (int a b) represents integers x such that ax < b.

## 5.4  List

The type (list type maxlen) represents lists which element type is type and the maximum length is maxlen.

## 5.5  Set

The type (set type) represents sets which element type is type.

## 5.6  Algebraic Data Type

Algebraic data types are defined with deftype operator.

(deftype type-name {literal | (constructor type-specifier ...)} ...)

For example, option type is defined as follows:

(deftype option None (Some (int 0 10))

The values of algebraic data types are destructed with case expressions:

(case e
(None e1)
((Some x) e2))

Note that neither polymorphic types or recursive types are supported.

# 6  Expressions

## 6.0  Constants

true and false are boolean constants.

Integer literals are represented as usual, such as 0, 123, -45.

UNIV means the universal set of each type.

event means the universal set of events. Note that event also means the type of events in the context of type-specifier.

Typenames defined with deftypename are regarded as the universal set which element type is equal to the typename. This is a shorthand notation of (type (set typename) UNIV).

## 6.1  Parameters

There are four types of parameters:

• Process and function parameters
• Channel parameters in channel receive form.
• Parameters introduced with let and case form.
• Parameters introduced with indexed operators: xalt, xndc, xseq, and xpar.

## 6.2  Function applications

Function applications take the form (f a ...), where f must a builtin function or a user-defined function.

Note that high-order functions are not supported.

## 6.3  Events and Channels

Events are defined in defch form with no type-specifiers for parameters. For example, an event e can be defined as follows:

(defch e)

This can be used in any place expecting an event, for example in prefix form:

(! e P)

On the other hand, if at least one type-specifier is specified in defch form, it defines a channel which parameter types are as specified. For example:

(defch ch (int -2 3) (int 0 4))

Since ch takes two parameters, (ch a b) represents events, whereas ch itself and (ch a) represent channels. These can be used as follows:

(! (ch a b) P)
(? ch (x y) P)
(? (ch a) (y) P)

Note that events may not be used in channel receive form.

(? e () P) ; wrong

## 6.4  Literals and Contructors of Algebraic Data Types

Literals of algebraic data types are constants.

Constructors are regarded as functions, and a constructor itself is not an expression because high-order functions are not supported. Only constructors with exactly the same number of arguments as defined are expressions.

Suppose that the following definition is given:

(deftype t A (B bool) (C (int -2 3) (int 0 5)))

In this case, A, (B false), and (C -1 2) are all expressions, but B, C, and (C -1) are not.

## 6.5  chset

chset is an operator to construct a set of events.

(chset event-or-channel ...)

You can specify events and channels together in chset regardless of their types. For example when we have the following channels:

(defch a)
(defch ch (int -1 2))
(defch ch2 bool (int -1 2))

(chset a ch (ch2 false)) means a set of events { a, (ch -1), (ch 0), (ch 1), (ch2 false -1), (ch2 false 0), (ch2 false 1) }.

## 6.6  chmap

chmap is an operator to construct an event map which maps events to events.

(chmap (event-or-channel  event-or-channel) ...)

Suppose $\mathtt{(}\mathit{ch}_1\ \mathit{ch}_2\mathtt{)}$ are specified in chmap where $\mathit{ch}_1$ is defined with types $t_1\ t_2\ \ldots\ t_m$ and $\mathit{ch}_2$ with $u_1\ u_2\ \ldots\ u_n$.

If $m \le n$ then $t_1\ \ldots\ t_m$ and $u_1\ \ldots\ u_m$ must match respectively and each $\mathtt{(}\mathit{ch}_1\ a_1\ \ldots\ a_m\mathtt{)}$ is mapped to $\mathtt{(}\mathit{ch}_2\ a_1\ \ldots\ a_m\ b_{m+1}\ \ldots\ b_n\mathtt{)}$ where $b_{m+1}\ \ldots\ b_n$ are arbitrary. This means one-to-many mapping.

If $m \ge n$ then $t_1\ \ldots\ t_n$ and $u_1\ \ldots\ u_n$ must match respectively and each $\mathtt{(}\mathit{ch}_1\ a_1\ \ldots\ a_n\ b_{n+1}\ \ldots\ b_m\mathtt{)}$ is mapped to $\mathtt{(}\mathit{ch}_2\ a_1\ \ldots\ a_n\mathtt{)}$. This means many-to-one mapping.

## 6.7  if

(if b  x  y)

If b evaluates to true, the value of this expression is x, otherwise y.

## 6.8  let

(let ((parameter-specifier  e) ...) expr)

parameter-specifier ::= parameter | (parameter type-specifier)

The let form introduces new parameters. The expression expr is evaluated in the environment where each parameter is bound to the result of evaluation of the paired expressions e.

## 6.9  case

(case e (pattern  expr) ...)

pattern ::= literal | (constructor parameter ...)

The expression e must be an expression which evaluates to a value of an algebraic data type defined with deftype. The branch which pattern matches to the value is selected, each parameter in the pattern is bound to the corresponding value, then the expression expr of the branch is evaluated.

Note that literals and constructors in the patterns must be exclusive and exhaustive. There is no "else" form.

## 6.10  type

(type type-specifier expression)

The operator type coerces the type of expression to the type specified by type-specifier.

Note that type coercion on lists and sets are not supported (except UNIV).

(def (P (xs (list (int -2 3) 4)))
(Q (type (list (int 0 8) 4) xs)))    ; wrong

(def X (type (set (int -2 3)) UNIV))   ; ok


# 7  Processes

## 7.0  STOP

STOP

CSP: $\mathrm{STOP}$

## 7.1  SKIP

SKIP

CSP: $\mathrm{SKIP}$

## 7.2  Process Call

process-name

(process-name expression ...)

Represent a process defined with def. The second form is used when the process takes parameters.

## 7.3  Prefix

(! e  P)

CSP: $e \rightarrow P$

(? ch (x ...) [guard] P)

$\begin{split} \mathrm{CSP:}\ & \mathit{ch}?x \rightarrow P \\ & \mathit{ch}?x:\{\,x\,|\,\mathit{guard}\,\} \rightarrow P \end{split}$

The expression guard is a condition which determines whether the process receives data or not. The process receives data if and only if guard evaluates to true. If guard evaluates to false, the process stops. guard is optional. If it is not specified, it is assumed to be true. Note that the parameters of the channel can be referred to in guard.

Example:

(defch ch (int -2 3))

(def (P (x (int -2 3)))
(? ch (y) (>= y x) (Q x y)))


## 7.5  Alternatives (external choice)

(alt P ... )

CSP: $P\ \square\ Q$

(alt) = STOP

(alt P) = P

## 7.6  Non-deterministic choice (internal choice)

(ndc P Q ...)

CSP: $P \sqcap Q$

Note that at least one process is required.

## 7.7  Sequential composition

(seq P ...)

CSP: $P; Q$

(seq) = SKIP

(seq P) = P

## 7.8  Parallel composition

(par X P Q R ...)

CSP: $P\ \underset{X}{||}\ Q$

X is a set of events. Note that at least two processes are required.

## 7.9  Hiding

(hide X P)

CSP: $P\ \backslash\ X$

X is a set of events.

## 7.10  Renaming

(rename R P)

CSP: $P[\![R]\!]$

R is a map from events to events, which can be constructed with chmap.

Example:

(def P
(rename (chmap (a b) (ch ch2)) Q))


## 7.11  Indexed operators

Indexed operators are folding forms of a sequence of processes for an operator. Four operators alt, ndc, seq, and par have corresponding indexed-operators xalt, xndc, xseq, and xpar respectively.

They commonly have three components: parameter-specifier, range, and process and takes the following form:

(xop parameter-specifier range [other-components] process)

where xop is one of four operators.

This form means the process which is the result of folding a sequence of processes by the operator corresponding to xop. The sequence of processes is obtained by enumerating the value in range and substituting it for the parameter in process. Either a set or a list can be used as a range except for xseq. For xseq only a list can be used because the operator seq does not satisfy the commutative law.

parameter-specifier has the following form:

parameter-specifier ::= parameter | (parameter type-specifier)

If it is unable to decide the type of the parameter from the context, type-specifier is required.

(xalt parameter-specifier range P)

CSP: $\underset{x \in S}{\square} P$

(xndc parameter-specifier range P)

CSP: $\underset{x \in S}{\sqcap} P$

(xseq parameter-specifier range P)

CSP: $\underset{x \in S}{;} P$

Note that range $(S)$ must be of type list.

(xpar parameter-specifier range event-set P)

CSP: $\underset{x \in S}{\underset{X}{||}} P$

## 7.12  if

(if b  P  Q)

CSP: $P <\!\!\!\!|\ b>\!\!\!\!\!|\ \,Q$

## 7.13  let

(let ((parameter-specifier  expression) ...) P)

parameter-specifier ::= parameter | (parameter type-specifier)

The let form introduces new parameters. The process P is executed in the environment where each parameter is bound to the result of evaluation of the expressions expression.

## 7.14  case

(case e (pattern  P) ...)

pattern ::= literal | (constructor parameter ...)

The expression e must be an expression which evaluates to a value of an algebraic data type defined with deftype. The branch which pattern matches to the value is selected, each parameter in the pattern is bound to the corresponding value, then the process P of the branch is executed.

Note that literals and constructors in the patterns must be exclusive and exhaustive. There is no "else" form.

# 8  Definitions

## 8.0  Constant definitions

Constants are defined with the operator def.

Examples:

(def N 4)
(def X (type (set (int -2 3)) (set -2 0 2)))


## 8.1  Type definitions

Algebraic Data Types are defined with the operator deftype.

Examples:

(deftype option None (Some (int -2 3)))
(deftype state Running Ready (Waiting objtype))


## 8.2  Typename definitions

Typenames are defined with the operator deftypename.

Examples:

(def M 4)
(def L 3)
(deftypename Domain (int 0 M))
(deftypename Seq (list Domain L))


Note that typenames are regarded as the universal set which element type is equal to the typename.

## 8.3  Function definitions

Functions are defined with the operator def.

Examples:

(def N 4)
(def (inc (x (int 0 N))) (mod (+ x 1) N))


In general, type-specifiers for parameters are required.

## 8.4  Event and Channel definitions

Events and channels are defined with the operator defch.

Examples:

(defch e)                     ; event
(defch ch (int -2 3))         ; channel which takes one parameter
(defch ch2 bool (int -2 3))   ; channel which takes two parameters


## 8.5  Process definitions

Processes are defined with the operator def.

Examples:

(def P (! e P))

(def (Q (xs (list (int -2 3) 4)))
(if (null? xs)
SKIP
(! (ch (car xs)) (Q (cdr xs)))))

(def SYSTEM
(hide (chset mch)
(par (chset mch)
(PRODUCER 0)
(CONSUMER 1))))


# 9  Assertions

Check if the process P has a deadlock state or not. If a deadlock state is found, the state and the shortest path from the initial state to the state are reported.

(check (divergence P))

Check if the process P has a divergence or not. In finite models, a divergence is a cycle of internal transitions. If a divergence is found, the cycle and the shortest path from the initial state to the state on the cycle are reported.

(check (traces P Q))

Check if the process Q refines the process P on the traces semantics. The condition does not hold if and only if there is a tuple of a trace $s$, a state $p$ of P, a state $q$ of Q, and an event $e$ that $p$ is reachable from the initial state of P through the trace $s$ and $q$ is reachable from the initial state of Q through the trace $s$ and $q$ has a transition labelled with the event $e$ but $p$ does not (trace violation). If the condition does not hold, the trace $s$, the pair of states $(p, q)$, and the event $e$ are reported.

Note that the reported trace is not guaranteed to be the shortest trace to the violation state.

(check (failures P Q))

Check if the process Q refines the process P on the failures semantics.

Since failures check implies traces check, if there is a trace violation, it is reported.

If there is a refusals violation, the violating states, the path from the initial states to the states, the initial events that Q offers at the state, and the minimal acceptances of the state of P are reported.

Note that the reported path is not guaranteed to be the shortest path to the violation state.

# 10  Report file

A report file consists of sections. Most of the sections correspond to the internal checking phase and it is not necessary to understand what is done in each phase. The important section to be consulted is a violation section which is a subsection of the phase section that the violation is detected.

The rest of sections are information sections which record the settings of the check program and statistics of the execution.

## 10.0  Structure of a report file

(model model-filename  section ...)

## 10.1  violation section

In deadlock violation, the following information is shown:

state

path

the shortest path from the initial state to the deadlock state

Example:

(violation (deadlock P)
(state STOP)
(path
(0 - ("(! a (! b (! c (! d  .."))
(1 a ("(! b (! c (! d (! e  .."))
(2 b ("(! c (! d (! e STOP)))"))
(3 c ("(! d (! e STOP))"))
(4 d ("(! e STOP)"))
(5 e STOP)))


### 10.1.1  Divergence

In divergence violation, the following information is shown:

initial-state-to-loop

the length of the path from the initial state to the tau cycle

tau-loop-length

the length of tau cycle

initial-path

the path from the initial state to the tau cycle

tau-loop

the tau cycle

Example:

(violation (divergence S)
(initial-state-to-loop 4)
(tau-loop-length 3)
(initial-path
(0 - ("(! a (! b (! c S1)))"))
(1 a ("(! b (! c S1))"))
(2 b ("(! c S1)"))
(3 c (hide 2 ("(! x (! x (! x S2)))"))))
(tau-loop
(hide 2 ("(! x (! x (! x S2)))"))
(hide 2 ("(! x (! x S2))"))
(hide 2 ("(! x S2)"))))


### 10.1.2  Trace violation

In traces violation, the following information is shown:

event

the violation event

state

the violation state on the implementation side

initials-imp

the initial events the implementation offers in the violation state

initials-spec

the initial events the specification offers in the violation state

path

the path from the initial state to the violation state

stateset

the set of states on the specification side

Example:

(violation (traces Q P)
(event a)
(state ("(alt (! a STOP) (! e  .."))
(initials-imp (a e))
(initials-spec (e))
(path
(0 - ("(! a (! b (! c (! d  .."))
(1 a ("(! b (! c (! d (alt  .."))
(2 b ("(! c (! d (alt (! a  .."))
(3 c ("(! d (alt (! a STOP)  .."))
(4 d ("(alt (! a STOP) (! e  ..")))
(stateset 1
("(! e STOP)") ))


### 10.1.3  Failures violation

In failures violation, the following information is shown:

state

the violation state on the implementation side

initials-imp

the initial events the implementation offers in the violation state

initials-spec

the initial events the specification offers in the violation state

minimal-acceptances

the minimal acceptances of the specification

path

the path from the initial state to the violation state

stateset

the set of states on the specification side

Example:

(violation (failures Q P)
(state ("(! a STOP)"))
(initials-imp (a))
(initials-spec (a b c))
(minimal-acceptances
(a b)
(b c)
(a c))
(path
(0 - ("(ndc (! a STOP) (! b  .."))
(1 tau ("(! a STOP)")))
(stateset 4
("(ndc (alt (! a STOP)  ..")
("(alt (! c STOP) (! a  ..")
("(alt (! b STOP) (! c  ..")
("(alt (! a STOP) (! b  ..") ))


## 10.2  settings section

settings section records the SSG version and the option settings.

• SSG version
• heap size in bytes.
• hashtable size in slots.
(settings
(version 1 0 0)
(heap 1073741824)
(hashtable-size 4000037))


## 10.3  statistics section

statistics section records the time it took to check and the memory size consumed in each heap. A checking program uses four heaps per thread.

heap0 is used for storing data such as LTSs, DLTSs, and minimal acceptances which are used in the succeeding phases. The size of heap0 shown in the report indicates the final size when all checks are done.

The other three heaps are used for storing temporary data in each phase. The values shown in the report indicate the maximum (peak) size of each heap used through the checks.

(statistics
(time 3043)
(heap0 39895920)
(heap1 16689656)
(heap2 4920)
(heap3 0))


## 10.4  event-set section

event-set section shows the mappings from event set ID to the value. Basically, values shown in a report are represented as in the same form in the modeling language. However, a set of events is shown by ID because its representation can be big.

Note that ID 0 is the empty set and ID 1 is the universal set.

(event-set
(2 ((ch1 0) (ch1 1) (ch1 2) (ch1 3)))
(3 ((ch3 0) (ch3 1) (ch3 2) (ch3 3)))
(4 ((ch2 0) (ch2 1) (ch2 2) (ch2 3)))
(5 ((ch5 0) (ch5 1) (ch5 2) (ch5 3)))
(6 ((ch4 0) (ch4 1) (ch4 2) (ch4 3))))


## 10.5  hashtable section

hahstable section is recorded when -h option is specified. It shows the statistics of the hashtable operations in order to adjust the hashtable size by the -t option.

• ent/slot-avg is (the number of states) / (the number of slots).
• occupation is (the number of slots used) / (the number of slots).
• conflicts-max is the maximum length of a chain.
• conflicts-avg is the average length of a chain.
• retry-count is the total number of retried count when adding an entry due to the conflict among threads.
(hashtable
(ent/slot-avg 0.001365)
(occupation 0.001365)
(conflicts-max 1)
(conflicts-avg 1.000000)
(retry-count 0))


## 10.6  Internal phases

Unfolding

Unfolding is a phase to find all reachable states from the initial state and their transitions. This phase generates a Labelled-Transition-System, a.k.a. an LTS.

If the assertion to check deadlock is specified for a process in a model, this phase is performed instead of unfolding. It tries to find deadlock state and the shortest path from the initial state while unfolding the process.

Checking divergence

If the assertion to check divergence is specified for a process in a model, this phase is performed just after the unfolding phase for the process. It tries to finds a cycle consisting of internal transitions (transitions with the internal event τ, in short τ-transitions). If a cycle is found, the shortest path from the initial state to one of the states on the cycle is calculated.

Determinizing

Determinizing is a phase to convert an LTS into a deterministic LTS, which is called a DLTS. A DLTS is an LTS in which every state has no τ-transitions. Each state in a DLTS is a set of states in the original LTS which can be reached from the initial state through the same trace.

Calculating minimal acceptances

If an assertion to check refinement relation on the stable-failures is specified for a process as the specification in a model, this phase is performed just after the determinizing phase for the process. It calculates one of the other representations of refusals called minimal acceptances for each state in the DLTS generated in determinizing phase.

Checking refinement relation

The phase tagged with traces and failures are phases to check refinement relation between two processes. It compares the traces (in the case of both traces and failures) and the refusals of each state (in the case of failures) of two processes based on a DLTS (with minimal acceptances) and an LTS.

# 11  Builtin functions

## 11.0  Equivalence

(= x y)

return true iff x and y are equal.

## 11.1  Boolean

(not x)

return false if x true, otherwise true.x

(and x ...)

return true iff all of x ... are true.

(or x ...)

return false iff all of x ... are false.

## 11.2  Integer

(< x y)

return true iff x < y

(> x y)

return true iff x > y

(<= x y)

return true iff x <= y

(>= x y)

return true iff x >= y

(+ x ...)

return the sum of x ...

(- x)

return 0 - x

(- x y)

return x - y

(* x ...)

return x * ...

(div x y)

return the quotient of x / y.

(mod x y)

return the remainder of x / y.

(expt x n)

return x to the n-th power.

## 11.3  List and Set

(mem x collection)

return true iff x is a member of collection. collection must be a list or a set.

(remove collection x)

return the same type of collection which member is in collection and is not equal to x. When collection is a list, the order is preserved.

(list->set xs)

return a set which includes all members of xs.

(set->list s)

return a list in which each member of s occurs exactly once. The order of elements is arbitrary.

## 11.4  List

(list x ...)

return a list concisting of x ...

(null? xs)

return true iff xs is the empty list.

(length xs)

return the length of the list xs.

(car xs)

return the car of xs. xs must be non-nil.

(cdr xs)

return the cdr of xs. xs must be non-nil.

(last xs)

return the last element of xs. xs must be non-nil.

(butlast xs)

return the prefix list other than the last element of xs. xs must be non-nil.

(ref xs k)

return the k-th element of xs.

(take xs k)

return the prefix list of xs which length is k. 0 ≤ k(length xs).

(drop xs k)

return the tail list of xs which length is (length xs) - k. 0 ≤ k(length xs).

(cons x xs)

return the list which car is x and cdr is xs.

(append1 xs x)

return the list which is the result of adding x to the tail of xs.

(append xs ...)

return the list which is the result of appending x ...

(update xs k x)

return the list which is the result of replacing the k-th element of xs with x.

(remove1 xs x)

return the list which is the result of removing the first occurrence of x in xs.

(find-index xs x)

return the index of the first occurrence of x in xs. If x in not xs, -1 is returned.

(insert xs k x)

return the list which is the result of inserting x at the position indicated by k in xs. 0 ≤ k(length xs).

(remove-index xs k)

return the list which is the result of removing the k-th element of xs.

(reverse xs)

return the reversed list of xs.

(interval a b)

return the list which elements are from a to b exclusive.

(make-list n x)

return the list which length is n and every elements is x.

## 11.5  Set

(set x ...)

return the set which elemets are x ...

(empty? s)

return true iff s is empty.

(subset? s t)

return true iff s is a ubset of t.

(card s)

return the number of elemetns in s.

return the set which is the result of adding x ... to s.

(union s ...)

return the union of s ...

(inter s t ...)

return the intersection of s t ...

(diff s t ...)

return the difference set of s of t ...

(choice s)

return an arbitrary element of s. s must be non-empty.