Skip to content

Commit

Permalink
WLS: Add description of list generator syntax #23
Browse files Browse the repository at this point in the history
  • Loading branch information
DavePearce committed Aug 3, 2015
1 parent 4752beb commit 01ba0f4
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 5 deletions.
12 changes: 7 additions & 5 deletions WhileyLanguageSpecification/examples/ch6/eg_8.whiley
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
function rangeOf(int start, int end) -> [int]:
[int] r = []
int i = start
while i < end:
r = r ++ [i]
function cons(int head, [int] tail) -> [int]:
[int] r = [head; |tail| + 1]
int i = 0
//
while i < |tail|:
r[i+1] = tail[i]
i = i + 1
//
return r
Binary file modified WhileyLanguageSpecification/src/WhileyLanguageSpec.pdf
Binary file not shown.
20 changes: 20 additions & 0 deletions WhileyLanguageSpecification/src/expressions.tex
Original file line number Diff line number Diff line change
Expand Up @@ -425,6 +425,7 @@ \section{List Expressions}
\verb+ListExpr+ & $::=$ &\\
& $|$ & \verb+ListLengthOfExpr+\\
& $|$ & \verb+ListAccessExpr+\\
& $|$ & \verb+ListGeneratorExpr+\\
& $|$ & \verb+ListConstructorExpr+\\
\end{syntax}

Expand Down Expand Up @@ -466,6 +467,25 @@ \subsection{Access Expressions}

The above function computes the sum of a list by recursively breaking it down in successively smaller lists. The index-of operator is used to get the first item in the list at each stage, whilst the sublist operator is used to strip off that first element.

% =======================================================================
% Generator Expressions
% =======================================================================

\subsection{Generator Expressions}
\label{c_expr_generator}

A {\em list generator} accepts two arguments and produces a value of list type. The second argument must be of \lstinline{int} type and the list produced contains exactly this many occurrences of the first argument.

\begin{syntax}
\verb+ListGeneratorExpr+ & $::=$ & \token{[}\ \verb+UnitExpr+\ \token{;}\ \verb+UnitExpr+\ \token{]}\\
\end{syntax}

\paragraph{Examples.} The following example illustrates a list generator:

\lstinputlisting{../examples/ch6/eg_8.whiley}

This function constructs a list by prepending a given element onto the front of a given list. The list generator is used to construct the initial list of values whose size is one larger than the given list.

% =======================================================================
% List Expression
% =======================================================================
Expand Down

0 comments on commit 01ba0f4

Please sign in to comment.