\usepackage{listings}
%\lstloadlanguages{C}
\lstdefinestyle{chalice}{%
  numbers=none,
  firstnumber=0,
  numberstyle=\tiny,
  stepnumber=5,
%  basicstyle=\scriptsize\sffamily,%
%  commentstyle=\itshape,%
%  keywordstyle=\bfseries,%
%  ndkeywordstyle=\bfseries,%
%  language=[Sharp]C,
  morekeywords={%
    above,acc,acquire,and,assert,assigned,assume,%
    below,between,bool,%
    call,class,const,%
    downgrade,%
    else,ensures,eval,exists,%
    false,fold,forall,fork,free,function,%
    ghost,%
    holds,%
    if,in,int,invariant,ite,%
    join,%
    lock,lockbottom,lockchange,%
    method,module,%
    new,nil,null,%
    old,%
    predicate,%
    rd,reorder,release,requires,result,returns,%
    seq,share,string,%
    this,token,true,%
    unfold,unfolding,unshare,%
    var,%
    waitlevel,while},
  literate=%
    {=}{{=~}}1%
    {+=}{{+}{=}~}3%
    {-=}{{-}{=}~}3%
    {*=}{{*}{=}~}3%
    {++}{{+}{+}}2%
    {--}{{-}{-}}2%
    {==}{==}2%
    {<=}{<=}2%
    {=>}{=>}2%
    {==>}{==>}3 %
    {<==>}{<==>}4 %
%% %    {!}{$\lnot$}1%  don't do this if ! is also used to indicate non-null types
    {!=}{!=}2%
}%
\lstnewenvironment{chalice}[1][]{%
  \lstset{style=chalice,
    floatplacement={tbp},showstringspaces=false,captionpos=b,
    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}%
\lstnewenvironment{chaliceNoLines}[1][]{%
  \lstset{style=chalice,
    floatplacement={tbp},showstringspaces=false,captionpos=b,
    xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}%
\def\S{%
    \lstinline[style=chalice,basicstyle=\ttfamily,columns=fixed]}
\newcommand{\lstfile}[1]{
  \lstinputlisting[style=chalice,%
    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
}