%\documentclass[11pt]{article}
%\usepackage[hmargin=18mm,vmargin=12mm]{geometry}
\documentclass[fontsize=11pt,paper=letter]{scrartcl}
\usepackage[hmargin=15mm,vmargin=15mm]{geometry}

%{{{ packages and macros
%\usepackage{proof} %style is available here: http://research.nii.ac.jp/%7Etatsuta/proof-sty.html
%\usepackage{amsmath,amssymb}
%\usepackage{MnSymbol}
%\usepackage{formac}
%\usepackage{etex}
%\usepackage{edcomms}
%\input diagram-2.2.tex
\usepackage{graphicx}
\usepackage{listings}
\usepackage{listingsACSL}
\lstset{%
  language=[ACSL]C,
  frame=single,
  identifierstyle=\slshape,
  columns=flexible}

\parindent0pt\parskip0.6ex % Better for literate code.

\def\shows{\vDash}
%}}}


\pagestyle{empty}
\usepackage{hyperref}
\begin{document}

%{{{ Linked Lists
\textbf{Linked Lists}

\kern1ex
Use the following datatype
for implemeting singly-linked lists in C:
\begin{lstlisting}
typedef int value_type;

typedef struct _cons { value_type head;
                       struct _cons * tail;
                     } nonEmptyList;

typedef nonEmptyList * list; // NULL used as Nil

#define Nil NULL

/*@
  logic list Nil = \null;

  inductive hasSuffix{L} (list xs, list ys) {
    case hasSuffix_refl{L}:
      \forall list xs; hasSuffix(xs,xs);
    case hasSuffix_next{L}:
      \forall list xs, ys;
        \valid(xs) ==> hasSuffix(xs->tail, ys) ==> hasSuffix(xs,ys);
  }

  predicate finite{L}(list xs) = hasSuffix(xs,Nil);
*/

nonEmptyList * cons(value_type x, list xs) { // NULL used as error
  nonEmptyList * result = malloc(sizeof(struct _cons));
  if (result)
    { result->head = x;
      result->tail = xs;
    }
  return result;
}
\end{lstlisting}
Note:
\begin{itemize}\itemsep=0.2ex
\item \lstinline|_cons| is a struct name.

  This name starts with un underscore to document that it should not
  be used by users of this declaration.
  
\item \lstinline|struct _cons| is a type, the same type as:
\item \lstinline|struct { value_type head; struct _cons * tail; }|.
\item The \lstinline|typedef ... nonEmptyList| makes ``\lstinline|nonEmptyList|'' another name for that type.
\item \textbf{\lstinline|list| is the type of (possibly empty!) lists!}
\end{itemize}

\pagebreak
%\medskip
%\hrule
%
%\medskip
The code listings above have been produced by including,
before \verb|\begin{document}|, the following:
\begin{lstlisting}[language=TeX,identifierstyle=\ttfamily]
\usepackage{listings}
\usepackage{listingsACSL}
\lstset{%
  language=[ACSL]C,
  frame=single,
  identifierstyle=\slshape,
  columns=flexible}
\end{lstlisting}
I am using no other packages that might be interfering ---
if you run into trouble, perhaps comment out some
\verb/\usepackage{...}/
lines you don't need?
\end{document}

%{{{ EMACS lv
% Local Variables:
% folded-file: t
% fold-internal-margins: 0
% end:
%}}}